Let X and Tx be given.
Assume Hcomp: compact_space X Tx.
We will prove limit_point_compact X Tx.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (compact_space_topology X Tx Hcomp).
We will prove topology_on X Tx ∧ ∀A : set, A ⊆ X → infinite A → ∃x : set, limit_point_of X Tx A x.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Let A be given.
Assume HA: A ⊆ X.
Assume HinfA: infinite A.
We will prove ∃x : set, limit_point_of X Tx A x.
Apply (xm (∃x : set, limit_point_of X Tx A x)) to the current goal.
Assume Hex: ∃x : set, limit_point_of X Tx A x.
An exact proof term for the current goal is Hex.
Assume Hnone: ¬ (∃x : set, limit_point_of X Tx A x).
We will prove ∃x : set, limit_point_of X Tx A x.
Apply FalseE to the current goal.
We will prove False.
Set Fam to be the term {U ∈ Tx|∃x : set, x ∈ X ∧ x ∈ U ∧ ¬ (∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U)}.
We prove the intermediate claim HFam_in_Tx: ∀U : set, U ∈ Fam → U ∈ Tx.
Let U be given.
Assume HU: U ∈ Fam.
An exact proof term for the current goal is (SepE1 Tx (λU0 : set ⇒ ∃x : set, x ∈ X ∧ x ∈ U0 ∧ ¬ (∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U0)) U HU).
We prove the intermediate claim HFam_sub_PowX: Fam ⊆ 𝒫 X.
Let U be given.
Assume HU: U ∈ Fam.
We will prove U ∈ 𝒫 X.
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (HFam_in_Tx U HU).
We prove the intermediate claim HUsubX: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U HTx HUinTx).
An exact proof term for the current goal is (PowerI X U HUsubX).
We prove the intermediate claim HX_sub_UnionFam: X ⊆ ⋃ Fam.
Let x be given.
Assume HxX: x ∈ X.
We will prove x ∈ ⋃ Fam.
We prove the intermediate claim HnotLp: ¬ limit_point_of X Tx A x.
Assume Hlp: limit_point_of X Tx A x.
Apply Hnone to the current goal.
We use x to witness the existential quantifier.
An exact proof term for the current goal is Hlp.
We prove the intermediate claim HnotForall: ¬ (∀U : set, U ∈ Tx → x ∈ U → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U).
Assume Hall: ∀U : set, U ∈ Tx → x ∈ U → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U.
Apply HnotLp 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 Hall.
We prove the intermediate claim HexU: ∃U : set, ¬ (U ∈ Tx → x ∈ U → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U).
An exact proof term for the current goal is (not_all_ex_demorgan_i (λU : set ⇒ U ∈ Tx → x ∈ U → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U) HnotForall).
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 HUinTx: U ∈ Tx.
Apply (xm (U ∈ Tx)) to the current goal.
Assume HU: U ∈ Tx.
An exact proof term for the current goal is HU.
Assume HUn: U ∉ Tx.
We will prove U ∈ Tx.
Apply FalseE to the current goal.
We will prove False.
We prove the intermediate claim Himp: U ∈ Tx → x ∈ U → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U.
Assume HU0: U ∈ Tx.
Assume _.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HUn HU0).
An exact proof term for the current goal is (HnotImp Himp).
We prove the intermediate claim HxU: x ∈ U.
Apply (xm (x ∈ U)) to the current goal.
Assume Hxu: x ∈ U.
An exact proof term for the current goal is Hxu.
Assume HxUn: x ∉ U.
We will prove x ∈ U.
Apply FalseE to the current goal.
We will prove False.
We prove the intermediate claim Himp: U ∈ Tx → x ∈ U → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U.
Assume _.
Assume Hxu: x ∈ U.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxUn Hxu).
An exact proof term for the current goal is (HnotImp Himp).
We prove the intermediate claim HnoY: ¬ (∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U).
Assume Hexy: ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U.
We will prove False.
We prove the intermediate claim Himp: U ∈ Tx → x ∈ U → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U.
Assume _.
Assume _.
An exact proof term for the current goal is Hexy.
An exact proof term for the current goal is (HnotImp Himp).
We prove the intermediate claim HUinFam: U ∈ Fam.
Apply (SepI Tx (λU0 : set ⇒ ∃x0 : set, x0 ∈ X ∧ x0 ∈ U0 ∧ ¬ (∃y : set, y ∈ A ∧ y ≠ x0 ∧ y ∈ U0)) U HUinTx) to the current goal.
We use x to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HxX.
An exact proof term for the current goal is HxU.
An exact proof term for the current goal is HnoY.
An exact proof term for the current goal is (UnionI Fam x U HxU HUinFam).
We prove the intermediate claim HFam_cover: open_cover_of X Tx Fam.
We will prove topology_on X Tx ∧ Fam ⊆ 𝒫 X ∧ X ⊆ ⋃ Fam ∧ (∀U : set, U ∈ Fam → U ∈ Tx).
Apply andI to the current goal.
We will prove (topology_on X Tx ∧ Fam ⊆ 𝒫 X) ∧ X ⊆ ⋃ Fam.
Apply andI to the current goal.
We will prove topology_on X Tx ∧ Fam ⊆ 𝒫 X.
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 HFam_sub_PowX.
An exact proof term for the current goal is HX_sub_UnionFam.
An exact proof term for the current goal is HFam_in_Tx.
We prove the intermediate claim Hsub: has_finite_subcover X Tx Fam.
An exact proof term for the current goal is (Heine_Borel_subcover X Tx Fam Hcomp HFam_cover).
Apply Hsub to the current goal.
Let G be given.
Assume HG: G ⊆ Fam ∧ finite G ∧ X ⊆ ⋃ G.
We prove the intermediate claim HG1: G ⊆ Fam ∧ finite G.
An exact proof term for the current goal is (andEL (G ⊆ Fam ∧ finite G) (X ⊆ ⋃ G) HG).
We prove the intermediate claim HGsub: G ⊆ Fam.
An exact proof term for the current goal is (andEL (G ⊆ Fam) (finite G) HG1).
We prove the intermediate claim HGfin: finite G.
An exact proof term for the current goal is (andER (G ⊆ Fam) (finite G) HG1).
We prove the intermediate claim HXcovG: X ⊆ ⋃ G.
An exact proof term for the current goal is (andER (G ⊆ Fam ∧ finite G) (X ⊆ ⋃ G) HG).
Set pickX to be the term λU : set ⇒ Eps_i (λx : set ⇒ x ∈ X ∧ x ∈ U ∧ ¬ (∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U)).
Set Ximg to be the term {pickX U|U ∈ G}.
We prove the intermediate claim HXimgFin: finite Ximg.
An exact proof term for the current goal is (Repl_finite (λU : set ⇒ pickX U) G HGfin).
We prove the intermediate claim HAsubXimg: A ⊆ Ximg.
Let a be given.
Assume HaA: a ∈ A.
We will prove a ∈ Ximg.
We prove the intermediate claim HaX: a ∈ X.
An exact proof term for the current goal is (HA a HaA).
We prove the intermediate claim HaUnionG: a ∈ ⋃ G.
An exact proof term for the current goal is (HXcovG a HaX).
Apply (UnionE_impred G a HaUnionG) to the current goal.
Let U be given.
Assume HaU: a ∈ U.
Assume HUinG: U ∈ G.
We prove the intermediate claim HUinFam: U ∈ Fam.
An exact proof term for the current goal is (HGsub U HUinG).
We prove the intermediate claim HexxU: ∃x : set, x ∈ X ∧ x ∈ U ∧ ¬ (∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U).
An exact proof term for the current goal is (SepE2 Tx (λU0 : set ⇒ ∃x : set, x ∈ X ∧ x ∈ U0 ∧ ¬ (∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U0)) U HUinFam).
We prove the intermediate claim HpickProp: pickX U ∈ X ∧ pickX U ∈ U ∧ ¬ (∃y : set, y ∈ A ∧ y ≠ pickX U ∧ y ∈ U).
Apply HexxU to the current goal.
Let x0 be given.
Assume Hx0: x0 ∈ X ∧ x0 ∈ U ∧ ¬ (∃y : set, y ∈ A ∧ y ≠ x0 ∧ y ∈ U).
An exact proof term for the current goal is (Eps_i_ax (λx : set ⇒ x ∈ X ∧ x ∈ U ∧ ¬ (∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U)) x0 Hx0).
We prove the intermediate claim HnoOther: ¬ (∃y : set, y ∈ A ∧ y ≠ pickX U ∧ y ∈ U).
An exact proof term for the current goal is (andER (pickX U ∈ X ∧ pickX U ∈ U) (¬ (∃y : set, y ∈ A ∧ y ≠ pickX U ∧ y ∈ U)) HpickProp).
We prove the intermediate claim HaEq: a = pickX U.
Apply (xm (a = pickX U)) to the current goal.
Assume Heq: a = pickX U.
An exact proof term for the current goal is Heq.
Assume Hneq: a ≠ pickX U.
We will prove a = pickX U.
Apply FalseE to the current goal.
We will prove False.
We prove the intermediate claim Hexy: ∃y : set, y ∈ A ∧ y ≠ pickX U ∧ y ∈ U.
We use a to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HaA.
An exact proof term for the current goal is Hneq.
An exact proof term for the current goal is HaU.
An exact proof term for the current goal is (HnoOther Hexy).
We prove the intermediate claim HpickInImg: pickX U ∈ Ximg.
An exact proof term for the current goal is (ReplI G (λU0 : set ⇒ pickX U0) U HUinG).
rewrite the current goal using HaEq (from left to right).
An exact proof term for the current goal is HpickInImg.
We prove the intermediate claim HfinA: finite A.
An exact proof term for the current goal is (Subq_finite Ximg HXimgFin A HAsubXimg).
An exact proof term for the current goal is (HinfA HfinA).
∎