proposition: Lemma uncountable_sub_Omega_prop E: sub E aleph1 -> ~ countable_set E -> exists x, [/\ x <o aleph1, limit_ordinal x & forall y, y <o x -> exists z, [/\ inc z E, y <o z & z <o x]].
proof: Proof. move => seO ucE. move: (aleph_lt_ltc olt_01); rewrite -/aleph1 aleph0E => clt01. move: (oclt clt01) => lto0o1. have oo1:= proj32_1 lto0o1. have ha: ordinal_ub E aleph1 by move => t /seO /(oltP oo1) /proj1. have hb: ordinal_set E by move => t /ha/proj31. move: (ord_ub_sup oo1 ha) => le1. have H x: x <o aleph1 <-> countable_ordinal x. apply: (iff_trans (oltP oo1 x)); rewrite Cantor_omega_pr3. exact:aleph_oneP. case: (equal_or_not (\osup E) aleph1) => eq1; last first. move/H: (conj le1 eq1) => /countable_succ /proj2 cs. have os := (proj31 le1). have hc: sub E (osucc (\osup E)). by move => t tE; apply/(oleP os); apply: (ord_sup_ub). by case: ucE; apply: (countable_sub hc). pose B x := Zo E (fun z => x <o z). have hc x: x <o aleph1 -> nonempty (B x). rewrite - eq1 => la; move: (olt_sup hb la) => [z za zb]; exists z. by apply: Zo_i => //; apply: seO. have hd x: ordinal_set (B x) by move => t /Zo_S/ hb. pose N x := intersection (B x). have Np x: x <o aleph1 -> inc (N x) E /\ x <o N x. by move => xa; move /Zo_P: (ordinal_setI (hc _ xa) (hd x)). have za: \0o <o aleph1 by move:(olt_ltT olt_0omega lto0o1). move: (induction_defined_pr N (N \0o)); set f:= induction_defined _ _. move =>[sf srjf f0 fs]; set A := target f. case:(srjf); rewrite sf => ff sjf. have sAE: sub A E. move => t /sjf [n nN ->]; move: n nN. apply: Nat_induction; first by rewrite f0; exact: (proj1 (Np _ za)). by move => n nN /seO /(oltP oo1) / Np/proj1; rewrite (fs _ nN). have osA: ordinal_set A by move => t /sAE/hb. have AP x: inc x A -> inc (N x) A /\ x <o N x. move => xA. move /(oltP oo1): (seO _ (sAE _ xA)) => /Np/proj2 lt1; split => //. move: (sjf _ xA) =>[n nN av]. by move:(fs _ nN); rewrite - av /A => <-; Wtac; rewrite sf; apply: NS_succ. have neA: nonempty A. by exists (Vf f \0c); rewrite /A; Wtac; rewrite sf; apply: NS0. have sas: ~ inc (union A) A. move => lsA; move: (AP _ lsA) => [qa qb]. case:(oleNgt (ord_sup_ub osA qa) qb). case: (ord_sup_inVlimit osA neA) => // lsA. have he: countable_set A. move: (image_smaller ff); rewrite (surjective_pr0 srjf); rewrite sf. by rewrite - aleph0_pr1; move/ countableP. have hf: alls A countable_ordinal. by move => t /sAE /seO /(oltP oo1) /H. move /H: (countable_ordinal_sup he hf) => lt2. exists (\osup A); split => // y ya. move:(olt_sup osA ya) =>[z zA ub]; exists z; split => //; first by apply: sAE. by split; [ apply:(ord_sup_ub osA zA) | move => bad; case: sas; rewrite - bad]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)