Let X, Tx, U and V be given.
Assume HTx: topology_on X Tx.
Assume HU: U ∈ Tx.
Assume HV: V ∈ Tx.
Assume Hsep: separation_of X U V.
We use U to witness the existential quantifier.
We will prove U ≠ Empty ∧ U ≠ X ∧ open_in X Tx U ∧ closed_in X Tx U.
We prove the intermediate claim H1: (((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty.
An exact proof term for the current goal is (andEL ((((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty) (U ∪ V = X) Hsep).
We prove the intermediate claim H2: ((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) ∧ U ≠ Empty.
An exact proof term for the current goal is (andEL (((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) ∧ U ≠ Empty) (V ≠ Empty) H1).
We prove the intermediate claim HUne: U ≠ Empty.
An exact proof term for the current goal is (andER (((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty)) (U ≠ Empty) H2).
We prove the intermediate claim Hunion: U ∪ V = X.
An exact proof term for the current goal is (andER ((((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty) (U ∪ V = X) Hsep).
We prove the intermediate claim HUneX: U ≠ X.
Assume Heq: U = X.
We prove the intermediate claim HVempty: V = Empty.
Apply Empty_eq to the current goal.
Let x be given.
Assume Hx: x ∈ V.
We prove the intermediate claim HxX: x ∈ X.
rewrite the current goal using Hunion (from right to left).
An exact proof term for the current goal is (binunionI2 U V x Hx).
We prove the intermediate claim HxU: x ∈ U.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HxX.
We prove the intermediate claim Hxdisj: x ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V x HxU Hx).
We prove the intermediate claim Hdisj: U ∩ V = Empty.
An exact proof term for the current goal is (andER (U ∈ 𝒫 X ∧ V ∈ 𝒫 X) (U ∩ V = Empty) (andEL ((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) (U ≠ Empty) H2)).
We prove the intermediate claim Hfalse: x ∈ Empty.
rewrite the current goal using Hdisj (from right to left).
An exact proof term for the current goal is Hxdisj.
An exact proof term for the current goal is (EmptyE x Hfalse).
We prove the intermediate claim HVne: V ≠ Empty.
An exact proof term for the current goal is (andER ((((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) ∧ U ≠ Empty)) (V ≠ Empty) H1).
An exact proof term for the current goal is (HVne HVempty).
We prove the intermediate claim HUopen: open_in X Tx U.
An exact proof term for the current goal is (andI (topology_on X Tx) (U ∈ Tx) HTx HU).
We prove the intermediate claim Hdisj: U ∩ V = Empty.
An exact proof term for the current goal is (andER (U ∈ 𝒫 X ∧ V ∈ 𝒫 X) (U ∩ V = Empty) (andEL ((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) (U ≠ Empty) H2)).
We prove the intermediate claim HUpower: U ∈ 𝒫 X.
An exact proof term for the current goal is (andEL (U ∈ 𝒫 X) (V ∈ 𝒫 X) (andEL (U ∈ 𝒫 X ∧ V ∈ 𝒫 X) (U ∩ V = Empty) (andEL ((U ∈ 𝒫 X ∧ V ∈ 𝒫 X) ∧ U ∩ V = Empty) (U ≠ Empty) H2))).
We prove the intermediate claim HUsubX: U ⊆ X.
An exact proof term for the current goal is (PowerE X U HUpower).
We prove the intermediate claim Heq_comp: U = X ∖ V.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ U.
We will prove x ∈ X ∖ V.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HUsubX x Hx).
We prove the intermediate claim HxnotV: x ∉ V.
Assume HxV: x ∈ V.
We prove the intermediate claim Hxdisj: x ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V x Hx HxV).
We prove the intermediate claim Hfalse: x ∈ Empty.
rewrite the current goal using Hdisj (from right to left).
An exact proof term for the current goal is Hxdisj.
An exact proof term for the current goal is (EmptyE x Hfalse).
An exact proof term for the current goal is (setminusI X V x HxX HxnotV).
Let x be given.
Assume Hx: x ∈ X ∖ V.
We will prove x ∈ U.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X V x Hx).
We prove the intermediate claim HxnotV: x ∉ V.
An exact proof term for the current goal is (setminusE2 X V x Hx).
We prove the intermediate claim HxUnion: x ∈ U ∪ V.
rewrite the current goal using Hunion (from left to right).
An exact proof term for the current goal is HxX.
Apply (binunionE U V x HxUnion) to the current goal.
Assume HxU.
An exact proof term for the current goal is HxU.
Assume HxV.
An exact proof term for the current goal is (FalseE (HxnotV HxV) (x ∈ U)).
We prove the intermediate claim HUclosed: closed_in X Tx U.
We will prove topology_on X Tx ∧ (U ⊆ X ∧ ∃W ∈ Tx, U = X ∖ W).
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Apply andI to the current goal.
An exact proof term for the current goal is HUsubX.
We use V to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HV.
An exact proof term for the current goal is Heq_comp.
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 HUne.
An exact proof term for the current goal is HUneX.
An exact proof term for the current goal is HUopen.
An exact proof term for the current goal is HUclosed.
∎