proposition: Lemma BQ_iso4 (E := Zo (permutations BQ) (fun f => order_isomorphism f BQ_order BQ_order)): cardinal E = \2c ^c aleph0.
proof: Proof. have cq:= cardinal_Q. apply: cleA. have ibq: infinite_set BQ. apply /infinite_setP; rewrite cq; apply: CIS_aleph0. have /sub_smaller sa: sub E (permutations BQ) by apply: Zo_S. move: (cleT sa (Exercise6_5c ibq)). by rewrite card_setP - cpowcr cq. move:constants_v => [c0 [c1 c2]]. have ->: \2c ^c aleph0 = cardinal (functions Nat C2). rewrite c2 cpow_pr1 aleph0_pr1 cpowcl //. pose f_to_g f := induction_defined0 (fun n v => csucc ((Vf f n) +c v)) \0c. have ftN: forall f, inc f (functions Nat C2) -> forall n, natp n -> natp (Vf f n). move => f /functionsP [ff sf tf] n nN. suff: sub (target f) Nat by apply; Wtac; ue. rewrite tf => t /set2_P;case => ->; rewrite ? c0 ? c1 -/(natp _); fprops. have pa: forall f, let g := (f_to_g f) in inc f (functions Nat C2) -> [/\ function g, Vf g \0c = \0c, forall n, natp n -> Vf g (csucc n) = csucc (Vf f n +c Vf g n), forall n, natp n -> natp (Vf g n) & forall n, natp n -> (Vf g n) <c (Vf g (csucc n))]. move => f g H ;move:(ftN _ H) => fn. move:(induction_defined_pr0 (fun n v : Set => csucc (Vf f n +c v)) \0c). rewrite -/(f_to_g f) -/g; move => [sg [fg _] g0 gs]. have gn: forall n, natp n -> natp (Vf g n). apply: Nat_induction; first by rewrite g0; fprops. move => n nn h; rewrite (gs _ nn);apply:NS_succ; apply:NS_sum; fprops. have gi //:forall n, natp n -> Vf g n <c Vf g (csucc n). move => n nn; rewrite (gs _ nn). have aux: Vf g n <=c (Vf f n +c Vf g n). apply:csum_Mle0;exact: (CS_nat (gn _ nn)). apply: (cle_ltT aux); apply: cltS; apply:NS_sum; fprops. have inj1: forall f1 f2, inc f1 (functions Nat C2) -> inc f2 (functions Nat C2) -> (forall n, natp n -> Vf (f_to_g f1) n = Vf (f_to_g f2) n) -> f1 = f2. move => f1 f2 f1a f2a sg1g2. move:(pa _ f1a) (pa _ f2a)=> [qa qb qc qd qe] [ra rb rc rd re]. move: (ftN _ f1a) (ftN _ f2a) => Ha Hb. move/functionsP : f1a => [ff1 sf1 tf1]. move/functionsP : f2a => [ff2 sf2 tf2]. apply: function_exten => //; try ue; move => n; rewrite sf1 => nN. move:(rc _ nN) (qc _ nN); rewrite (sg1g2 _ (NS_succ nN)) (sg1g2 _ nN). have sa: cardinalp (Vf f2 n +c Vf (f_to_g f2) n)by fprops. have sb: cardinalp (Vf f1 n +c Vf (f_to_g f2) n)by fprops. move: (Ha _ nN)(Hb _ nN) => na nb. move => -> /(csucc_inj sa sb). by move/(csum_eq2r (rd _ nN) nb na). pose mif f := multiple_interpolation (fun z => (BQ_of_nat (Vf (f_to_g f) z))). have pb: forall f, let g := (mif f) in inc f (functions Nat C2) -> [/\ forall x, inc x BQp -> inc (g x) BQp, forall y, inc y BQp -> exists2 x : Set, inc x BQp & g x = y, forall n, natp n -> g (BQ_of_nat n) = BQ_of_nat (Vf (f_to_g f) n) & forall x y, inc x BQp -> x <q y -> g x <q g y]. move => f g ff; move:(pa _ ff) => [qa qb qc qd qe]. by apply:multiple_interpolation_prop. move: BQor_sr BQor_tor => sr tor; move: (proj1 tor) => orc. have pc: forall f, order_isomorphism f BQ_order BQ_order -> inc f E. move => f h; apply/Zo_P; split => //. move: h => [_ _ ]; rewrite sr; move => [ha hb hc] _. apply/Zo_P; split => //; apply/functionsP; split => //; fct_tac. pose f_to_A f z := Yo (inc z BQp) (mif f z) z. pose f_to_B f := Lf ( f_to_A f) BQ BQ. have pd:forall f, inc f (functions Nat C2) -> lf_axiom (f_to_A f) BQ BQ. move => f ff x xQ; rewrite /f_to_A; Ytac h => //. by move:(pb _ ff) => [ ha _ _ _]; move: (BQp_sBQ (ha _ h)). have pe: forall f, inc f (functions Nat C2) -> forall x y, ratp x -> ratp y -> x <q y -> f_to_A f x <q f_to_A f y. move => f fa x y xq yp lxy; rewrite /f_to_A. move:(pb _ fa) => [sa _ _ sb]. Ytac h1; Ytac h2. + by apply: sb. + case h2; apply/ qle0xP; move/ qle0xP: h1 => xp; move:(proj1 lxy) => lxy'. BQo_tac. + move / qle0xP:(sa _ h2) => ha; case/BQ_i0P:xq => // / qgt0xP hb; BQo_tac. + done. have pf: forall f, inc f (functions Nat C2) -> bijection (f_to_B f). move => f ff; move: (pd _ ff)(pe _ ff) => sa sb. move:(pb _ ff) => [_ sc _ _]. apply:lf_bijective => //. move => u v uq vq eq; case: (qleT_ell uq vq) => // cp. by case:(proj2 (sb _ _ uq vq cp)). by case:(proj2 (sb _ _ vq uq cp)). move => y yq; case:(inc_or_not y BQp) => yp. move:(sc _ yp) => [x xp h]; move: (BQp_sBQ xp) => xq; exists x => //. by rewrite /f_to_A; Ytac0. by exists y => //; rewrite /f_to_A; Ytac0. have ax: forall f, inc f (functions Nat C2) -> (inc (f_to_B f) E). rewrite /f_to_B;move => f fa; move: (pf _ fa) (pd _ fa) => pea pda. apply: pc;apply: total_order_isomorphism; aw; trivial. move => x y xq yq /=; rewrite !LfV//. move /BQle_P => lxy; apply/BQle_P; case: (equal_or_not x y) => eqxy. by rewrite eqxy; apply: qleR; apply:pda. exact: (proj1 (pe _ fa _ _ xq yq (conj lxy eqxy))). suff: injection (Lf f_to_B (functions Nat C2) E). by move/ inj_source_smaller; aw. apply: (lf_injective ax) => f1 f2 f1a f2a sf; apply: (inj1 _ _ f1a f2a). move:(pb _ f1a) (pb _ f2a) => [_ _ sa _] [_ _ sb _]. move => n nN. have cnp: inc (BQ_of_nat n) BQp by apply: QpS_of_nat. move:(BQp_sBQ cnp) => cnq. move: (pd _ f1a) (pd _ f2a) => ax1 ax2. move: (f_equal (fun z => (Vf z (BQ_of_nat n))) sf). rewrite /f_to_B {1} (LfV ax1 cnq)(LfV ax2 cnq) /f_to_A {1} (Y_true cnp). rewrite (Y_true cnp) (sa _ nN) (sb _ nN); apply: BQ_of_nat_injective. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)