proposition: Lemma prl_ne2_prop: (forall i, inc i (psI S) -> prl_ne1_condii' i) -> pr1_ne2_hyp3_plain -> prl_ne2_res_a.
proof: Proof. move => ha hb. pose intv i:= (Zo (psI S) (gle (psr S) i)). pose IIF i := intersectionf (intv i)(fun j=> Imf (Vg (psf S) (J i j))). have Hw i:inc i (psI S) -> nonempty (intv i). by move => iI; exists i; apply/Zo_P; split => //; apply: prl_prop1. move => i iI; set_extens t. case:(prl_can_fun_fp iI) => [fc sc tc]. move/(Imf_P fc); rewrite sc; move => [u ua ->]. apply/(setIf_P _ (Hw _ iI)) => [j /Zo_P [ji lij]]. case:(ps_function_f lij); aw => fij sij tij. apply/(Imf_P fij); rewrite sij (prl_proj_ev iI ua). move/(prl_limitP): ua => [qa qb qc qd]. by exists (Vg u j); [apply: qc |apply: qd ]. move => tinter. pose II j := (Vfi1 (Vg (psf S) (J i j)) t). have Ha k: gle (psr S) i k -> ( forall x, inc x (II k) <-> inc x (Vg (psE S) k) /\ t = Vf (Vg (psf S) (J i k)) x). move => lik x. move:(prl_prop4 lik) => [ff sf _]. rewrite - sf. by apply:iim_fun_set1_P. pose Bi j := Yo (gle (psr S) i j) (II j) (Vg (psE S) j). have tei: inc t (Vg (psE S) i). by move:(setIf_hi tinter (prl_ne2_int_i iI)); rewrite prl_ne2_im_of_id. have qa: forall j, inc j (psI S) -> inc (Bi j) (Vg FS_fam j). rewrite /Bi;move => j jI; Ytac h; last by apply: FS_whole. apply: (hb _ _ _ h tei). have qb: inc (Lg (psI S) Bi) (productb FS_fam). apply/setXb_P;split;aww; rewrite FS_domain => //. by move => j jI; rewrite LgV//; apply: qa. have qc j: inc j (psI S) -> nonempty (Vg (Lg (psI S) Bi) j). rewrite /Bi;move => jI; rewrite LgV//; Ytac lij; fprops. move/prl_ne2_intP: (lij) => jj; move:(setIf_hi tinter jj) => tt. move:(prl_prop4 lij) => [ff sf tf]. move /(Imf_P ff): tt => [u usf tv]. by exists u; apply/(iim_fun_set1_P _ ff). have sII k: gle (psr S) i k -> sub (II k) (Vg (psE S) k). by move => lik x /(Ha _ lik); case. have Bsigma: inc (Lg (psI S) Bi) prl_ne2_sigma. apply/Zo_P; split => //; split => // j k ljk. move:(prl_prop0 ljk) => [jI kI]. rewrite /Bi ! LgV// => u. move: (prl_prop4 ljk) => [fjk sjk tjk]. case: (p_or_not_p (gle (psr S) i j)) => lij; Ytac0. move: (proj33 (ps_preorder_r S) _ _ _ lij ljk) => lik; Ytac0. have hu: sub (II k) (source (Vg (psf S) (J j k))). by rewrite sjk; apply sII. move/(Vf_image_P fjk hu) => [v /(Ha _ lik) [ua ub] ->]. apply/(Ha _ lij); split; first by Wtac. by rewrite (prl_prop3 lij ljk). have hu: sub (Yo (gle (psr S) i k) (II k) (Vg (psE S) k)) (source (Vg (psf S) (J j k))). rewrite sjk;Ytac h; fprops. move /(Vf_image_P fjk hu) => [v va ->]; Wtac. move:prl_ne2_sigma_osr => [or osr]. rewrite - osr in Bsigma. move: (inductive_max_greater or (prl_ne2_sigma_inductive ha) Bsigma). move => [A Amax leBA]. move:(pr1_ne2_hyp3_weak_prop hb) => hb'. move: (prl_ne2_sigma_maximal_prop3 ha hb' Amax)=> [ra rb]. move/graph_on_P1: leBA=> [_ _ h]; move:(h _ iI). move:(prl_prop1 iI) => iir. rewrite (ra _ iI); set xx := union _ => /sub1setP. rewrite /Bi LgV//; Ytac0; move/(Ha _ iir) => [xe ->]. rewrite (ps_identity_f iI) (idV xe). move:(prl_can_fun_fp iI) => [ff sf tf]. apply/(Imf_P ff); rewrite sf; ex_tac. rewrite prl_proj_ev // LgV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)