proposition: Lemma ex4_propc x (s := fun_image I (fun z => ex4_fct_s (Vg x z))): inc x (projective_limit ex4_system) -> countable_set s /\ cofinal r s.
proof: Proof. move:ex4_system_prop =>[s_E s_I s_r s_f]. move => /prl_limitP; rewrite s_I s_r s_E s_f ; move => [fgx dx xa xb]. have ha i: inc i I -> inc (Vg x i) (ex4_setEi i). move=> iI; move:(xa _ iI); rewrite LgV//. pose rr i := ex4_fct_r (Vg x i). pose ss i := ex4_fct_s (Vg x i). have rri i: inc i I -> rr i = i by move => /ha /Zo_P[]. have hb i: inc i I -> inc (ss i) I /\ glt r i (ss i). move => iI; move/Zo_P:(ha _ iI)=> [xf _]. by case:(ex4_fct_r_in_I xf); rewrite -/(rr i) -/(ss i) (rri _ iI). move:(ex4H) => [_ or sr rdr _]. have cf: cofinal r s. split; first by move => t /funI_P [i /hb [qa _] ->]; rewrite sr. rewrite sr => i iI; move:(hb _ iI) => [qa [qb _]]; exists (ss i) => //. by apply/funI_P; exists i. split => //. have hc i j: inc i I -> inc j I -> domain (Vg x i) = domain (Vg x j) -> ss i = ss j. move/right_directedP: rdr => [_];rewrite /right_directed_prop sr => rdr'. move => iI jI sd. move:(rdr' _ _ iI jI) => [k [le1 le2]]. move: (xb _ _ le1) (xb _ _ le2); rewrite /ex4_function_f_fam !LgV// => ea eb. move: (arg2_sr le1); rewrite sr => kI. exact: (ex4_propb le1 le2 (ha _ kI) ea eb sd). pose f := Lg Nat (fun n => (Zo s (fun z => exists i, [/\ inc i I, z = ss i & domain (Vg x i) = n]))). have <- : unionb f = s. rewrite /f;set_extens t. by move/setUb_P; aw; move => [y yd]; rewrite LgV//; case/Zo_P. move => ts; apply/setUb_P; aw; move/funI_P:(ts) => [z zI zv]. move:(ha _ zI) => /Zo_P[/ex4_inF_hi[_ [nd _ _ _ _] _] _]. by exists (domain (Vg x z)) => //; rewrite LgV//; apply/Zo_P; split => //; exists z. rewrite/f; apply: countable_union; first by aw; apply: countable_Nat. rewrite /allf; aw => n nN; rewrite LgV//; set Sn := Zo _ _; apply: finite_is_countable. have: small_set Sn. move => i j /Zo_P [aS [u [uI -> da]]] /Zo_P [jS [v [vI -> db]]]. by apply: (hc _ _ uI vI); rewrite db. case/small_set_pr. move => ->; apply:emptyset_finite. move => [t ->]; apply:set1_finite. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)