Assume Hsc: second_countable_space Sorgenfrey_line Sorgenfrey_topology.
We will prove False.
We prove the intermediate claim HexB: ∃B : set, basis_on Sorgenfrey_line B ∧ countable_set B ∧ basis_generates Sorgenfrey_line B Sorgenfrey_topology.
An exact proof term for the current goal is (andER (topology_on Sorgenfrey_line Sorgenfrey_topology) (∃B : set, basis_on Sorgenfrey_line B ∧ countable_set B ∧ basis_generates Sorgenfrey_line B Sorgenfrey_topology) Hsc).
Apply HexB to the current goal.
Let B be given.
Assume HBpair.
We prove the intermediate claim HBasisCount: basis_on Sorgenfrey_line B ∧ countable_set B.
An exact proof term for the current goal is (andEL (basis_on Sorgenfrey_line B ∧ countable_set B) (basis_generates Sorgenfrey_line B Sorgenfrey_topology) HBpair).
We prove the intermediate claim HBasis: basis_on Sorgenfrey_line B.
An exact proof term for the current goal is (andEL (basis_on Sorgenfrey_line B) (countable_set B) HBasisCount).
We prove the intermediate claim HBcount: countable_set B.
An exact proof term for the current goal is (andER (basis_on Sorgenfrey_line B) (countable_set B) HBasisCount).
We prove the intermediate claim HBgener: basis_generates Sorgenfrey_line B Sorgenfrey_topology.
An exact proof term for the current goal is (andER (basis_on Sorgenfrey_line B ∧ countable_set B) (basis_generates Sorgenfrey_line B Sorgenfrey_topology) HBpair).
We prove the intermediate claim HTxeq: generated_topology Sorgenfrey_line B = Sorgenfrey_topology.
An exact proof term for the current goal is (andER (basis_on Sorgenfrey_line B) (generated_topology Sorgenfrey_line B = Sorgenfrey_topology) HBgener).
Set pick to be the term (λx : set ⇒ Eps_i (λb : set ⇒ b ∈ B ∧ x ∈ b ∧ b ⊆ halfopen_interval_left x (add_SNo x 1))).
We prove the intermediate claim HpickP: ∀x : set, x ∈ Sorgenfrey_line → (λb : set ⇒ b ∈ B ∧ x ∈ b ∧ b ⊆ halfopen_interval_left x (add_SNo x 1)) (pick x).
Let x be given.
Assume HxX: x ∈ Sorgenfrey_line.
We will prove (λb : set ⇒ b ∈ B ∧ x ∈ b ∧ b ⊆ halfopen_interval_left x (add_SNo x 1)) (pick x).
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is HxX.
We prove the intermediate claim Hx1R: add_SNo x 1 ∈ R.
An exact proof term for the current goal is (real_add_SNo x HxR 1 real_1).
Set U to be the term halfopen_interval_left x (add_SNo x 1).
We prove the intermediate claim HUDef: U = halfopen_interval_left x (add_SNo x 1).
Use reflexivity.
We prove the intermediate claim HUopen: U ∈ Sorgenfrey_topology.
An exact proof term for the current goal is (halfopen_interval_left_in_R_lower_limit_topology x (add_SNo x 1) HxR Hx1R).
We prove the intermediate claim HUgen: U ∈ generated_topology Sorgenfrey_line B.
rewrite the current goal using HTxeq (from left to right).
An exact proof term for the current goal is HUopen.
We prove the intermediate claim HUbasis: ∀z ∈ U, ∃b ∈ B, z ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 Sorgenfrey_line) (λU0 : set ⇒ ∀z0 ∈ U0, ∃b0 ∈ B, z0 ∈ b0 ∧ b0 ⊆ U0) U HUgen).
We prove the intermediate claim HxU: x ∈ U.
rewrite the current goal using HUDef (from left to right).
We prove the intermediate claim HUeq: halfopen_interval_left x (add_SNo x 1) = {z ∈ R|¬ (Rlt z x) ∧ Rlt z (add_SNo x 1)}.
Use reflexivity.
rewrite the current goal using HUeq (from left to right).
Apply (SepI R (λz : set ⇒ ¬ (Rlt z x) ∧ Rlt z (add_SNo x 1)) x HxR) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (not_Rlt_refl x HxR).
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
We prove the intermediate claim Htmp: add_SNo x 0 < add_SNo x 1.
An exact proof term for the current goal is (add_SNo_Lt2 x 0 1 HxS SNo_0 SNo_1 SNoLt_0_1).
We prove the intermediate claim Hlt: x < add_SNo x 1.
We will prove x < add_SNo x 1.
rewrite the current goal using (add_SNo_0R x HxS) (from right to left) at position 1.
An exact proof term for the current goal is Htmp.
An exact proof term for the current goal is (RltI x (add_SNo x 1) HxR Hx1R Hlt).
We prove the intermediate claim Hexb: ∃b ∈ B, x ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (HUbasis x HxU).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is (andEL (b ∈ B) (x ∈ b ∧ b ⊆ U) Hbpair).
We prove the intermediate claim Hbprop: x ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (andER (b ∈ B) (x ∈ b ∧ b ⊆ U) Hbpair).
We prove the intermediate claim Hxb: x ∈ b.
An exact proof term for the current goal is (andEL (x ∈ b) (b ⊆ U) Hbprop).
We prove the intermediate claim Hbsub: b ⊆ U.
An exact proof term for the current goal is (andER (x ∈ b) (b ⊆ U) Hbprop).
We prove the intermediate claim Hwit0: b ∈ B ∧ x ∈ b ∧ b ⊆ halfopen_interval_left x (add_SNo x 1).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HbB.
An exact proof term for the current goal is Hxb.
rewrite the current goal using HUDef (from right to left).
An exact proof term for the current goal is Hbsub.
An exact proof term for the current goal is (Eps_i_ax (λb0 : set ⇒ b0 ∈ B ∧ x ∈ b0 ∧ b0 ⊆ halfopen_interval_left x (add_SNo x 1)) b Hwit0).
We prove the intermediate claim HinjRB: inj R B pick.
We prove the intermediate claim H1: ∀x ∈ R, pick x ∈ B.
Let x be given.
Assume HxR: x ∈ R.
We will prove pick x ∈ B.
We prove the intermediate claim Hp: (λb : set ⇒ b ∈ B ∧ x ∈ b ∧ b ⊆ halfopen_interval_left x (add_SNo x 1)) (pick x).
An exact proof term for the current goal is (HpickP x HxR).
Apply Hp to the current goal.
Assume Hcore Hsub.
Apply Hcore to the current goal.
Assume HpB HxIn.
An exact proof term for the current goal is HpB.
We prove the intermediate claim H2: ∀x0 x1 ∈ R, pick x0 = pick x1 → x0 = x1.
Let x0 be given.
Assume Hx0R: x0 ∈ R.
Let x1 be given.
Assume Hx1R: x1 ∈ R.
Assume Heq: pick x0 = pick x1.
We will prove x0 = x1.
We prove the intermediate claim Hp0: (λb : set ⇒ b ∈ B ∧ x0 ∈ b ∧ b ⊆ halfopen_interval_left x0 (add_SNo x0 1)) (pick x0).
An exact proof term for the current goal is (HpickP x0 Hx0R).
We prove the intermediate claim Hp1: (λb : set ⇒ b ∈ B ∧ x1 ∈ b ∧ b ⊆ halfopen_interval_left x1 (add_SNo x1 1)) (pick x1).
An exact proof term for the current goal is (HpickP x1 Hx1R).
We prove the intermediate claim Hx0in0: x0 ∈ pick x0.
Apply Hp0 to the current goal.
Assume Hcore0 Hsub0.
Apply Hcore0 to the current goal.
Assume Hp0B Hx0in.
An exact proof term for the current goal is Hx0in.
We prove the intermediate claim Hsub1: pick x1 ⊆ halfopen_interval_left x1 (add_SNo x1 1).
Apply Hp1 to the current goal.
Assume Hcore1 Hsub1.
An exact proof term for the current goal is Hsub1.
We prove the intermediate claim Hx0in1: x0 ∈ pick x1.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hx0in0.
We prove the intermediate claim Hx0U1: x0 ∈ halfopen_interval_left x1 (add_SNo x1 1).
An exact proof term for the current goal is (Hsub1 x0 Hx0in1).
We prove the intermediate claim HU1prop: ¬ (Rlt x0 x1) ∧ Rlt x0 (add_SNo x1 1).
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z x1) ∧ Rlt z (add_SNo x1 1)) x0 Hx0U1).
We prove the intermediate claim Hnlt01: ¬ (Rlt x0 x1).
An exact proof term for the current goal is (andEL (¬ (Rlt x0 x1)) (Rlt x0 (add_SNo x1 1)) HU1prop).
We prove the intermediate claim Hx0S: SNo x0.
An exact proof term for the current goal is (real_SNo x0 Hx0R).
We prove the intermediate claim Hx1S: SNo x1.
An exact proof term for the current goal is (real_SNo x1 Hx1R).
Apply (SNoLt_trichotomy_or_impred x0 x1 Hx0S Hx1S (x0 = x1)) to the current goal.
Assume Hlt: x0 < x1.
We will prove x0 = x1.
We prove the intermediate claim H01: Rlt x0 x1.
An exact proof term for the current goal is (RltI x0 x1 Hx0R Hx1R Hlt).
An exact proof term for the current goal is (FalseE (Hnlt01 H01) (x0 = x1)).
Assume Heq01: x0 = x1.
An exact proof term for the current goal is Heq01.
Assume Hlt: x1 < x0.
We will prove x0 = x1.
We prove the intermediate claim Hx1in1: x1 ∈ pick x1.
Apply Hp1 to the current goal.
Assume Hcore1 Hsub1.
Apply Hcore1 to the current goal.
Assume Hp1B Hx1in.
An exact proof term for the current goal is Hx1in.
We prove the intermediate claim Hsub0: pick x0 ⊆ halfopen_interval_left x0 (add_SNo x0 1).
Apply Hp0 to the current goal.
Assume Hcore0 Hsub0.
An exact proof term for the current goal is Hsub0.
We prove the intermediate claim Hx1in0: x1 ∈ pick x0.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is Hx1in1.
We prove the intermediate claim Hx1U0: x1 ∈ halfopen_interval_left x0 (add_SNo x0 1).
An exact proof term for the current goal is (Hsub0 x1 Hx1in0).
We prove the intermediate claim HU0prop: ¬ (Rlt x1 x0) ∧ Rlt x1 (add_SNo x0 1).
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z x0) ∧ Rlt z (add_SNo x0 1)) x1 Hx1U0).
We prove the intermediate claim Hnlt10: ¬ (Rlt x1 x0).
An exact proof term for the current goal is (andEL (¬ (Rlt x1 x0)) (Rlt x1 (add_SNo x0 1)) HU0prop).
We prove the intermediate claim H10: Rlt x1 x0.
An exact proof term for the current goal is (RltI x1 x0 Hx1R Hx0R Hlt).
An exact proof term for the current goal is (FalseE (Hnlt10 H10) (x0 = x1)).
An exact proof term for the current goal is (injI R B pick H1 H2).
We prove the intermediate claim HinjRBp: atleastp R B.
We will prove ∃f : set → set, inj R B f.
We use pick to witness the existential quantifier.
An exact proof term for the current goal is HinjRB.
We prove the intermediate claim HcountB: atleastp B ω.
An exact proof term for the current goal is HBcount.
We prove the intermediate claim HcountR: atleastp R ω.
An exact proof term for the current goal is (atleastp_tra R B ω HinjRBp HcountB).
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
We prove the intermediate claim Hcount_real: atleastp real ω.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HcountR.
An exact proof term for the current goal is (form100_22_real_uncountable_atleastp Hcount_real).
∎