Let X and Tx be given.
Assume Hcomp: compact_space X Tx.
Assume HH: Hausdorff_space X Tx.
We will prove normal_space 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 prove the intermediate claim HT1: one_point_sets_closed X Tx.
We will prove topology_on X Tx ∧ ∀x : set, x ∈ X → closed_in X Tx {x}.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Let x be given.
Assume HxX: x ∈ X.
An exact proof term for the current goal is (Hausdorff_singletons_closed X Tx x HH HxX).
We will prove one_point_sets_closed X Tx ∧ ∀A B : set, closed_in X Tx A → closed_in X Tx B → A ∩ B = Empty → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty.
Apply andI to the current goal.
An exact proof term for the current goal is HT1.
Let A and B be given.
Assume HAcl: closed_in X Tx A.
Assume HBcl: closed_in X Tx B.
Assume Hdisj: A ∩ B = Empty.
We will prove ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty.
We prove the intermediate claim HAsubX: A ⊆ X.
An exact proof term for the current goal is (closed_in_subset X Tx A HAcl).
We prove the intermediate claim HBsubX: B ⊆ X.
An exact proof term for the current goal is (closed_in_subset X Tx B HBcl).
We prove the intermediate claim HcompA: compact_space A (subspace_topology X Tx A).
An exact proof term for the current goal is (closed_subspace_compact X Tx A Hcomp HAcl).
We prove the intermediate claim HcompB: compact_space B (subspace_topology X Tx B).
An exact proof term for the current goal is (closed_subspace_compact X Tx B Hcomp HBcl).
Set Uof to be the term λa : set ⇒ Eps_i (λU : set ⇒ ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ a ∈ U ∧ B ⊆ V ∧ U ∩ V = Empty).
Set Vof to be the term λa : set ⇒ Eps_i (λV : set ⇒ Uof a ∈ Tx ∧ V ∈ Tx ∧ a ∈ Uof a ∧ B ⊆ V ∧ Uof a ∩ V = Empty).
We prove the intermediate claim UVprop: ∀a : set, a ∈ A → Uof a ∈ Tx ∧ (Vof a ∈ Tx ∧ (a ∈ Uof a ∧ (B ⊆ Vof a ∧ Uof a ∩ Vof a = Empty))).
Let a be given.
Assume HaA: a ∈ A.
We prove the intermediate claim HaX: a ∈ X.
An exact proof term for the current goal is (HAsubX a HaA).
We prove the intermediate claim HanotB: a ∉ B.
Assume HaB: a ∈ B.
We prove the intermediate claim HaAB: a ∈ A ∩ B.
An exact proof term for the current goal is (binintersectI A B a HaA HaB).
We prove the intermediate claim HaE: a ∈ Empty.
rewrite the current goal using Hdisj (from right to left).
An exact proof term for the current goal is HaAB.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE a HaE False).
We prove the intermediate claim HexUV: ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ a ∈ U ∧ B ⊆ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (Hausdorff_separate_point_compact_set X Tx B a HH HBsubX HcompB HaX HanotB).
We prove the intermediate claim HUof: ∃V : set, Uof a ∈ Tx ∧ V ∈ Tx ∧ a ∈ Uof a ∧ B ⊆ V ∧ Uof a ∩ V = Empty.
An exact proof term for the current goal is (Eps_i_ex (λU : set ⇒ ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ a ∈ U ∧ B ⊆ V ∧ U ∩ V = Empty) HexUV).
We prove the intermediate claim HVof: Uof a ∈ Tx ∧ Vof a ∈ Tx ∧ a ∈ Uof a ∧ B ⊆ Vof a ∧ Uof a ∩ Vof a = Empty.
An exact proof term for the current goal is (Eps_i_ex (λV : set ⇒ Uof a ∈ Tx ∧ V ∈ Tx ∧ a ∈ Uof a ∧ B ⊆ V ∧ Uof a ∩ V = Empty) HUof).
We prove the intermediate claim H1234: ((Uof a ∈ Tx ∧ Vof a ∈ Tx) ∧ a ∈ Uof a) ∧ B ⊆ Vof a.
An exact proof term for the current goal is (andEL (((Uof a ∈ Tx ∧ Vof a ∈ Tx) ∧ a ∈ Uof a) ∧ B ⊆ Vof a) (Uof a ∩ Vof a = Empty) HVof).
We prove the intermediate claim H5: Uof a ∩ Vof a = Empty.
An exact proof term for the current goal is (andER (((Uof a ∈ Tx ∧ Vof a ∈ Tx) ∧ a ∈ Uof a) ∧ B ⊆ Vof a) (Uof a ∩ Vof a = Empty) HVof).
We prove the intermediate claim H123: (Uof a ∈ Tx ∧ Vof a ∈ Tx) ∧ a ∈ Uof a.
An exact proof term for the current goal is (andEL ((Uof a ∈ Tx ∧ Vof a ∈ Tx) ∧ a ∈ Uof a) (B ⊆ Vof a) H1234).
We prove the intermediate claim H4: B ⊆ Vof a.
An exact proof term for the current goal is (andER ((Uof a ∈ Tx ∧ Vof a ∈ Tx) ∧ a ∈ Uof a) (B ⊆ Vof a) H1234).
We prove the intermediate claim H12: Uof a ∈ Tx ∧ Vof a ∈ Tx.
An exact proof term for the current goal is (andEL (Uof a ∈ Tx ∧ Vof a ∈ Tx) (a ∈ Uof a) H123).
We prove the intermediate claim H3: a ∈ Uof a.
An exact proof term for the current goal is (andER (Uof a ∈ Tx ∧ Vof a ∈ Tx) (a ∈ Uof a) H123).
We prove the intermediate claim HUofTx: Uof a ∈ Tx.
An exact proof term for the current goal is (andEL (Uof a ∈ Tx) (Vof a ∈ Tx) H12).
We prove the intermediate claim HVofTx: Vof a ∈ Tx.
An exact proof term for the current goal is (andER (Uof a ∈ Tx) (Vof a ∈ Tx) H12).
Apply andI to the current goal.
An exact proof term for the current goal is HUofTx.
Apply andI to the current goal.
An exact proof term for the current goal is HVofTx.
Apply andI to the current goal.
An exact proof term for the current goal is H3.
Apply andI to the current goal.
An exact proof term for the current goal is H4.
An exact proof term for the current goal is H5.
Set Fam to be the term {Uof a|a ∈ A}.
We prove the intermediate claim HFamSub: Fam ⊆ Tx.
Let U be given.
Assume HU: U ∈ Fam.
Apply (ReplE_impred A (λa : set ⇒ Uof a) U HU (U ∈ Tx)) to the current goal.
Let a be given.
Assume HaA: a ∈ A.
Assume HUeq: U = Uof a.
We prove the intermediate claim HUofTx: Uof a ∈ Tx.
An exact proof term for the current goal is (andEL (Uof a ∈ Tx) (Vof a ∈ Tx ∧ (a ∈ Uof a ∧ (B ⊆ Vof a ∧ Uof a ∩ Vof a = Empty))) (UVprop a HaA)).
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is HUofTx.
We prove the intermediate claim HAcov: A ⊆ ⋃ Fam.
Let a be given.
Assume HaA: a ∈ A.
We will prove a ∈ ⋃ Fam.
We prove the intermediate claim HaU: a ∈ Uof a.
An exact proof term for the current goal is (andEL (a ∈ Uof a) (B ⊆ Vof a ∧ Uof a ∩ Vof a = Empty) (andER (Vof a ∈ Tx) (a ∈ Uof a ∧ (B ⊆ Vof a ∧ Uof a ∩ Vof a = Empty)) (andER (Uof a ∈ Tx) (Vof a ∈ Tx ∧ (a ∈ Uof a ∧ (B ⊆ Vof a ∧ Uof a ∩ Vof a = Empty))) (UVprop a HaA)))).
We prove the intermediate claim HUinFam: Uof a ∈ Fam.
An exact proof term for the current goal is (ReplI A (λa0 : set ⇒ Uof a0) a HaA).
An exact proof term for the current goal is (UnionI Fam a (Uof a) HaU HUinFam).
We prove the intermediate claim HcoverProp: ∀Fam0 : set, (Fam0 ⊆ Tx ∧ A ⊆ ⋃ Fam0) → has_finite_subcover A Tx Fam0.
We prove the intermediate claim Hequiv: (compact_space A (subspace_topology X Tx A) ↔ ∀Fam0 : set, (Fam0 ⊆ Tx ∧ A ⊆ ⋃ Fam0) → has_finite_subcover A Tx Fam0).
An exact proof term for the current goal is (compact_subspace_via_ambient_covers X Tx A HTx HAsubX).
An exact proof term for the current goal is (iffEL (compact_space A (subspace_topology X Tx A)) (∀Fam0 : set, (Fam0 ⊆ Tx ∧ A ⊆ ⋃ Fam0) → has_finite_subcover A Tx Fam0) Hequiv HcompA).
We prove the intermediate claim Hfin: has_finite_subcover A Tx Fam.
An exact proof term for the current goal is (HcoverProp Fam (andI (Fam ⊆ Tx) (A ⊆ ⋃ Fam) HFamSub HAcov)).
Apply Hfin to the current goal.
Let G be given.
Assume HG: G ⊆ Fam ∧ finite G ∧ A ⊆ ⋃ G.
We prove the intermediate claim HGleft: G ⊆ Fam ∧ finite G.
An exact proof term for the current goal is (andEL (G ⊆ Fam ∧ finite G) (A ⊆ ⋃ G) HG).
We prove the intermediate claim HGsubFam: G ⊆ Fam.
An exact proof term for the current goal is (andEL (G ⊆ Fam) (finite G) HGleft).
We prove the intermediate claim HGfin: finite G.
An exact proof term for the current goal is (andER (G ⊆ Fam) (finite G) HGleft).
We prove the intermediate claim HAcovG: A ⊆ ⋃ G.
An exact proof term for the current goal is (andER (G ⊆ Fam ∧ finite G) (A ⊆ ⋃ G) HG).
We prove the intermediate claim HGsubTx: G ⊆ Tx.
Let U be given.
Assume HU: U ∈ G.
We will prove U ∈ Tx.
We prove the intermediate claim HUfam: U ∈ Fam.
An exact proof term for the current goal is (HGsubFam U HU).
An exact proof term for the current goal is (HFamSub U HUfam).
Set U to be the term ⋃ G.
We prove the intermediate claim HUtx: U ∈ Tx.
An exact proof term for the current goal is (topology_union_closed X Tx G HTx HGsubTx).
Set Wof to be the term λU0 : set ⇒ Eps_i (λa : set ⇒ a ∈ A ∧ U0 = Uof a).
We prove the intermediate claim Wof_spec: ∀U0 : set, U0 ∈ G → Wof U0 ∈ A ∧ U0 = Uof (Wof U0).
Let U0 be given.
Assume HU0G: U0 ∈ G.
We prove the intermediate claim HU0Fam: U0 ∈ Fam.
An exact proof term for the current goal is (HGsubFam U0 HU0G).
We prove the intermediate claim Hexa: ∃a : set, a ∈ A ∧ U0 = Uof a.
Apply (ReplE_impred A (λa0 : set ⇒ Uof a0) U0 HU0Fam (∃a : set, a ∈ A ∧ U0 = Uof a)) to the current goal.
Let a be given.
Assume HaA: a ∈ A.
Assume HU0eq: U0 = Uof a.
We use a to witness the existential quantifier.
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 HU0eq.
Apply Hexa to the current goal.
Let a be given.
Assume HaPair: a ∈ A ∧ U0 = Uof a.
An exact proof term for the current goal is (Eps_i_ax (λa0 : set ⇒ a0 ∈ A ∧ U0 = Uof a0) a HaPair).
Set GV to be the term {Vof (Wof U0)|U0 ∈ G}.
We prove the intermediate claim HGVfin: finite GV.
An exact proof term for the current goal is (Repl_finite (λU0 : set ⇒ Vof (Wof U0)) G HGfin).
We prove the intermediate claim HGVsubTx: GV ⊆ Tx.
Let V be given.
Assume HV: V ∈ GV.
Apply (ReplE_impred G (λU0 : set ⇒ Vof (Wof U0)) V HV (V ∈ Tx)) to the current goal.
Let U0 be given.
Assume HU0G: U0 ∈ G.
Assume HVe: V = Vof (Wof U0).
We prove the intermediate claim HWofA: Wof U0 ∈ A.
An exact proof term for the current goal is (andEL (Wof U0 ∈ A) (U0 = Uof (Wof U0)) (Wof_spec U0 HU0G)).
We prove the intermediate claim HVofTx: Vof (Wof U0) ∈ Tx.
An exact proof term for the current goal is (andEL (Vof (Wof U0) ∈ Tx) (Wof U0 ∈ Uof (Wof U0) ∧ (B ⊆ Vof (Wof U0) ∧ Uof (Wof U0) ∩ Vof (Wof U0) = Empty)) (andER (Uof (Wof U0) ∈ Tx) (Vof (Wof U0) ∈ Tx ∧ (Wof U0 ∈ Uof (Wof U0) ∧ (B ⊆ Vof (Wof U0) ∧ Uof (Wof U0) ∩ Vof (Wof U0) = Empty))) (UVprop (Wof U0) HWofA))).
rewrite the current goal using HVe (from left to right).
An exact proof term for the current goal is HVofTx.
Set V to be the term intersection_of_family X GV.
We prove the intermediate claim HVtx: V ∈ Tx.
We prove the intermediate claim HGVpow: GV ∈ 𝒫 Tx.
Apply PowerI to the current goal.
An exact proof term for the current goal is HGVsubTx.
An exact proof term for the current goal is (finite_intersection_in_topology X Tx GV HTx HGVpow HGVfin).
We prove the intermediate claim HBsubV: B ⊆ V.
Let b be given.
Assume HbB: b ∈ B.
We will prove b ∈ V.
We prove the intermediate claim HbPred: ∀U1 : set, U1 ∈ GV → b ∈ U1.
Let W be given.
Assume HW: W ∈ GV.
We will prove b ∈ W.
Apply (ReplE_impred G (λU0 : set ⇒ Vof (Wof U0)) W HW (b ∈ W)) to the current goal.
Let U0 be given.
Assume HU0G: U0 ∈ G.
Assume HWeq: W = Vof (Wof U0).
We prove the intermediate claim HWofA: Wof U0 ∈ A.
An exact proof term for the current goal is (andEL (Wof U0 ∈ A) (U0 = Uof (Wof U0)) (Wof_spec U0 HU0G)).
We prove the intermediate claim HUV1: Vof (Wof U0) ∈ Tx ∧ (Wof U0 ∈ Uof (Wof U0) ∧ (B ⊆ Vof (Wof U0) ∧ Uof (Wof U0) ∩ Vof (Wof U0) = Empty)).
An exact proof term for the current goal is (andER (Uof (Wof U0) ∈ Tx) (Vof (Wof U0) ∈ Tx ∧ (Wof U0 ∈ Uof (Wof U0) ∧ (B ⊆ Vof (Wof U0) ∧ Uof (Wof U0) ∩ Vof (Wof U0) = Empty))) (UVprop (Wof U0) HWofA)).
We prove the intermediate claim HUV2: Wof U0 ∈ Uof (Wof U0) ∧ (B ⊆ Vof (Wof U0) ∧ Uof (Wof U0) ∩ Vof (Wof U0) = Empty).
An exact proof term for the current goal is (andER (Vof (Wof U0) ∈ Tx) (Wof U0 ∈ Uof (Wof U0) ∧ (B ⊆ Vof (Wof U0) ∧ Uof (Wof U0) ∩ Vof (Wof U0) = Empty)) HUV1).
We prove the intermediate claim HUV3: B ⊆ Vof (Wof U0) ∧ Uof (Wof U0) ∩ Vof (Wof U0) = Empty.
An exact proof term for the current goal is (andER (Wof U0 ∈ Uof (Wof U0)) (B ⊆ Vof (Wof U0) ∧ Uof (Wof U0) ∩ Vof (Wof U0) = Empty) HUV2).
We prove the intermediate claim HBsubVof: B ⊆ Vof (Wof U0).
An exact proof term for the current goal is (andEL (B ⊆ Vof (Wof U0)) (Uof (Wof U0) ∩ Vof (Wof U0) = Empty) HUV3).
rewrite the current goal using HWeq (from left to right).
An exact proof term for the current goal is (HBsubVof b HbB).
An exact proof term for the current goal is (SepI X (λx : set ⇒ ∀U1 : set, U1 ∈ GV → x ∈ U1) b (HBsubX b HbB) HbPred).
We prove the intermediate claim HUVdisj: U ∩ V = Empty.
Apply Empty_Subq_eq to the current goal.
Let z be given.
Assume Hz: z ∈ U ∩ V.
We will prove z ∈ Empty.
We prove the intermediate claim HzU: z ∈ U.
An exact proof term for the current goal is (binintersectE1 U V z Hz).
We prove the intermediate claim HzV: z ∈ V.
An exact proof term for the current goal is (binintersectE2 U V z Hz).
Apply (UnionE_impred G z HzU (z ∈ Empty)) to the current goal.
Let U0 be given.
Assume HzU0: z ∈ U0.
Assume HU0G: U0 ∈ G.
We prove the intermediate claim HWofA: Wof U0 ∈ A.
An exact proof term for the current goal is (andEL (Wof U0 ∈ A) (U0 = Uof (Wof U0)) (Wof_spec U0 HU0G)).
We prove the intermediate claim HU0eq: U0 = Uof (Wof U0).
An exact proof term for the current goal is (andER (Wof U0 ∈ A) (U0 = Uof (Wof U0)) (Wof_spec U0 HU0G)).
We prove the intermediate claim HVinGV: Vof (Wof U0) ∈ GV.
An exact proof term for the current goal is (ReplI G (λU1 : set ⇒ Vof (Wof U1)) U0 HU0G).
We prove the intermediate claim HzVof: z ∈ Vof (Wof U0).
An exact proof term for the current goal is (SepE2 X (λx : set ⇒ ∀U1 : set, U1 ∈ GV → x ∈ U1) z HzV (Vof (Wof U0)) HVinGV).
We prove the intermediate claim HzUof: z ∈ Uof (Wof U0).
rewrite the current goal using HU0eq (from right to left).
An exact proof term for the current goal is HzU0.
We prove the intermediate claim Hdisj0: Uof (Wof U0) ∩ Vof (Wof U0) = Empty.
We prove the intermediate claim HUV1: Vof (Wof U0) ∈ Tx ∧ (Wof U0 ∈ Uof (Wof U0) ∧ (B ⊆ Vof (Wof U0) ∧ Uof (Wof U0) ∩ Vof (Wof U0) = Empty)).
An exact proof term for the current goal is (andER (Uof (Wof U0) ∈ Tx) (Vof (Wof U0) ∈ Tx ∧ (Wof U0 ∈ Uof (Wof U0) ∧ (B ⊆ Vof (Wof U0) ∧ Uof (Wof U0) ∩ Vof (Wof U0) = Empty))) (UVprop (Wof U0) HWofA)).
We prove the intermediate claim HUV2: Wof U0 ∈ Uof (Wof U0) ∧ (B ⊆ Vof (Wof U0) ∧ Uof (Wof U0) ∩ Vof (Wof U0) = Empty).
An exact proof term for the current goal is (andER (Vof (Wof U0) ∈ Tx) (Wof U0 ∈ Uof (Wof U0) ∧ (B ⊆ Vof (Wof U0) ∧ Uof (Wof U0) ∩ Vof (Wof U0) = Empty)) HUV1).
We prove the intermediate claim HUV3: B ⊆ Vof (Wof U0) ∧ Uof (Wof U0) ∩ Vof (Wof U0) = Empty.
An exact proof term for the current goal is (andER (Wof U0 ∈ Uof (Wof U0)) (B ⊆ Vof (Wof U0) ∧ Uof (Wof U0) ∩ Vof (Wof U0) = Empty) HUV2).
An exact proof term for the current goal is (andER (B ⊆ Vof (Wof U0)) (Uof (Wof U0) ∩ Vof (Wof U0) = Empty) HUV3).
We prove the intermediate claim HzUV0: z ∈ Uof (Wof U0) ∩ Vof (Wof U0).
An exact proof term for the current goal is (binintersectI (Uof (Wof U0)) (Vof (Wof U0)) z HzUof HzVof).
rewrite the current goal using Hdisj0 (from right to left).
An exact proof term for the current goal is HzUV0.
We use U to witness the existential quantifier.
We use V to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HUtx.
An exact proof term for the current goal is HVtx.
An exact proof term for the current goal is HAcovG.
An exact proof term for the current goal is HBsubV.
An exact proof term for the current goal is HUVdisj.
∎