Let X, Tx and A be given.
Assume Hnorm: normal_space X Tx.
Assume HAcl: closed_in X Tx A.
Set Ta to be the term subspace_topology X Tx A.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (normal_space_topology_on X Tx Hnorm).
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 Hone: one_point_sets_closed X Tx.
An exact proof term for the current goal is (andEL (one_point_sets_closed X Tx) (∀A0 B0 : set, closed_in X Tx A0 → closed_in X Tx B0 → A0 ∩ B0 = Empty → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A0 ⊆ U ∧ B0 ⊆ V ∧ U ∩ V = Empty) Hnorm).
We prove the intermediate claim Hsep: ∀A0 B0 : set, closed_in X Tx A0 → closed_in X Tx B0 → A0 ∩ B0 = Empty → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A0 ⊆ U ∧ B0 ⊆ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (andER (one_point_sets_closed X Tx) (∀A0 B0 : set, closed_in X Tx A0 → closed_in X Tx B0 → A0 ∩ B0 = Empty → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A0 ⊆ U ∧ B0 ⊆ V ∧ U ∩ V = Empty) Hnorm).
We will prove one_point_sets_closed A Ta ∧ ∀C D : set, closed_in A Ta C → closed_in A Ta D → C ∩ D = Empty → ∃U V : set, U ∈ Ta ∧ V ∈ Ta ∧ C ⊆ U ∧ D ⊆ V ∧ U ∩ V = Empty.
Apply andI to the current goal.
We will prove topology_on A Ta ∧ ∀x : set, x ∈ A → closed_in A Ta {x}.
Apply andI to the current goal.
An exact proof term for the current goal is (subspace_topology_is_topology X Tx A HTx HAsubX).
Let x be given.
Assume HxA: x ∈ A.
We will prove closed_in A Ta {x}.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
We prove the intermediate claim HsingAll: ∀y : set, y ∈ X → closed_in X Tx {y}.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀y : set, y ∈ X → closed_in X Tx {y}) Hone).
We prove the intermediate claim HsingClosedX: closed_in X Tx {x}.
An exact proof term for the current goal is (HsingAll x HxX).
Apply (iffER (closed_in A Ta {x}) (∃C0 : set, closed_in X Tx C0 ∧ {x} = C0 ∩ A) (closed_in_subspace_iff_intersection X Tx A {x} HTx HAsubX)) to the current goal.
We use {x} to witness the existential quantifier.
We will prove closed_in X Tx {x} ∧ {x} = {x} ∩ A.
Apply andI to the current goal.
An exact proof term for the current goal is HsingClosedX.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ {x}.
We will prove y ∈ {x} ∩ A.
We prove the intermediate claim HyEq: y = x.
An exact proof term for the current goal is (SingE x y Hy).
We prove the intermediate claim HyA: y ∈ A.
rewrite the current goal using HyEq (from left to right).
An exact proof term for the current goal is HxA.
An exact proof term for the current goal is (binintersectI {x} A y Hy HyA).
Let y be given.
Assume Hy: y ∈ {x} ∩ A.
We will prove y ∈ {x}.
An exact proof term for the current goal is (binintersectE1 {x} A y Hy).
Let C and D be given.
Assume HCcl: closed_in A Ta C.
Assume HDcl: closed_in A Ta D.
Assume Hdisj: C ∩ D = Empty.
We will prove ∃U V : set, U ∈ Ta ∧ V ∈ Ta ∧ C ⊆ U ∧ D ⊆ V ∧ U ∩ V = Empty.
We prove the intermediate claim HCclX: closed_in X Tx C.
An exact proof term for the current goal is (ex17_2_closed_in_closed_subspace X Tx A C HAcl HCcl).
We prove the intermediate claim HDclX: closed_in X Tx D.
An exact proof term for the current goal is (ex17_2_closed_in_closed_subspace X Tx A D HAcl HDcl).
Apply (Hsep C D HCclX HDclX Hdisj) to the current goal.
Let U0 be given.
Assume HU0.
Apply HU0 to the current goal.
Let V0 be given.
Assume HUV0.
We use (U0 ∩ A) to witness the existential quantifier.
We use (V0 ∩ A) to witness the existential quantifier.
We prove the intermediate claim H1234: ((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ C ⊆ U0) ∧ D ⊆ V0.
An exact proof term for the current goal is (andEL (((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ C ⊆ U0) ∧ D ⊆ V0) (U0 ∩ V0 = Empty) HUV0).
We prove the intermediate claim H5: U0 ∩ V0 = Empty.
An exact proof term for the current goal is (andER (((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ C ⊆ U0) ∧ D ⊆ V0) (U0 ∩ V0 = Empty) HUV0).
We prove the intermediate claim H123: (U0 ∈ Tx ∧ V0 ∈ Tx) ∧ C ⊆ U0.
An exact proof term for the current goal is (andEL ((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ C ⊆ U0) (D ⊆ V0) H1234).
We prove the intermediate claim H4: D ⊆ V0.
An exact proof term for the current goal is (andER ((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ C ⊆ U0) (D ⊆ V0) H1234).
We prove the intermediate claim H12: U0 ∈ Tx ∧ V0 ∈ Tx.
An exact proof term for the current goal is (andEL (U0 ∈ Tx ∧ V0 ∈ Tx) (C ⊆ U0) H123).
We prove the intermediate claim H3: C ⊆ U0.
An exact proof term for the current goal is (andER (U0 ∈ Tx ∧ V0 ∈ Tx) (C ⊆ U0) H123).
We prove the intermediate claim HU0Tx: U0 ∈ Tx.
An exact proof term for the current goal is (andEL (U0 ∈ Tx) (V0 ∈ Tx) H12).
We prove the intermediate claim HV0Tx: V0 ∈ Tx.
An exact proof term for the current goal is (andER (U0 ∈ Tx) (V0 ∈ Tx) H12).
We will prove (U0 ∩ A) ∈ Ta ∧ V0 ∩ A ∈ Ta ∧ C ⊆ U0 ∩ A ∧ D ⊆ V0 ∩ A ∧ (U0 ∩ A) ∩ (V0 ∩ A) = 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 (subspace_topologyI X Tx A U0 HU0Tx).
An exact proof term for the current goal is (subspace_topologyI X Tx A V0 HV0Tx).
We will prove C ⊆ U0 ∩ A.
We prove the intermediate claim HCsubA: C ⊆ A.
An exact proof term for the current goal is (closed_in_subset A Ta C HCcl).
Let x be given.
Assume HxC: x ∈ C.
We will prove x ∈ U0 ∩ A.
We prove the intermediate claim HxU0: x ∈ U0.
An exact proof term for the current goal is (H3 x HxC).
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (HCsubA x HxC).
An exact proof term for the current goal is (binintersectI U0 A x HxU0 HxA).
We will prove D ⊆ V0 ∩ A.
We prove the intermediate claim HDsubA: D ⊆ A.
An exact proof term for the current goal is (closed_in_subset A Ta D HDcl).
Let x be given.
Assume HxD: x ∈ D.
We will prove x ∈ V0 ∩ A.
We prove the intermediate claim HxV0: x ∈ V0.
An exact proof term for the current goal is (H4 x HxD).
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (HDsubA x HxD).
An exact proof term for the current goal is (binintersectI V0 A x HxV0 HxA).
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ (U0 ∩ A) ∩ (V0 ∩ A).
We will prove x ∈ Empty.
We prove the intermediate claim HxU: x ∈ U0 ∩ A.
An exact proof term for the current goal is (binintersectE1 (U0 ∩ A) (V0 ∩ A) x Hx).
We prove the intermediate claim HxV: x ∈ V0 ∩ A.
An exact proof term for the current goal is (binintersectE2 (U0 ∩ A) (V0 ∩ A) x Hx).
We prove the intermediate claim HxU0: x ∈ U0.
An exact proof term for the current goal is (binintersectE1 U0 A x HxU).
We prove the intermediate claim HxV0: x ∈ V0.
An exact proof term for the current goal is (binintersectE1 V0 A x HxV).
We prove the intermediate claim HxUV: x ∈ U0 ∩ V0.
An exact proof term for the current goal is (binintersectI U0 V0 x HxU0 HxV0).
rewrite the current goal using H5 (from right to left).
An exact proof term for the current goal is HxUV.
Let x be given.
Assume Hx: x ∈ Empty.
We will prove x ∈ (U0 ∩ A) ∩ (V0 ∩ A).
An exact proof term for the current goal is (EmptyE x Hx (x ∈ (U0 ∩ A) ∩ (V0 ∩ A))).
∎