proposition: Lemma cont_fun_th2 (F: fterm2) b: ordinalp b -> (forall i x, i <o b -> x <o aleph1 -> ordinalp (F i x)) -> (forall i, i <o b -> ocontinuous_below (fun x => F i x) aleph1) -> (forall x, x <o aleph1 -> olimit (fun i => (F i x)) b (osucc x)) -> False.
proof: Proof. move => ob ha hb hc. pose B x := Zo b (fun y => forall i, y <=o i -> i <o b -> (F i x) = osucc x). pose Y x := intersection (B x). have hd x: x <o aleph1 -> nonempty (B x). move => xo; move:(hc x xo) => hcx. have ox := (proj31_1 xo). move/ (olimit_succ _ _ ox): hcx => [y ya yb]; exists y; apply: Zo_i => //. by apply/(oltP ob). have he x: ordinal_set (B x) by move => t /Zo_S; apply: Os_ordinal. have hf x: x <o aleph1 -> Y x <o b /\ (forall i, Y x <=o i -> i <o b -> F i x = osucc x). move => xo; move /Zo_P:(ordinal_setI (hd x xo) (he x)) => [ra rb]. by split => //; apply /(oltP ob). have hf1 x: x <o aleph1 -> Y x <o b by move /hf/proj1. move: (aleph_lt_ltc olt_01); rewrite -/aleph1 aleph0E => clt01. move: (oclt clt01) => lto0o1. pose E := fun_image (osucc omega0) Y. have ra1 t: inc t E -> t <o b. move => /funI_P [x /(oleP OS_omega) xa ->]. exact:(hf1 _ (ole_ltT xa lto0o1)). have ra: ordinal_ub E b by move => t /ra1/proj1. have osE: ordinal_set E by move => t /ra/proj31. set c := \osup E. have rb: c <=o b by apply: (ord_ub_sup ob ra). case: (equal_or_not c b) => sEb; last first. have hg x: x <=o omega0 -> F c x = osucc x. move => h; move: (ole_ltT h lto0o1) => h1. move: (hf _ h1) =>[qa qb]; apply: qb => //. by apply: (ord_sup_ub osE); apply: funI_i; apply /(oleP OS_omega). have loo:= omega_limit. move: (hb _ (conj rb sEb) _ loo lto0o1) => ct1. case:(non_cont_ex1 loo). have osb: (esame_below (F c) osucc omega0). exists \0o; first by apply: olt_0omega. by move => i ia /proj1 ib; apply: hg. move/(olim_exten _ osb): ct1; rewrite hg //; apply:(oleR OS_omega). have Eu i: i <o b -> exists2 j, inc j E & i <o j. rewrite - sEb => lt1; exact: (olt_sup osE lt1). pose Bb x := (Zo E (fun j => Y x <o j)). pose C x := intersection (Bb x). have hdb x: x <o aleph1 -> nonempty (Bb x). by move => /hf/proj1/Eu [j ja jb];exists j; apply:Zo_i. have heb x: ordinal_set (Bb x) by move => t /Zo_S; apply: osE. have hg x: x <o aleph1 -> [/\ C x <o b, inc (C x) E & forall i, C x <=o i -> i <o b -> F i x = osucc x]. move => xo; move /Zo_P:(ordinal_setI (hdb x xo) (heb x)) => [sa sb]. split; [ by apply: ra1 | done | move => u ua ub]. apply: (proj2(hf _ xo) _ (oleT (proj1 sb) ua) ub). pose Ii i := Zo aleph1 (fun x => C x = i). pose If := (Lg E Ii). have csdif: countable_set (domain If). rewrite Lgd; apply: countable_fun_image. exact: (proj2 (countable_succ (countable_leomega (oleR OS_omega)))). have fgf: fgraph If by rewrite /If; fprops. case: (all_exists_dichot1 countable_set (range If)) => q. have ac: (allf If countable_set). by move => t tf; apply: q; apply: inc_V_range. move: (countable_union csdif ac). have ->: unionb If = aleph1. rewrite - setU_bf;set_extens t; first by move => /setUf_P [i iE /Zo_S]. move => ta; move/(oltP (proj32_1 lto0o1)): (ta). by move => /hg [_ cr _]; union_tac; apply:Zo_i. move/countableP. rewrite (card_card (proj32_1 clt01)); exact: (cltNge clt01). move: q => [Zi /(range_gP fgf)]; rewrite Lgd; move =>[p pE]; rewrite LgV//. move => Eiv icEi; clear If fgf csdif. have zia: sub Zi aleph1 by rewrite Eiv; apply: Zo_S. move:(uncountable_sub_Omega_prop zia icEi) => [x [xo lx xp]]. move: (hf x xo) =>[qa qb]. have pb: p <o b by apply: ra1. move: (omax_p1 (proj31_1 qa) (proj31_1 pb)); set n := omax _ _; move =>[qc qd]. have nb: n <o b by rewrite /n/omax/Gmax; Ytac h. move: (qb n qc nb) => Fnx. move: (hb n nb x lx xo); rewrite /ocontinuous_at Fnx. move/(olimit_succ _ _ (proj31_1 xo)) => [y lyx yp]. move: (xp _ lyx) =>[z [za zb zc]]. move:za; rewrite Eiv => /Zo_hi Cz. have ll: C z <=o n by ue. move: (proj33 (hg _ (olt_ltT zc xo)) n ll nb). rewrite (yp z (proj1 zb) zc); move: zc => [[oz ox _] /nesym ezx]. by move/(osucc_inj ox oz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)