proposition: Lemma Exercise6_33x (T0 := fun z => E6_33_choose (target z)) (T := Imf (transfinite_defined (ole_on N) T0)): [/\ sub T N, cardinal T = c & forall u v, inc u T -> inc v T -> u <> v -> Vf X u \cap Vf X v = E6_33_Q].
proof: Proof. move: Exercise6_33t =>[pa pb _ _]. move: Exercise6_33q => [_ _ _ pc _]. have pd := sub_trans pb pc. have oc:=(proj1 (proj1 Exercise6_33c)). have pe: ordinal_set N by move => t/pd /(Os_ordinal oc). move: (wordering_ole_pr pe). set r := (ole_on N); move =>[wor sr]. case: (transfinite_defined_pr T0 wor); set f := transfinite_defined _ _. rewrite sr; move => sjf sf fprop. pose fr x :=(restriction1 f (segment r x)). have axf x: inc x N -> sub (segment r x) (source f). move => xn; rewrite sf - sr; apply: sub_segment. have ff: function f by fct_tac. have frs x: inc x N -> surjection (fr x). move => xN; apply: (restriction1_fs ff (axf _ xN)). have fri x: inc x N -> Imf (fr x) = target (fr x). by move => /frs xn; apply: surjective_pr0. have sfr x: inc x N -> source (fr x) = segment r x. by move => xN; move: (proj32 (restriction1_prop ff (axf _ xN))). have ffr x: inc x N -> function (fr x) by move/frs/proj1. have frsi x: inc x N -> cardinal (target (fr x)) <c c. move => xN; rewrite - (fri _ xN). move: (ffr _ xN) (sfr _ xN) => fra frb. move: (image_smaller fra) => q; apply: (cle_ltT q). rewrite frb. have: sub (segment r x) x. move => t/segmentP [ /graph_on_P1/proj33 qa qb]. by apply/(oltP (proj32 qa)). move/sub_smaller => q';apply: (cle_ltT q'). apply:(colt1 (proj1 Exercise6_33c) (pd _ xN)). pose pr x := sub (target (fr x)) N /\ cardinal (target (fr x)) <c c. have prp x: inc x N -> pr x -> inc (Vf f x) N. move => xN [qa qb]. move /setC_P: (proj1 (Exercise6_33w qa qb)) => /proj1. by rewrite (fprop _ xN). set U := Zo N (fun x => ~ pr x). case: (emptyset_dichot U) => Ue; last first. have sU: sub U (substrate r) by rewrite sr; apply: Zo_S. move: (worder_prop wor sU Ue) =>[x /Zo_P [xN npx] etc]. case: npx; split; last by apply: frsi. move: (ffr _ xN) (sfr _ xN) => qa qb. rewrite - (fri _ xN) => t /(Imf_P qa). move => [u us ->]; rewrite qb in us. rewrite (restriction1_V ff (axf _ xN) us). have lux: glt r u x by apply/segmentP. have uN: inc u N by move: (arg1_sr (proj1 lux)); rewrite sr. apply: (prp u uN); split; last by apply: frsi. case: (inc_or_not u U) => uU. case: (not_le_gt (proj1 wor) (etc u uU) lux). case: (p_or_not_p (pr u)) => prf; first by case: prf. case: uU; apply: Zo_i => //. have prs x: inc x N -> pr x. by move => xN;ex_middle bad; empty_tac1 x; apply:Zo_i. have prq x: inc x N -> E6_33_res_prop (target (fr x)) (Vf f x). move => xN; move: (prs _ xN) => [qa qb]. move: (Exercise6_33w qa qb). by rewrite fprop. have finj: injection f. split => // u v; rewrite sf => uN vN sv. move: (proj2 (worder_total wor)); rewrite sr => h. ex_middle ne. wlog: u v uN vN ne sv /(gle r u v). move => H; case: (h u v uN vN) => le1; first by apply:H. by symmetry; apply: H => //; apply:nesym. move => luv. move: (prq _ vN) =>[/setC_P [ea eb] _]; case: eb. have usv: inc u (segment r v) by apply/segmentP. rewrite - (fri _ vN); apply/(Imf_P (ffr _ vN)). rewrite (sfr _ vN); ex_tac. by rewrite (restriction1_V ff (axf _ vN) usv) sv. have imf x: inc x N -> inc (Vf f x) N. by move => xN; case/setC_P: (proj1 (prq _ xN)). have cp1 u v t: glt r u v -> inc t (Vf X (Vf f u)) -> inc t (Vf X (Vf f v)) -> inc t E6_33_Q. move => lt1 tt ttv. move: (arg1_sr (proj1 lt1)) (arg2_sr (proj1 lt1)); rewrite sr => uB vN. have usc: inc u (segment r v) by apply/segmentP. have qa: inc (Vf f u) (target (fr v)). rewrite -(fri _ vN); apply/(Imf_P (ffr _ vN)); exists u=> //. by rewrite (sfr _ vN). by rewrite (restriction1_V ff (axf _ vN) usc). move: (proj2 (prq _ vN) _ _ qa tt) => lta. move: (Exercise6_33t) =>[_ NN0 /functionsP [fz sz rz] zv]. move: Exercise6_33q =>[qpa qpb qbc N0c _]. have vN0: inc (Vf f v) N0 by apply: NN0; apply: imf. move: (qpa _ vN0) =>[vc iar _]. move: (Exercise6_33j vc) =>[ya yb yc]. pose p := (Vf (inverse_fun (y (Vf f v))) t). move: (ya) =>[_ _ /proj31 bp mor]. have ps: inc p (rho (Vf f v)). by rewrite /p -yb; apply/inverse_Vis => //; rewrite yc. have tp: t = Vf (y (Vf f v)) p by rewrite inverse_V //; ue. move: (lta); rewrite tp=> -[le ne]. rewrite yb in iar. move/ (Exercise6_33k vc ps iar): le; case/ ole_eqVlt => lpa. by case: ne; rewrite lpa. apply/(Imf_P fz); rewrite sz. move: (olt_i lpa) => ipa; exists p => //. rewrite - (zv _ (imf _ vN)). by rewrite (proj33 (Exercise6_33r vN0) _ ipa). have Ra: sub (Imf f) N. by move => t /(Imf_P (proj1 finj)) [ u usf ->]; apply: imf; rewrite - sf. have Rb: cardinal (Imf f) = c. by rewrite (cardinal_range finj) sf. have Rc u v: inc u (Imf f) -> inc v (Imf f) -> u <> v -> (Vf X u) \cap (Vf X v) = E6_33_Q. move/(Imf_P ff) =>[i isf ->] /(Imf_P ff) [j jsf ->]. rewrite sf in isf jsf. move: (proj2 (worder_total wor)); rewrite sr => h. wlog: i j isf jsf / gle r i j. move => H; case: (h i j isf jsf) => le1; first by apply:H. by move/nesym => neq; rewrite setI2_C; apply: H. move => leij nej. have lij: glt r i j by split => // bad; case: nej; rewrite bad. set_extens t. by move/setI2_P => [tf1 tf2]; move: (cp1 i j t lij tf1 tf2). move => tq; apply/setI2_P; split. by apply: (Exercise6_33u (imf _ isf)). by apply: (Exercise6_33u (imf _ jsf)). done. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)