Let X, Tx and A be given.
Assume Hsc: second_countable_space X Tx.
Assume HA: A ⊆ X.
Assume HuncA: ¬ countable A.
We will prove ¬ countable {x ∈ A|limit_point_of X Tx A x}.
Set L to be the term {x ∈ A|limit_point_of X Tx A x}.
Assume HcountL: countable L.
We will prove False.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (∃B : set, basis_on X B ∧ countable_set B ∧ basis_generates X B Tx) Hsc).
We prove the intermediate claim HexB: ∃B : set, basis_on X B ∧ countable_set B ∧ basis_generates X B Tx.
An exact proof term for the current goal is (andER (topology_on X Tx) (∃B : set, basis_on X B ∧ countable_set B ∧ basis_generates X B Tx) Hsc).
Set B to be the term Eps_i (λB0 : set ⇒ basis_on X B0 ∧ countable_set B0 ∧ basis_generates X B0 Tx).
We prove the intermediate claim HBspec: basis_on X B ∧ countable_set B ∧ basis_generates X B Tx.
An exact proof term for the current goal is (Eps_i_ex (λB0 : set ⇒ basis_on X B0 ∧ countable_set B0 ∧ basis_generates X B0 Tx) HexB).
We prove the intermediate claim HBleft: basis_on X B ∧ countable_set B.
An exact proof term for the current goal is (andEL (basis_on X B ∧ countable_set B) (basis_generates X B Tx) HBspec).
We prove the intermediate claim HBasis: basis_on X B.
An exact proof term for the current goal is (andEL (basis_on X B) (countable_set B) HBleft).
We prove the intermediate claim HBcountset: countable_set B.
An exact proof term for the current goal is (andER (basis_on X B) (countable_set B) HBleft).
We prove the intermediate claim HBgen: basis_generates X B Tx.
An exact proof term for the current goal is (andER (basis_on X B ∧ countable_set B) (basis_generates X B Tx) HBspec).
We prove the intermediate claim HGenEq: generated_topology X B = Tx.
An exact proof term for the current goal is (andER (basis_on X B) (generated_topology X B = Tx) HBgen).
Set I to be the term {x ∈ A|¬ limit_point_of X Tx A x}.
Set pick_iso to be the term λx0 : set ⇒ Eps_i (λb0 : set ⇒ b0 ∈ B ∧ x0 ∈ b0 ∧ b0 ∩ A = {x0}) of type set → set.
We prove the intermediate claim HexIso: ∀x : set, x ∈ I → ∃b0 : set, b0 ∈ B ∧ x ∈ b0 ∧ b0 ∩ A = {x}.
Let x be given.
Assume HxI: x ∈ I.
We will prove ∃b0 : set, b0 ∈ B ∧ x ∈ b0 ∧ b0 ∩ A = {x}.
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (SepE1 A (λx0 : set ⇒ ¬ limit_point_of X Tx A x0) x HxI).
We prove the intermediate claim HxnotLP: ¬ limit_point_of X Tx A x.
An exact proof term for the current goal is (SepE2 A (λx0 : set ⇒ ¬ limit_point_of X Tx A x0) x HxI).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HA x HxA).
We prove the intermediate claim HnotP: ¬ (∀U : set, U ∈ Tx → x ∈ U → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U).
Assume HP: ∀U : set, U ∈ Tx → x ∈ U → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U.
Apply HxnotLP to the current goal.
We will prove (topology_on X Tx ∧ x ∈ X) ∧ (∀U : set, U ∈ Tx → x ∈ U → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
An exact proof term for the current goal is HxX.
An exact proof term for the current goal is HP.
We prove the intermediate claim HexU: ∃U : set, ¬ (U ∈ Tx → x ∈ U → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U).
Apply (xm (∃U : set, ¬ (U ∈ Tx → x ∈ U → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U))) to the current goal.
Assume Hex: ∃U : set, ¬ (U ∈ Tx → x ∈ U → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U).
An exact proof term for the current goal is Hex.
Assume Hno: ¬ (∃U : set, ¬ (U ∈ Tx → x ∈ U → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U)).
Apply FalseE to the current goal.
We will prove False.
Apply HnotP to the current goal.
Let U be given.
We will prove U ∈ Tx → x ∈ U → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U.
Apply (xm (U ∈ Tx → x ∈ U → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U)) to the current goal.
Assume HUimp: U ∈ Tx → x ∈ U → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U.
An exact proof term for the current goal is HUimp.
Assume HnotHUimp: ¬ (U ∈ Tx → x ∈ U → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U).
Apply FalseE to the current goal.
We will prove False.
Apply Hno to the current goal.
We use U to witness the existential quantifier.
An exact proof term for the current goal is HnotHUimp.
Apply HexU to the current goal.
Let U be given.
Assume HnotImp: ¬ (U ∈ Tx → x ∈ U → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U).
We prove the intermediate claim HU: U ∈ Tx.
Apply (xm (U ∈ Tx)) to the current goal.
Assume HU0: U ∈ Tx.
An exact proof term for the current goal is HU0.
Assume HnotHU: U ∉ Tx.
Apply FalseE to the current goal.
We will prove False.
Apply HnotImp to the current goal.
Assume HU1: U ∈ Tx.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HnotHU HU1).
We prove the intermediate claim HxU: x ∈ U.
Apply (xm (x ∈ U)) to the current goal.
Assume HxU0: x ∈ U.
An exact proof term for the current goal is HxU0.
Assume HnotHxU: x ∉ U.
Apply FalseE to the current goal.
We will prove False.
Apply HnotImp to the current goal.
Assume HU1: U ∈ Tx.
Assume HxU1: x ∈ U.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HnotHxU HxU1).
We prove the intermediate claim HnoY: ¬ (∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U).
Assume Hexy: ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U.
Apply HnotImp to the current goal.
Assume HU1: U ∈ Tx.
Assume HxU1: x ∈ U.
An exact proof term for the current goal is Hexy.
We prove the intermediate claim HUcapAeq: U ∩ A = {x}.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ U ∩ A.
We will prove y ∈ {x}.
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (binintersectE1 U A y Hy).
We prove the intermediate claim HyA: y ∈ A.
An exact proof term for the current goal is (binintersectE2 U A y Hy).
Apply (xm (y = x)) to the current goal.
Assume Heq: y = x.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (SingI x).
Assume Hneq: y ≠ x.
Apply FalseE to the current goal.
We will prove False.
Apply HnoY to the current goal.
We use y to witness the existential quantifier.
We will prove y ∈ A ∧ y ≠ x ∧ y ∈ U.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HyA.
An exact proof term for the current goal is Hneq.
An exact proof term for the current goal is HyU.
Let y be given.
Assume Hy: y ∈ {x}.
We will prove y ∈ U ∩ A.
We prove the intermediate claim Heq: y = x.
An exact proof term for the current goal is (SingE x y Hy).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (binintersectI U A x HxU HxA).
We prove the intermediate claim HUgen: U ∈ generated_topology X B.
rewrite the current goal using HGenEq (from left to right).
An exact proof term for the current goal is HU.
We prove the intermediate claim HUprop: ∀y ∈ U, ∃b0 ∈ B, y ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀y0 : set, y0 ∈ U0 → ∃b0 ∈ B, y0 ∈ b0 ∧ b0 ⊆ U0) U HUgen).
We prove the intermediate claim Hexb: ∃b0 ∈ B, x ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (HUprop x HxU).
Set b0 to be the term Eps_i (λb : set ⇒ b ∈ B ∧ (x ∈ b ∧ b ⊆ U)).
We prove the intermediate claim Hb0spec: b0 ∈ B ∧ (x ∈ b0 ∧ b0 ⊆ U).
An exact proof term for the current goal is (Eps_i_ex (λb : set ⇒ b ∈ B ∧ (x ∈ b ∧ b ⊆ U)) Hexb).
We prove the intermediate claim Hb0B: b0 ∈ B.
An exact proof term for the current goal is (andEL (b0 ∈ B) (x ∈ b0 ∧ b0 ⊆ U) Hb0spec).
We prove the intermediate claim Hb0prop: x ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (andER (b0 ∈ B) (x ∈ b0 ∧ b0 ⊆ U) Hb0spec).
We prove the intermediate claim Hxb0: x ∈ b0.
An exact proof term for the current goal is (andEL (x ∈ b0) (b0 ⊆ U) Hb0prop).
We prove the intermediate claim Hb0subU: b0 ⊆ U.
An exact proof term for the current goal is (andER (x ∈ b0) (b0 ⊆ U) Hb0prop).
We use b0 to witness the existential quantifier.
We will prove b0 ∈ B ∧ x ∈ b0 ∧ b0 ∩ A = {x}.
We prove the intermediate claim Hb0pair2: b0 ∈ B ∧ x ∈ b0.
An exact proof term for the current goal is (andI (b0 ∈ B) (x ∈ b0) Hb0B Hxb0).
We prove the intermediate claim Hb0cap: b0 ∩ A = {x}.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ b0 ∩ A.
We will prove y ∈ {x}.
We prove the intermediate claim HyA: y ∈ A.
An exact proof term for the current goal is (binintersectE2 b0 A y Hy).
We prove the intermediate claim Hyb0: y ∈ b0.
An exact proof term for the current goal is (binintersectE1 b0 A y Hy).
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (Hb0subU y Hyb0).
We prove the intermediate claim HyUA: y ∈ U ∩ A.
An exact proof term for the current goal is (binintersectI U A y HyU HyA).
rewrite the current goal using HUcapAeq (from right to left).
An exact proof term for the current goal is HyUA.
Let y be given.
Assume Hy: y ∈ {x}.
We will prove y ∈ b0 ∩ A.
We prove the intermediate claim Heq: y = x.
An exact proof term for the current goal is (SingE x y Hy).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (binintersectI b0 A x Hxb0 HxA).
An exact proof term for the current goal is (andI (b0 ∈ B ∧ x ∈ b0) (b0 ∩ A = {x}) Hb0pair2 Hb0cap).
We prove the intermediate claim HinjIB: inj I B pick_iso.
We will prove (∀u ∈ I, pick_iso u ∈ B) ∧ (∀u ∈ I, ∀v ∈ I, pick_iso u = pick_iso v → u = v).
Apply andI to the current goal.
Let u be given.
Assume HuI: u ∈ I.
We will prove pick_iso u ∈ B.
We prove the intermediate claim Hexb: ∃b0 : set, b0 ∈ B ∧ u ∈ b0 ∧ b0 ∩ A = {u}.
An exact proof term for the current goal is (HexIso u HuI).
We prove the intermediate claim Hpick: pick_iso u ∈ B ∧ u ∈ pick_iso u ∧ pick_iso u ∩ A = {u}.
An exact proof term for the current goal is (Eps_i_ex (λb0 : set ⇒ b0 ∈ B ∧ u ∈ b0 ∧ b0 ∩ A = {u}) Hexb).
We prove the intermediate claim HpickL: pick_iso u ∈ B ∧ u ∈ pick_iso u.
An exact proof term for the current goal is (andEL (pick_iso u ∈ B ∧ u ∈ pick_iso u) (pick_iso u ∩ A = {u}) Hpick).
An exact proof term for the current goal is (andEL (pick_iso u ∈ B) (u ∈ pick_iso u) HpickL).
Let u be given.
Assume HuI: u ∈ I.
Let v be given.
Assume HvI: v ∈ I.
Assume Heq: pick_iso u = pick_iso v.
We will prove u = v.
We prove the intermediate claim Hexu: ∃b0 : set, b0 ∈ B ∧ u ∈ b0 ∧ b0 ∩ A = {u}.
An exact proof term for the current goal is (HexIso u HuI).
We prove the intermediate claim Hexv: ∃b0 : set, b0 ∈ B ∧ v ∈ b0 ∧ b0 ∩ A = {v}.
An exact proof term for the current goal is (HexIso v HvI).
We prove the intermediate claim Hpu: pick_iso u ∩ A = {u}.
We prove the intermediate claim Hpick: pick_iso u ∈ B ∧ u ∈ pick_iso u ∧ pick_iso u ∩ A = {u}.
An exact proof term for the current goal is (Eps_i_ex (λb0 : set ⇒ b0 ∈ B ∧ u ∈ b0 ∧ b0 ∩ A = {u}) Hexu).
An exact proof term for the current goal is (andER (pick_iso u ∈ B ∧ u ∈ pick_iso u) (pick_iso u ∩ A = {u}) Hpick).
We prove the intermediate claim Hpv: pick_iso v ∩ A = {v}.
We prove the intermediate claim Hpick: pick_iso v ∈ B ∧ v ∈ pick_iso v ∧ pick_iso v ∩ A = {v}.
An exact proof term for the current goal is (Eps_i_ex (λb0 : set ⇒ b0 ∈ B ∧ v ∈ b0 ∧ b0 ∩ A = {v}) Hexv).
An exact proof term for the current goal is (andER (pick_iso v ∈ B ∧ v ∈ pick_iso v) (pick_iso v ∩ A = {v}) Hpick).
We prove the intermediate claim HsingEq: {u} = {v}.
rewrite the current goal using Hpu (from right to left).
rewrite the current goal using Heq (from left to right).
rewrite the current goal using Hpv (from left to right).
Use reflexivity.
We prove the intermediate claim HuIn: u ∈ {u}.
An exact proof term for the current goal is (SingI u).
We prove the intermediate claim HuInV: u ∈ {v}.
rewrite the current goal using HsingEq (from right to left).
An exact proof term for the current goal is HuIn.
An exact proof term for the current goal is (SingE v u HuInV).
We prove the intermediate claim HcountI: countable I.
We will prove countable I.
We will prove atleastp I ω.
We prove the intermediate claim HIB: atleastp I B.
We will prove ∃f : set → set, inj I B f.
We use pick_iso to witness the existential quantifier.
An exact proof term for the current goal is HinjIB.
We prove the intermediate claim HBO: atleastp B ω.
An exact proof term for the current goal is HBcountset.
An exact proof term for the current goal is (atleastp_tra I B ω HIB HBO).
We prove the intermediate claim HAeq: A = I ∪ L.
Apply set_ext to the current goal.
Let x be given.
Assume HxA: x ∈ A.
We will prove x ∈ I ∪ L.
Apply (xm (limit_point_of X Tx A x)) to the current goal.
Assume Hlp: limit_point_of X Tx A x.
Apply binunionI2 to the current goal.
An exact proof term for the current goal is (SepI A (λx0 : set ⇒ limit_point_of X Tx A x0) x HxA Hlp).
Assume Hnotlp: ¬ limit_point_of X Tx A x.
Apply binunionI1 to the current goal.
An exact proof term for the current goal is (SepI A (λx0 : set ⇒ ¬ limit_point_of X Tx A x0) x HxA Hnotlp).
Let x be given.
Assume HxUL: x ∈ I ∪ L.
We will prove x ∈ A.
Apply (binunionE' I L x (x ∈ A)) to the current goal.
Assume HxI: x ∈ I.
An exact proof term for the current goal is (SepE1 A (λx0 : set ⇒ ¬ limit_point_of X Tx A x0) x HxI).
Assume HxL: x ∈ L.
An exact proof term for the current goal is (SepE1 A (λx0 : set ⇒ limit_point_of X Tx A x0) x HxL).
An exact proof term for the current goal is HxUL.
We prove the intermediate claim HcountUnion: countable (I ∪ L).
An exact proof term for the current goal is (binunion_countable I L HcountI HcountL).
We prove the intermediate claim HcountA: countable A.
rewrite the current goal using HAeq (from left to right).
An exact proof term for the current goal is HcountUnion.
An exact proof term for the current goal is (HuncA HcountA).
∎