proposition: Lemma ex5_result: nonempty (projective_limit ex5_S').
proof: Proof. suff: exists2 x, ex5_coherent2 x & domain x = psI S. move => [x [[pa _ pc] _ pd] dx]; rewrite dx in pc pd. rewrite prl_subsets_prop2; exists x; apply /setI2_P; split. apply/prl_limitP; split => //. move => i iI; exact:(ex5_G4 iI (pc _ iI)). move => i j leij. move:(prl_prop0 leij) => [iI jI]. move: (set2_1 i j) (set2_2 i j) => di dj. have fsd: finite_ne_sub (doubleton i j) (psI S). by split; [ apply:set2_finite | apply:set2_ne | apply:sub_set2]. move:(pd _ fsd) => [_ _] h; move:(h _ _ di dj leij); rewrite !LgV//. by apply/setXb_P; rewrite ex5_G2. set Y0:= sub_fgraphs (psI S) (unionb Gf). have Y0_p: forall x, ex5_coherent2 x -> inc x Y0. move => x [[ha1 ha2 ha3] hb _]; apply/sub_fgraphsP; exists (domain x) => //. apply/ gfunctions_P2; split => // t/(range_gP ha1) [i idx ->]. by apply/setUb_P; rewrite ex5_G2; exists i => // ; [apply: hb | apply: ha3]. set Y := Zo Y0 ex5_coherent2. have Y_p: forall x, inc x Y <-> ex5_coherent2 x. move => x; split;[ by case/Zo_P | move => h; apply:(Zo_i (Y0_p _ h) h)]. have aux: sub Y (\Po (union Y)). move => t tA; apply/setP_P => x xt; union_tac. have aux2:forall X, (forall x y, inc x X -> inc y X -> sub x y \/ sub y x) -> sub X Y -> inc (union X) Y. move => X ha hb; apply/Y_p. have hc: sub (domain (union X)) (psI S). move=> t /funI_P [z /setU_P [y zy /hb /Y_p yX] ->]. move: yX => [_ dx _]; apply:dx; apply/funI_P; ex_tac. have hd: sgraph (union X). move => t /setU_P [y ty /hb /Y_p [[ra _ _ ] _ _]]; exact: (proj1 ra _ ty). have he: fgraph (union X). split => // a b /setU_P [y ay yX] /setU_P [y' by' yX'] sp. move/hb:(yX) => /Y_p [[ra _ _ ] _ _];move/hb:(yX') => /Y_p [[rb _ _ ] _ _]. case:(ha _ _ yX yX') => syy. by move:(proj2 rb _ _ (syy _ ay) by' sp). by move:(proj2 ra _ _ ay (syy _ by') sp). have Hb z t: inc z t -> inc t X -> Vg (union X) (P z) = Vg t (P z). move => zt tX. have tU: sub t (union X) by move => i it; apply/setU_P; exists t. rewrite -(restr_to_domain he tU); rewrite LgV//; apply/funI_P; ex_tac. have hf i: inc i (domain (union X)) -> inc (Vg (union X) i) (Vg Gf i). move => /funI_P [z /setU_P [t zt tX] ->]; rewrite (Hb _ _ zt tX). move/hb:(tX) => /Y_p [[_ _ rc ] _ _]; apply: rc; apply/funI_P; ex_tac. have hg:ex5_prodG (domain (union X)) (union X) by []. split => // K [fsk nek sk]. have [t ta tb]: exists2 t, inc t X & sub K (domain t). pose A K := sub K (domain (union X)). pose B K := exists2 t, inc t X & sub K (domain t). have hi a: A (singleton a) -> B (singleton a). rewrite /A/B=> hh. move:(hh _ (set1_1 a)) => /funI_P [z /setU_P [y zy yx] ->]; ex_tac. move => t/set1_P ->; apply/funI_P; ex_tac. apply:(finite_set_induction2 (A:= A) (B := B) hi _ fsk nek sk). move => a b hu ane hv. have hw: A a by move => t ta; apply: hv; fprops. move:(hu ane hw) => [t1 t1X t1a]. have: inc b (domain (union X)) by apply:hv; fprops. move => /funI_P [z/setU_P [t2 zt2 t2X] bv]. have t2b: inc b (domain t2) by apply/funI_P; ex_tac. case: (ha _ _ t1X t2X) => /domain_S t1t2. exists t2 => // t/setU1_P; case => hq;[ by apply:t1t2; apply: t1a| ue]. exists t1 => // t/setU1_P; case => hq;[ by apply: t1a | apply:t1t2; ue]. have ->: (restr (union X) K) = restr t K. have tU: sub t (union X) by move => i it; apply/setU_P; exists t. by rewrite -(restr_to_domain he tU); rewrite double_restr. by move/hb:(ta) => /Y_p [_ tra rb]; apply: rb. move: (setP_maximal aux aux2) => [x []]. rewrite (proj2 (sub_osr Y)) => /Y_p co2 xmax. case: (equal_or_not (domain x) (psI S)) => dx; first by exists x. have /setC_ne [j /setC_P jp]: ssub(domain x)(psI S) by split => //; exact: (proj32 co2). have [x' x'p]: (exists x' : Set, ex5_extend_prop x j x'). case: (emptyset_dichot (domain x)) => xe. apply:(ex5_res2 co2 (proj1 jp) xe). exact: (ex5_res5 co2 jp xe). have: gle (sub_order Y) x ((ex5_extend x j x')). apply/sub_gleP; split; (try apply/Y_p => //); rewrite /ex5_extend; fprops. move/xmax => /(f_equal domain). rewrite /ex5_extend domain_setU1 => eqb. case: (proj2 jp); rewrite - eqb; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)