proposition: Lemma closed_cofinal_inter C S (E := cnext C) (T:= intersectionb S): infinite_c C -> fgraph S -> ordinalp (domain S) -> cardinal (domain S) <=c C -> nonempty (domain S) -> (forall i, inc i (domain S) -> iclosed_set (Vg S i)) -> (forall i, inc i (domain S) -> ord_cofinal (Vg S i) E) -> (forall i j, i<o j -> inc i (domain S) -> inc j (domain S) -> sub (Vg S j) (Vg S i)) -> iclosed_set T /\ ord_cofinal T E.
proof: Proof. move => ic fgs ods cds /nonemptyP neds h1 h2 h4. move: (cnext_pr1 (proj1 ic)) => [sa sb sc]. have pa:=(olt_i (ord_ne0_pos ods neds)). have h3: (forall i, inc i (domain S) -> sub (Vg S i) E) by move => i /h2 []. have pb: sub T E by move => x h; move:(setIb_hi h pa); apply: h3. move: (infinite_card_limit2 (cle_inf_inf ic (proj1 sb))) => hy. move: (hy) => [oe _ _]. have ucc:union (cnext C) = E by rewrite - [union _] (limit_nonsucc hy). have pc: forall i, inc i (domain S) -> \osup (Vg S i) = E. move => i ids; move /(ord_cofinal_p2 hy (h3 _ ids)): (h2 _ ids). by rewrite ucc. have ose: ordinal_set E by move => t /(Os_ordinal oe). have neS: nonempty S by apply/domain_set0P; exists \0c. have pd: ord_cofinal T E. split => // x xe. pose yipp i y := [/\ inc y (Vg S i), x <=o y & forall z, inc z (Vg S i) -> x <=o z -> y <=o z]. pose yis i := Zo (Vg S i) (yipp i). pose yi i := intersection (yis i). have yip:forall i, inc i (domain S) -> yipp i (yi i). move => i ids; suff: inc (yi i) (yis i) by move/Zo_hi. move: (pc _ ids) => h. have xe1 : x <o \osup (Vg S i) by rewrite h; move/(oltP oe): xe. have osi: ordinal_set (Vg S i) by move => t /(h3 _ ids) /ose. apply:ordinal_setI; last by move => t /Zo_P [/osi]. move: (olt_sup osi xe1) => [z za [zb _]]. pose p z := inc z (Vg S i) /\ x <=o z. have pz: p z by split. have oz:= proj32 zb. move: (least_ordinal4 oz pz) => [ta [tb tc] td]. have ok: (yipp i (least_ordinal p z)). by split => // t te tf; move:(proj32 tf)=> ot; apply: td. by exists (least_ordinal p z); apply:Zo_i. have yi1: forall i j, inc i (domain S) -> inc j (domain S) -> i <o j -> inc (yi j) (Vg S i). move => i j ids jds ij; apply: (h4 _ _ ij ids jds). by case:(yip _ jds). have yi2: forall i j, inc i (domain S) -> inc j (domain S) -> i <o j -> (yi i) <=o (yi j). move => i j ids jds ij; move: (yi1 _ _ ids jds ij) => h. move: (yip _ ids) (yip _ jds) => [_ _ uc] [ _ ub _]; apply: uc => //. set F := fun_image (domain S) yi. have cf: cardinal F <=c C. exact:cleT (fun_image_smaller (domain S) yi) cds. have fe: sub F E. move => t /funI_P [z zdf ->]; move /yip:(zdf) => [ua ub _]. by apply: (h3 _ zdf). have osf: ordinal_set F by move => t /fe /ose. move: (cnext_sup ic cf fe); rewrite -/E => pd. have pe: x <=o (union F). move:(yip _ pa) => [_ ua _]; apply: (oleT ua); apply: ord_sup_ub => //. apply /funI_P; ex_tac. exists (\osup F) => //; apply/setIb_P => //. move => i ids. set G := fun_image (Zo (domain S) (fun z => i <=o z)) yi. have oi:= (Os_ordinal ods ids). have pf:inc i (Zo (domain S) [eta ordinal_le i]). apply/Zo_P; split => //; exact: (oleR oi). have eq1: \osup G = \osup F. apply:ord_sup_1cofinal => //; split. move => t /funI_P [z /Zo_P [ha _] ->]; apply/funI_P; ex_tac. move => a /funI_P [z za ->]. have oz:= (Os_ordinal ods za). case (oleT_el oi oz) => h5. exists (yi z); first by apply/funI_P; exists z => //; apply/Zo_P => //. by move: (yip _ za) => [_ /proj32 /oleR h6 _]. by exists (yi i); [ apply/funI_P; exists i | apply:yi2 ]. have g1: sub G (Vg S i). move => t /funI_P [j /Zo_P [ja jb] ->]; case (equal_or_not i j) => ij. by rewrite ij; move: (yip _ ja) => [h6 _ _]. apply:yi1 => //. have neg: nonempty G by exists (yi i); apply/funI_P; exists i. move:(h1 _ ids) => [sd se]; move: (se _ g1 neg); rewrite eq1. case => //;move: (pc _ ids) => -> h6. by case: (ordinal_irreflexive oe); move: pd; rewrite h6. split => //. have pe: \osup T = E by move /(ord_cofinal_p2 hy pb): pd ->. split; first by move => x /pb /(cnextP (proj1 ic)) []. move => F FT neF; rewrite pe;set x := (\osup F). case (equal_or_not x E) => xe; [by left | right ]. apply/setIb_P => // i ids; move:(h1 _ ids) => [_ h5]. have h6: sub F (Vg S i) by move => t /FT ts; exact :(setIb_hi ts ids). move: (h5 _ h6 neF); rewrite (pc _ ids); rewrite - /x; case => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)