proposition: Lemma prl_ne2_sigma_maximal_prop3 A (xi := fun i => union (Vg A i)): (forall i, inc i (psI S) -> prl_ne1_condii' i) -> pr1_ne2_hyp3_weak -> maximal prl_ne2_sigma_order A -> (forall i, inc i (psI S) -> (Vg A i) = singleton (xi i)) /\ inc (Lg (psI S) xi) (projective_limit S).
proof: Proof. move => ha hb hc. move:(prl_ne2_sigma_maximal_prop2 ha hb hc) => si. have xip: forall i, inc i (psI S) -> (Vg A i) = singleton (xi i). by move => i iI; rewrite /xi; move:(si _ iI) => [t ->]; rewrite setU_1. move:(prl_ne2_sigma_maximal_prop1 ha hc) => av. have xiE i: inc i (psI S) -> inc (xi i) (Vg (psE S) i). move => iI; apply/sub1setP;rewrite - (xip _ iI); apply/setP_P. move: (proj1 hc); rewrite (proj2 prl_ne2_sigma_osr) => /Zo_P [/setXb_P]. rewrite FS_domain; move => [_ _ h] _. by move: ((FS_range iI) _ (h _ iI)). have fij: forall i j, gle (psr S) i j -> xi i = Vf (Vg (psf S) (J i j)) (xi j). move => i j lij; move: (av _ _ lij). move: (prl_prop0 lij) => [iI jI]. rewrite (xip _ iI) (xip _ jI) => ea. move:(prl_prop4 lij) => [ff sf tf]. have hd:sub (singleton (xi j)) (source (Vg (psf S) (J i j))). by move => t /set1_P ->; rewrite sf; apply: xiE. by move:(set1_1 (xi i)); rewrite ea => /(Vf_image_P ff hd) [u /set1_P -> ub]. split => //; apply/prl_limitP; split. - fprops. - by aw. - by move => i ii; rewrite LgV//; apply: xiE. - move => i j lij; move: (prl_prop0 lij) => [iI jI]. by rewrite ! LgV//; apply: fij. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)