Let X, Tx, Y and x be given.
Assume HH: Hausdorff_space X Tx.
Assume HYsub: Y ⊆ X.
Assume Hcomp: compact_space Y (subspace_topology X Tx Y).
Assume HxX: x ∈ X.
Assume Hx: x ∉ Y.
We will prove ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ Y ⊆ V ∧ U ∩ V = Empty.
Set Ty to be the term subspace_topology X Tx Y.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (∀x1 x2 : set, x1 ∈ X → x2 ∈ X → x1 ≠ x2 → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty) HH).
We prove the intermediate claim Hsep: ∀x1 x2 : set, x1 ∈ X → x2 ∈ X → x1 ≠ x2 → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀x1 x2 : set, x1 ∈ X → x2 ∈ X → x1 ≠ x2 → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty) HH).
Set Vof to be the term λy : set ⇒ Eps_i (λV : set ⇒ ∃U : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = Empty).
Set Uof to be the term λy : set ⇒ Eps_i (λU : set ⇒ U ∈ Tx ∧ x ∈ U ∧ U ∩ (Vof y) = Empty).
We prove the intermediate claim Vof_exists: ∀y : set, y ∈ Y → ∃U : set, U ∈ Tx ∧ (Vof y) ∈ Tx ∧ x ∈ U ∧ y ∈ (Vof y) ∧ U ∩ (Vof y) = Empty.
Let y be given.
Assume HyY: y ∈ Y.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HYsub y HyY).
We prove the intermediate claim Hneq: x ≠ y.
Assume Heq: x = y.
Apply Hx to the current goal.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HyY.
We prove the intermediate claim Hex: ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (Hsep x y HxX HyX Hneq).
Apply Hex to the current goal.
Let U0 be given.
Assume HexV0: ∃V0 : set, U0 ∈ Tx ∧ V0 ∈ Tx ∧ x ∈ U0 ∧ y ∈ V0 ∧ U0 ∩ V0 = Empty.
Apply HexV0 to the current goal.
Let V0 be given.
Assume HUV0: U0 ∈ Tx ∧ V0 ∈ Tx ∧ x ∈ U0 ∧ y ∈ V0 ∧ U0 ∩ V0 = Empty.
We prove the intermediate claim HpV0: ∃U : set, U ∈ Tx ∧ V0 ∈ Tx ∧ x ∈ U ∧ y ∈ V0 ∧ U ∩ V0 = Empty.
We use U0 to witness the existential quantifier.
An exact proof term for the current goal is HUV0.
An exact proof term for the current goal is (Eps_i_ax (λV : set ⇒ ∃U : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = Empty) V0 HpV0).
We prove the intermediate claim Vof_in_Tx: ∀y : set, y ∈ Y → (Vof y) ∈ Tx.
Let y be given.
Assume HyY: y ∈ Y.
Apply (Vof_exists y HyY) to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ Tx ∧ (Vof y) ∈ Tx ∧ x ∈ U0 ∧ y ∈ (Vof y) ∧ U0 ∩ (Vof y) = Empty.
We prove the intermediate claim HU0A: ((U0 ∈ Tx ∧ (Vof y) ∈ Tx) ∧ x ∈ U0) ∧ y ∈ (Vof y).
An exact proof term for the current goal is (andEL (((U0 ∈ Tx ∧ (Vof y) ∈ Tx) ∧ x ∈ U0) ∧ y ∈ (Vof y)) (U0 ∩ (Vof y) = Empty) HU0).
We prove the intermediate claim HU0A1: (U0 ∈ Tx ∧ (Vof y) ∈ Tx) ∧ x ∈ U0.
An exact proof term for the current goal is (andEL ((U0 ∈ Tx ∧ (Vof y) ∈ Tx) ∧ x ∈ U0) (y ∈ (Vof y)) HU0A).
We prove the intermediate claim HU0AB: U0 ∈ Tx ∧ (Vof y) ∈ Tx.
An exact proof term for the current goal is (andEL (U0 ∈ Tx ∧ (Vof y) ∈ Tx) (x ∈ U0) HU0A1).
An exact proof term for the current goal is (andER (U0 ∈ Tx) ((Vof y) ∈ Tx) HU0AB).
We prove the intermediate claim y_in_Vof: ∀y : set, y ∈ Y → y ∈ (Vof y).
Let y be given.
Assume HyY: y ∈ Y.
Apply (Vof_exists y HyY) to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ Tx ∧ (Vof y) ∈ Tx ∧ x ∈ U0 ∧ y ∈ (Vof y) ∧ U0 ∩ (Vof y) = Empty.
We prove the intermediate claim HU0A: ((U0 ∈ Tx ∧ (Vof y) ∈ Tx) ∧ x ∈ U0) ∧ y ∈ (Vof y).
An exact proof term for the current goal is (andEL (((U0 ∈ Tx ∧ (Vof y) ∈ Tx) ∧ x ∈ U0) ∧ y ∈ (Vof y)) (U0 ∩ (Vof y) = Empty) HU0).
An exact proof term for the current goal is (andER ((U0 ∈ Tx ∧ (Vof y) ∈ Tx) ∧ x ∈ U0) (y ∈ (Vof y)) HU0A).
We prove the intermediate claim Uof_props: ∀y : set, y ∈ Y → (Uof y) ∈ Tx ∧ x ∈ (Uof y) ∧ (Uof y) ∩ (Vof y) = Empty.
Let y be given.
Assume HyY: y ∈ Y.
We prove the intermediate claim HexU: ∃U0 : set, U0 ∈ Tx ∧ x ∈ U0 ∧ U0 ∩ (Vof y) = Empty.
Apply (Vof_exists y HyY) to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ Tx ∧ (Vof y) ∈ Tx ∧ x ∈ U0 ∧ y ∈ (Vof y) ∧ U0 ∩ (Vof y) = Empty.
We use U0 to witness the existential quantifier.
We prove the intermediate claim HU0A: ((U0 ∈ Tx ∧ (Vof y) ∈ Tx) ∧ x ∈ U0) ∧ y ∈ (Vof y).
An exact proof term for the current goal is (andEL (((U0 ∈ Tx ∧ (Vof y) ∈ Tx) ∧ x ∈ U0) ∧ y ∈ (Vof y)) (U0 ∩ (Vof y) = Empty) HU0).
We prove the intermediate claim HU0A1: (U0 ∈ Tx ∧ (Vof y) ∈ Tx) ∧ x ∈ U0.
An exact proof term for the current goal is (andEL ((U0 ∈ Tx ∧ (Vof y) ∈ Tx) ∧ x ∈ U0) (y ∈ (Vof y)) HU0A).
We prove the intermediate claim HU0AB: U0 ∈ Tx ∧ (Vof y) ∈ Tx.
An exact proof term for the current goal is (andEL (U0 ∈ Tx ∧ (Vof y) ∈ Tx) (x ∈ U0) HU0A1).
We prove the intermediate claim HU0Tx: U0 ∈ Tx.
An exact proof term for the current goal is (andEL (U0 ∈ Tx) ((Vof y) ∈ Tx) HU0AB).
We prove the intermediate claim HxU0: x ∈ U0.
An exact proof term for the current goal is (andER (U0 ∈ Tx ∧ (Vof y) ∈ Tx) (x ∈ U0) HU0A1).
We prove the intermediate claim HU0disj: U0 ∩ (Vof y) = Empty.
An exact proof term for the current goal is (andER (((U0 ∈ Tx ∧ (Vof y) ∈ Tx) ∧ x ∈ U0) ∧ y ∈ (Vof y)) (U0 ∩ (Vof y) = Empty) HU0).
We prove the intermediate claim HU0pair: U0 ∈ Tx ∧ x ∈ U0.
Apply andI to the current goal.
An exact proof term for the current goal is HU0Tx.
An exact proof term for the current goal is HxU0.
An exact proof term for the current goal is (andI (U0 ∈ Tx ∧ x ∈ U0) (U0 ∩ (Vof y) = Empty) HU0pair HU0disj).
Apply HexU to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ Tx ∧ x ∈ U0 ∧ U0 ∩ (Vof y) = Empty.
An exact proof term for the current goal is (Eps_i_ax (λU : set ⇒ U ∈ Tx ∧ x ∈ U ∧ U ∩ (Vof y) = Empty) U0 HU0).
Set VFam to be the term {Vof y|y ∈ Y}.
We prove the intermediate claim HVFamSub: VFam ⊆ Tx.
Let V be given.
Assume HV: V ∈ VFam.
Apply (ReplE_impred Y (λy0 : set ⇒ Vof y0) V HV) to the current goal.
Let y be given.
Assume HyY: y ∈ Y.
Assume HVe: V = Vof y.
rewrite the current goal using HVe (from left to right).
An exact proof term for the current goal is (Vof_in_Tx y HyY).
We prove the intermediate claim HYcovVFam: Y ⊆ ⋃ VFam.
Let y be given.
Assume HyY: y ∈ Y.
We will prove y ∈ ⋃ VFam.
An exact proof term for the current goal is (UnionI VFam y (Vof y) (y_in_Vof y HyY) (ReplI Y (λy0 : set ⇒ Vof y0) y HyY)).
We prove the intermediate claim Hcovprop: ∀Fam : set, (Fam ⊆ Tx ∧ Y ⊆ ⋃ Fam) → has_finite_subcover Y Tx Fam.
An exact proof term for the current goal is (iffEL (compact_space Y Ty) (∀Fam : set, (Fam ⊆ Tx ∧ Y ⊆ ⋃ Fam) → has_finite_subcover Y Tx Fam) (compact_subspace_via_ambient_covers X Tx Y HTx HYsub) Hcomp).
We prove the intermediate claim Hfin: has_finite_subcover Y Tx VFam.
An exact proof term for the current goal is (Hcovprop VFam (andI (VFam ⊆ Tx) (Y ⊆ ⋃ VFam) HVFamSub HYcovVFam)).
Apply Hfin to the current goal.
Let G be given.
Assume HG: G ⊆ VFam ∧ finite G ∧ Y ⊆ ⋃ G.
We prove the intermediate claim HGleft: G ⊆ VFam ∧ finite G.
An exact proof term for the current goal is (andEL (G ⊆ VFam ∧ finite G) (Y ⊆ ⋃ G) HG).
We prove the intermediate claim HGsub: G ⊆ VFam.
An exact proof term for the current goal is (andEL (G ⊆ VFam) (finite G) HGleft).
We prove the intermediate claim HGfin: finite G.
An exact proof term for the current goal is (andER (G ⊆ VFam) (finite G) HGleft).
We prove the intermediate claim HGcov: Y ⊆ ⋃ G.
An exact proof term for the current goal is (andER (G ⊆ VFam ∧ finite G) (Y ⊆ ⋃ G) HG).
Set V to be the term ⋃ G.
We prove the intermediate claim HGTX: G ⊆ Tx.
Let W be given.
Assume HW: W ∈ G.
We prove the intermediate claim HWVFam: W ∈ VFam.
An exact proof term for the current goal is (HGsub W HW).
An exact proof term for the current goal is (HVFamSub W HWVFam).
We prove the intermediate claim HVopen: V ∈ Tx.
An exact proof term for the current goal is (topology_union_closed X Tx G HTx HGTX).
We prove the intermediate claim HYsubV: Y ⊆ V.
An exact proof term for the current goal is HGcov.
Set pickY to be the term λV0 : set ⇒ Eps_i (λy0 : set ⇒ y0 ∈ Y ∧ V0 = Vof y0).
Set UFam to be the term {Uof (pickY V0)|V0 ∈ G}.
Set U to be the term intersection_of_family X UFam.
We prove the intermediate claim HUFamSub: UFam ⊆ Tx.
Let U0 be given.
Assume HU0: U0 ∈ UFam.
Apply (ReplE_impred G (λV0 : set ⇒ Uof (pickY V0)) U0 HU0) to the current goal.
Let V0 be given.
Assume HV0G: V0 ∈ G.
Assume HU0eq: U0 = Uof (pickY V0).
rewrite the current goal using HU0eq (from left to right).
We prove the intermediate claim Hpick: pickY V0 ∈ Y.
We prove the intermediate claim HV0VFam: V0 ∈ VFam.
An exact proof term for the current goal is (HGsub V0 HV0G).
Apply (ReplE_impred Y (λy0 : set ⇒ Vof y0) V0 HV0VFam) to the current goal.
Let y0 be given.
Assume Hy0Y: y0 ∈ Y.
Assume HV0eq: V0 = Vof y0.
We prove the intermediate claim Hp: (y0 ∈ Y ∧ V0 = Vof y0).
An exact proof term for the current goal is (andI (y0 ∈ Y) (V0 = Vof y0) Hy0Y HV0eq).
An exact proof term for the current goal is (andEL (pickY V0 ∈ Y) (V0 = Vof (pickY V0)) (Eps_i_ax (λy : set ⇒ y ∈ Y ∧ V0 = Vof y) y0 Hp)).
We prove the intermediate claim HUof: (Uof (pickY V0)) ∈ Tx ∧ x ∈ (Uof (pickY V0)) ∧ (Uof (pickY V0)) ∩ (Vof (pickY V0)) = Empty.
An exact proof term for the current goal is (Uof_props (pickY V0) Hpick).
We prove the intermediate claim HUof1: (Uof (pickY V0)) ∈ Tx ∧ x ∈ (Uof (pickY V0)).
An exact proof term for the current goal is (andEL ((Uof (pickY V0)) ∈ Tx ∧ x ∈ (Uof (pickY V0))) ((Uof (pickY V0)) ∩ (Vof (pickY V0)) = Empty) HUof).
An exact proof term for the current goal is (andEL ((Uof (pickY V0)) ∈ Tx) (x ∈ (Uof (pickY V0))) HUof1).
We prove the intermediate claim HUFamFin: finite UFam.
An exact proof term for the current goal is (Repl_finite (λV0 : set ⇒ Uof (pickY V0)) G HGfin).
We prove the intermediate claim HUFamPow: UFam ∈ 𝒫 Tx.
An exact proof term for the current goal is (PowerI Tx UFam HUFamSub).
We prove the intermediate claim HUopen: U ∈ Tx.
An exact proof term for the current goal is (finite_intersection_in_topology X Tx UFam HTx HUFamPow HUFamFin).
We prove the intermediate claim HxU: x ∈ U.
We will prove x ∈ intersection_of_family X UFam.
We will prove x ∈ {z ∈ X|∀T : set, T ∈ UFam → z ∈ T}.
Apply SepI to the current goal.
An exact proof term for the current goal is HxX.
Let W be given.
Assume HW: W ∈ UFam.
Apply (ReplE_impred G (λV0 : set ⇒ Uof (pickY V0)) W HW) to the current goal.
Let V0 be given.
Assume HV0G: V0 ∈ G.
Assume HWeq: W = Uof (pickY V0).
rewrite the current goal using HWeq (from left to right).
We prove the intermediate claim Hpick: pickY V0 ∈ Y.
We prove the intermediate claim HV0VFam: V0 ∈ VFam.
An exact proof term for the current goal is (HGsub V0 HV0G).
Apply (ReplE_impred Y (λy0 : set ⇒ Vof y0) V0 HV0VFam) to the current goal.
Let y0 be given.
Assume Hy0Y: y0 ∈ Y.
Assume HV0eq: V0 = Vof y0.
We prove the intermediate claim Hp: (y0 ∈ Y ∧ V0 = Vof y0).
An exact proof term for the current goal is (andI (y0 ∈ Y) (V0 = Vof y0) Hy0Y HV0eq).
An exact proof term for the current goal is (andEL (pickY V0 ∈ Y) (V0 = Vof (pickY V0)) (Eps_i_ax (λy : set ⇒ y ∈ Y ∧ V0 = Vof y) y0 Hp)).
We prove the intermediate claim HUof: (Uof (pickY V0)) ∈ Tx ∧ x ∈ (Uof (pickY V0)) ∧ (Uof (pickY V0)) ∩ (Vof (pickY V0)) = Empty.
An exact proof term for the current goal is (Uof_props (pickY V0) Hpick).
We prove the intermediate claim HUof1: (Uof (pickY V0)) ∈ Tx ∧ x ∈ (Uof (pickY V0)).
An exact proof term for the current goal is (andEL ((Uof (pickY V0)) ∈ Tx ∧ x ∈ (Uof (pickY V0))) ((Uof (pickY V0)) ∩ (Vof (pickY V0)) = Empty) HUof).
An exact proof term for the current goal is (andER ((Uof (pickY V0)) ∈ Tx) (x ∈ (Uof (pickY V0))) HUof1).
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 False.
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).
We prove the intermediate claim HzUG: z ∈ ⋃ G.
An exact proof term for the current goal is HzV.
Apply (UnionE_impred G z HzUG) to the current goal.
Let V0 be given.
Assume HzV0: z ∈ V0.
Assume HV0G: V0 ∈ G.
We prove the intermediate claim HV0VFam: V0 ∈ VFam.
An exact proof term for the current goal is (HGsub V0 HV0G).
Apply (ReplE_impred Y (λy0 : set ⇒ Vof y0) V0 HV0VFam) to the current goal.
Let y0 be given.
Assume Hy0Y: y0 ∈ Y.
Assume HV0eq: V0 = Vof y0.
We prove the intermediate claim Hp: y0 ∈ Y ∧ V0 = Vof y0.
An exact proof term for the current goal is (andI (y0 ∈ Y) (V0 = Vof y0) Hy0Y HV0eq).
We prove the intermediate claim HpickY: pickY V0 ∈ Y ∧ V0 = Vof (pickY V0).
An exact proof term for the current goal is (Eps_i_ax (λy : set ⇒ y ∈ Y ∧ V0 = Vof y) y0 Hp).
We prove the intermediate claim Hpick: pickY V0 ∈ Y.
An exact proof term for the current goal is (andEL (pickY V0 ∈ Y) (V0 = Vof (pickY V0)) HpickY).
We prove the intermediate claim HV0rep: V0 = Vof (pickY V0).
An exact proof term for the current goal is (andER (pickY V0 ∈ Y) (V0 = Vof (pickY V0)) HpickY).
We prove the intermediate claim HUof: (Uof (pickY V0)) ∈ Tx ∧ x ∈ (Uof (pickY V0)) ∧ (Uof (pickY V0)) ∩ (Vof (pickY V0)) = Empty.
An exact proof term for the current goal is (Uof_props (pickY V0) Hpick).
We prove the intermediate claim HUofdisj: (Uof (pickY V0)) ∩ (Vof (pickY V0)) = Empty.
An exact proof term for the current goal is (andER ((Uof (pickY V0)) ∈ Tx ∧ x ∈ (Uof (pickY V0))) ((Uof (pickY V0)) ∩ (Vof (pickY V0)) = Empty) HUof).
We prove the intermediate claim HzUof: z ∈ (Uof (pickY V0)).
We prove the intermediate claim Hall: ∀T : set, T ∈ UFam → z ∈ T.
An exact proof term for the current goal is (SepE2 X (λz0 : set ⇒ ∀T : set, T ∈ UFam → z0 ∈ T) z HzU).
Apply Hall to the current goal.
An exact proof term for the current goal is (ReplI G (λV1 : set ⇒ Uof (pickY V1)) V0 HV0G).
We prove the intermediate claim HzVof: z ∈ (Vof (pickY V0)).
rewrite the current goal using HV0rep (from right to left) at position 1.
An exact proof term for the current goal is HzV0.
We prove the intermediate claim HzInt: z ∈ (Uof (pickY V0)) ∩ (Vof (pickY V0)).
An exact proof term for the current goal is (binintersectI (Uof (pickY V0)) (Vof (pickY V0)) z HzUof HzVof).
We prove the intermediate claim HzEmpty: z ∈ Empty.
rewrite the current goal using HUofdisj (from right to left) at position 1.
An exact proof term for the current goal is HzInt.
An exact proof term for the current goal is (EmptyE z HzEmpty False).
We use U to witness the existential quantifier.
We use V to witness the existential quantifier.
We will prove U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ Y ⊆ V ∧ U ∩ V = Empty.
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 HUopen.
An exact proof term for the current goal is HVopen.
An exact proof term for the current goal is HxU.
An exact proof term for the current goal is HYsubV.
An exact proof term for the current goal is HUVdisj.
∎