Let X and Tx be given.
Assume Htop: topology_on X Tx.
We will prove T1_space X Tx ↔ ∀x y : set, x ∈ X → y ∈ X → x ≠ y → (∃U : set, U ∈ Tx ∧ x ∈ U ∧ y ∉ U) ∧ (∃V : set, V ∈ Tx ∧ y ∈ V ∧ x ∉ V).
Apply iffI to the current goal.
Assume HT1: T1_space X Tx.
We will prove ∀x y : set, x ∈ X → y ∈ X → x ≠ y → (∃U : set, U ∈ Tx ∧ x ∈ U ∧ y ∉ U) ∧ (∃V : set, V ∈ Tx ∧ y ∈ V ∧ x ∉ V).
We prove the intermediate claim Hsing_closed: ∀z : set, z ∈ X → closed_in X Tx {z}.
An exact proof term for the current goal is (iffEL (T1_space X Tx) (∀z : set, z ∈ X → closed_in X Tx {z}) (lemma_T1_singletons_closed X Tx Htop) HT1).
Let x and y be given.
Assume HxX: x ∈ X.
Assume HyX: y ∈ X.
Assume Hne: x ≠ y.
We will prove (∃U : set, U ∈ Tx ∧ x ∈ U ∧ y ∉ U) ∧ (∃V : set, V ∈ Tx ∧ y ∈ V ∧ x ∉ V).
Apply andI to the current goal.
We prove the intermediate claim Hcy: closed_in X Tx {y}.
An exact proof term for the current goal is (Hsing_closed y HyX).
We prove the intermediate claim Hcy2: {y} ⊆ X ∧ ∃U ∈ Tx, {y} = X ∖ U.
An exact proof term for the current goal is (andER (topology_on X Tx) ({y} ⊆ X ∧ ∃U ∈ Tx, {y} = X ∖ U) Hcy).
We prove the intermediate claim HexU: ∃U : set, U ∈ Tx ∧ {y} = X ∖ U.
An exact proof term for the current goal is (andER ({y} ⊆ X) (∃U ∈ Tx, {y} = X ∖ U) Hcy2).
Set U to be the term Eps_i (λU0 : set ⇒ U0 ∈ Tx ∧ {y} = X ∖ U0).
We prove the intermediate claim HUprop: U ∈ Tx ∧ {y} = X ∖ U.
An exact proof term for the current goal is (Eps_i_ex (λU0 : set ⇒ U0 ∈ Tx ∧ {y} = X ∖ U0) HexU).
We prove the intermediate claim HUopen: U ∈ Tx.
An exact proof term for the current goal is (andEL (U ∈ Tx) ({y} = X ∖ U) HUprop).
We prove the intermediate claim Heq: {y} = X ∖ U.
An exact proof term for the current goal is (andER (U ∈ Tx) ({y} = X ∖ U) HUprop).
We use U 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 HUopen.
We prove the intermediate claim Hxnoty: x ∉ {y}.
Assume Hxy: x ∈ {y}.
We prove the intermediate claim Hxyeq: x = y.
An exact proof term for the current goal is (SingE y x Hxy).
An exact proof term for the current goal is (Hne Hxyeq).
We prove the intermediate claim Hxnot: x ∉ (X ∖ U).
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hxnoty.
Apply (xm (x ∈ U)) to the current goal.
Assume HxU: x ∈ U.
An exact proof term for the current goal is HxU.
Assume HxnotU: ¬ (x ∈ U).
We prove the intermediate claim HxXU: x ∈ X ∖ U.
An exact proof term for the current goal is (setminusI X U x HxX HxnotU).
An exact proof term for the current goal is (FalseE (Hxnot HxXU) (x ∈ U)).
Assume HyU: y ∈ U.
We prove the intermediate claim HySing: y ∈ {y}.
An exact proof term for the current goal is (SingI y).
We prove the intermediate claim HyXU: y ∈ X ∖ U.
We will prove y ∈ X ∖ U.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HySing.
An exact proof term for the current goal is ((setminusE2 X U y HyXU) HyU).
We prove the intermediate claim Hcx: closed_in X Tx {x}.
An exact proof term for the current goal is (Hsing_closed x HxX).
We prove the intermediate claim Hcx2: {x} ⊆ X ∧ ∃V ∈ Tx, {x} = X ∖ V.
An exact proof term for the current goal is (andER (topology_on X Tx) ({x} ⊆ X ∧ ∃V ∈ Tx, {x} = X ∖ V) Hcx).
We prove the intermediate claim HexV: ∃V : set, V ∈ Tx ∧ {x} = X ∖ V.
An exact proof term for the current goal is (andER ({x} ⊆ X) (∃V ∈ Tx, {x} = X ∖ V) Hcx2).
Set V to be the term Eps_i (λV0 : set ⇒ V0 ∈ Tx ∧ {x} = X ∖ V0).
We prove the intermediate claim HVprop: V ∈ Tx ∧ {x} = X ∖ V.
An exact proof term for the current goal is (Eps_i_ex (λV0 : set ⇒ V0 ∈ Tx ∧ {x} = X ∖ V0) HexV).
We prove the intermediate claim HVopen: V ∈ Tx.
An exact proof term for the current goal is (andEL (V ∈ Tx) ({x} = X ∖ V) HVprop).
We prove the intermediate claim Heq: {x} = X ∖ V.
An exact proof term for the current goal is (andER (V ∈ Tx) ({x} = X ∖ V) HVprop).
We use V 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 HVopen.
We prove the intermediate claim Hynotx: y ∉ {x}.
Assume Hyx: y ∈ {x}.
We prove the intermediate claim Hyxeq: y = x.
An exact proof term for the current goal is (SingE x y Hyx).
We prove the intermediate claim Hxyeq: x = y.
rewrite the current goal using Hyxeq (from left to right).
Use reflexivity.
An exact proof term for the current goal is (Hne Hxyeq).
We prove the intermediate claim Hynot: y ∉ (X ∖ V).
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hynotx.
Apply (xm (y ∈ V)) to the current goal.
Assume HyV: y ∈ V.
An exact proof term for the current goal is HyV.
Assume HynotV: ¬ (y ∈ V).
We prove the intermediate claim HyXV: y ∈ X ∖ V.
An exact proof term for the current goal is (setminusI X V y HyX HynotV).
An exact proof term for the current goal is (FalseE (Hynot HyXV) (y ∈ V)).
Assume HxV: x ∈ V.
We prove the intermediate claim HxSing: x ∈ {x}.
An exact proof term for the current goal is (SingI x).
We prove the intermediate claim HxXV: x ∈ X ∖ V.
We will prove x ∈ X ∖ V.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HxSing.
An exact proof term for the current goal is ((setminusE2 X V x HxXV) HxV).
Assume Hsep: ∀x y : set, x ∈ X → y ∈ X → x ≠ y → (∃U : set, U ∈ Tx ∧ x ∈ U ∧ y ∉ U) ∧ (∃V : set, V ∈ Tx ∧ y ∈ V ∧ x ∉ V).
We will prove T1_space X Tx.
Apply (iffER (T1_space X Tx) (∀z : set, z ∈ X → closed_in X Tx {z}) (lemma_T1_singletons_closed X Tx Htop)) to the current goal.
We will prove ∀z : set, z ∈ X → closed_in X Tx {z}.
Let x be given.
Assume HxX: x ∈ X.
We will prove closed_in X Tx {x}.
Set UFam to be the term {U ∈ Tx|x ∉ U}.
We prove the intermediate claim HUnionOpen: ⋃ UFam ∈ Tx.
We prove the intermediate claim HUFamSub: UFam ⊆ Tx.
Let U be given.
Assume HU: U ∈ UFam.
An exact proof term for the current goal is (SepE1 Tx (λU0 : set ⇒ x ∉ U0) U HU).
An exact proof term for the current goal is (topology_union_closed X Tx UFam Htop HUFamSub).
We prove the intermediate claim HUnionEq: ⋃ UFam = X ∖ {x}.
Apply set_ext to the current goal.
Let y be given.
Assume HyU: y ∈ ⋃ UFam.
We will prove y ∈ X ∖ {x}.
We prove the intermediate claim HyUex: ∃W : set, y ∈ W ∧ W ∈ UFam.
An exact proof term for the current goal is (UnionE UFam y HyU).
Set U to be the term Eps_i (λU0 : set ⇒ y ∈ U0 ∧ U0 ∈ UFam).
We prove the intermediate claim HUprop: y ∈ U ∧ U ∈ UFam.
An exact proof term for the current goal is (Eps_i_ex (λU0 : set ⇒ y ∈ U0 ∧ U0 ∈ UFam) HyUex).
We prove the intermediate claim HyU0: y ∈ U.
An exact proof term for the current goal is (andEL (y ∈ U) (U ∈ UFam) HUprop).
We prove the intermediate claim HUin: U ∈ UFam.
An exact proof term for the current goal is (andER (y ∈ U) (U ∈ UFam) HUprop).
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (SepE1 Tx (λU0 : set ⇒ x ∉ U0) U HUin).
We prove the intermediate claim HUSubX: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U Htop HUinTx).
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HUSubX y HyU0).
We prove the intermediate claim Hynotx: y ∉ {x}.
Assume Hyx: y ∈ {x}.
We prove the intermediate claim Hyxeq: y = x.
An exact proof term for the current goal is (SingE x y Hyx).
We prove the intermediate claim HxnotU: x ∉ U.
An exact proof term for the current goal is (SepE2 Tx (λU0 : set ⇒ x ∉ U0) U HUin).
We prove the intermediate claim HynotU: y ∉ U.
Assume HyU1: y ∈ U.
We prove the intermediate claim Hxy: x = y.
We will prove x = y.
Use symmetry.
An exact proof term for the current goal is Hyxeq.
We prove the intermediate claim HxU1: x ∈ U.
We will prove x ∈ U.
rewrite the current goal using Hxy (from left to right) at position 1.
An exact proof term for the current goal is HyU1.
An exact proof term for the current goal is (HxnotU HxU1).
An exact proof term for the current goal is (HynotU HyU0).
An exact proof term for the current goal is (setminusI X {x} y HyX Hynotx).
Let y be given.
Assume HyXx: y ∈ X ∖ {x}.
We will prove y ∈ ⋃ UFam.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (setminusE1 X {x} y HyXx).
We prove the intermediate claim Hynot: y ∉ {x}.
An exact proof term for the current goal is (setminusE2 X {x} y HyXx).
We prove the intermediate claim Hyne: y ≠ x.
Assume Heq.
We prove the intermediate claim Hyx: y ∈ {x}.
We will prove y ∈ {x}.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (SingI x).
An exact proof term for the current goal is (Hynot Hyx).
We prove the intermediate claim Hsep_yx: ∃V : set, V ∈ Tx ∧ y ∈ V ∧ x ∉ V.
An exact proof term for the current goal is (andEL (∃V : set, V ∈ Tx ∧ y ∈ V ∧ x ∉ V) (∃U : set, U ∈ Tx ∧ x ∈ U ∧ y ∉ U) (Hsep y x HyX HxX Hyne)).
Set V to be the term Eps_i (λV0 : set ⇒ V0 ∈ Tx ∧ y ∈ V0 ∧ x ∉ V0).
We prove the intermediate claim HVprop: V ∈ Tx ∧ y ∈ V ∧ x ∉ V.
An exact proof term for the current goal is (Eps_i_ex (λV0 : set ⇒ V0 ∈ Tx ∧ y ∈ V0 ∧ x ∉ V0) Hsep_yx).
We prove the intermediate claim HVleft: V ∈ Tx ∧ y ∈ V.
An exact proof term for the current goal is (andEL (V ∈ Tx ∧ y ∈ V) (x ∉ V) HVprop).
We prove the intermediate claim HVinTx: V ∈ Tx.
An exact proof term for the current goal is (andEL (V ∈ Tx) (y ∈ V) HVleft).
We prove the intermediate claim HyV: y ∈ V.
An exact proof term for the current goal is (andER (V ∈ Tx) (y ∈ V) HVleft).
We prove the intermediate claim HxnotV: x ∉ V.
An exact proof term for the current goal is (andER (V ∈ Tx ∧ y ∈ V) (x ∉ V) HVprop).
We prove the intermediate claim HVinFam: V ∈ UFam.
An exact proof term for the current goal is (SepI Tx (λU0 : set ⇒ x ∉ U0) V HVinTx HxnotV).
An exact proof term for the current goal is (UnionI UFam y V HyV HVinFam).
We will prove topology_on X Tx ∧ ({x} ⊆ X ∧ ∃U ∈ Tx, {x} = X ∖ U).
Apply andI to the current goal.
An exact proof term for the current goal is Htop.
Apply andI to the current goal.
Let z be given.
Assume Hz: z ∈ {x}.
We prove the intermediate claim Hzeq: z = x.
An exact proof term for the current goal is (SingE x z Hz).
rewrite the current goal using Hzeq (from left to right).
An exact proof term for the current goal is HxX.
We use (⋃ UFam) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HUnionOpen.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ {x}.
We will prove z ∈ X ∖ ⋃ UFam.
We prove the intermediate claim Hzeq: z = x.
An exact proof term for the current goal is (SingE x z Hz).
rewrite the current goal using Hzeq (from left to right).
Apply setminusI to the current goal.
An exact proof term for the current goal is HxX.
Assume Hxin: x ∈ ⋃ UFam.
We prove the intermediate claim Hxin': x ∈ X ∖ {x}.
We will prove x ∈ X ∖ {x}.
rewrite the current goal using HUnionEq (from right to left).
An exact proof term for the current goal is Hxin.
An exact proof term for the current goal is ((setminusE2 X {x} x Hxin') (SingI x)).
Let z be given.
Assume Hz: z ∈ X ∖ ⋃ UFam.
We will prove z ∈ {x}.
We prove the intermediate claim HsingSub: {x} ⊆ X.
Let t be given.
Assume Ht: t ∈ {x}.
We prove the intermediate claim Hteq: t = x.
An exact proof term for the current goal is (SingE x t Ht).
rewrite the current goal using Hteq (from left to right).
An exact proof term for the current goal is HxX.
rewrite the current goal using (setminus_setminus_eq X {x} HsingSub) (from right to left).
rewrite the current goal using HUnionEq (from right to left).
An exact proof term for the current goal is Hz.
∎