proposition: Lemma Exercise6_33v A: sub A N -> cardinal A <c c -> exists i, E6_33_res_prop A i.
proof: Proof. move=> sAN cA. have ic := Exercise6_33c. have cc := proj1 ic. move:Exercise6_33q =>[E33q1 E33q2 _ E33q4 _]. have sNc: sub N c. by apply: sub_trans E33q4; case: Exercise6_33t. set B := unionf A (Vf X). have lcBc: cardinal B <c c. pose f := Lg A (fun i => cardinal (Vf X i)). pose g := Lg A (fun i => b). have sd: domain f = domain g by rewrite /f /g; aw. have la x: inc x (domain f) -> Vg f x <=c Vg g x. rewrite /f /g; aw => xd; bw => //; apply: Exercise6_33d2. by apply: sNc; apply: sAN. move: (csum_increasing sd la). rewrite /g -/(csumb _ _) csum_of_same. move: (csum_pr1_bis A (Vf X)); rewrite -/B /f -/(csumb _ _) => lb lc. move: (cleT lb lc). rewrite - cprod2cr => le. exact: (cle_ltT le (cprod_inf5 Exercise6_33a4 cA ic)). have sbM: sub B M. by move => t/setUf_P [u uA etc]; apply: (Exercise6_33e (sNc _ (sAN u uA))). move: Exercise6_33h; simpl. set r := E6_33_r. set f := E6_33_x. move =>[orM [o1 o2 fbp _] iso]. move: fbp. rewrite (proj2 orM)ordinal_o_sr=> h. move: (inverse_bij_bp h) => [bif sif tif]. move:h =>[bf sf tf]. have ff: function f by fct_tac. have fif: function (inverse_fun f) by fct_tac. have sbM': sub B (source (inverse_fun f)) by ue. move: (cardinal_image sbM' (proj1 bif)). set C := Vfs (inverse_fun f) B => cc1. have sCc: sub C c by rewrite - tif; apply:fun_image_Starget1. have cc2: cardinal C <=c a ^c b by apply/Exercise6_33aP; ue. move: (cnext_sup Exercise6_33a cc2 sCc) => ra. pose D := N -s A. set D1 := fun_image D (fun t => Vf (y t) alpha). have cD: cardinal D = c. move: (proj41 (Exercise6_33t)) => r3. have r1: infinite_set N by apply/infinite_setP; rewrite r3. have r2: cardinal A <c cardinal N by rewrite r3. by move: (infinite_compl r1 r2); rewrite r3. have sdd: sub D N0. by move => t /setC_P [ta _]; apply: (proj42 (Exercise6_33t)). have cD1: cardinal D1 = c. rewrite - cD; apply: cardinal_fun_image. by move => u v uS vD; apply: E33q2; apply: sdd. have sdM: sub D1 M. move => u /funI_P [ t ta ->]. by move: (E33q1 _ (sdd _ ta)) =>[_ _ /Zo_S mc]. have sdM': sub D1 (source (inverse_fun f)) by ue. move: (cardinal_image sdM' (proj1 bif)). set D2 := Vfs (inverse_fun f) D1 => cc3. have sDc: sub D2 c by rewrite - tif; apply:fun_image_Starget1. have cc4: cardinal D2 = c by rewrite cc3. pose ma := osucc (union C). have mac: inc ma c by exact:(proj33 (infinite_card_limit2 Exercise6_33c) _ ra). have cic := (proj1 Exercise6_33c). move /cardinalP: (cic) =>[sa sb]. case: (all_exists_dichot1 (fun z => z <o ma) D2) => hu. move/(oltP sa): (mac) => /proj1/proj33/sub_smaller; case/cle_eqVlt => la1. by move: (sb _ mac); case/card_eqP. have: sub D2 ma by move =>t /hu /olt_i. by move/sub_smaller; rewrite cc4; case/cleNgt; rewrite - (card_card cic). move: hu =>[mb mbd bad]. case: (oleT_el (Os_ordinal sa mac) (Os_ordinal sa (sDc _ mbd))) => // la. have mbp i: inc i C -> i <o mb. move => oic. apply: olt_leT la; apply /oltSleP; apply: ord_sup_ub => //. by move => t /sCc /(Os_ordinal sa). pose mc := Vf f mb. have md1: inc mc D1. have s1: sub D1 (source (inverse_fun f)) by ue. rewrite /mc; move/(Vf_image_P fif s1): mbd => [u ud1 ->]. by rewrite inverse_V //; rewrite tf; apply: sdM. have m3s i: inc i B -> glt r i mc. move => iB. set j := Vf (inverse_fun f) i. have jC: inc j C by apply/(Vf_image_P fif sbM'); ex_tac. move: (mbp _ jC) =>[ta tb]. move: (sCc _ jC) (sDc _ mbd) => jc mcc. have: glt r (Vf f j) (Vf f mb). split; [by move/(iso j mb jc mcc): ta | dneg b2 ]. by rewrite - sf in jc mcc; move: (proj2 (proj1 bf) j mb jc mcc b2). by rewrite /j inverse_V //; ue. move/funI_P: md1 =>[i uA ee]; exists i; split => //. by move => n t qa qb; rewrite - ee; apply:m3s; apply/setUf_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)