Let X, Tx and A be given.
Assume HTx: topology_on X Tx.
Assume HAne: A ≠ Empty.
Assume HAneX: A ≠ X.
Assume HAopen: open_in X Tx A.
Assume HAclosed: closed_in X Tx A.
We prove the intermediate claim HATx: A ∈ Tx.
An exact proof term for the current goal is (andER (topology_on X Tx) (A ∈ Tx) HAopen).
We prove the intermediate claim HcompOpen: open_in X Tx (X ∖ A).
An exact proof term for the current goal is (open_of_closed_complement X Tx A HAclosed).
We prove the intermediate claim HcompTx: X ∖ A ∈ Tx.
An exact proof term for the current goal is (andER (topology_on X Tx) ((X ∖ A) ∈ Tx) HcompOpen).
We use A to witness the existential quantifier.
We use (X ∖ A) 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 HATx.
An exact proof term for the current goal is HcompTx.
We will prove separation_of X A (X ∖ A).
We will prove A ∈ 𝒫 X ∧ (X ∖ A) ∈ 𝒫 X ∧ A ∩ (X ∖ A) = Empty ∧ A ≠ Empty ∧ (X ∖ A) ≠ Empty ∧ A ∪ (X ∖ A) = X.
We prove the intermediate claim HAsubX: A ⊆ X.
An exact proof term for the current goal is (open_in_subset X Tx A HAopen).
We prove the intermediate claim HApower: A ∈ 𝒫 X.
An exact proof term for the current goal is (PowerI X A HAsubX).
We prove the intermediate claim HcompSubX: X ∖ A ⊆ X.
An exact proof term for the current goal is (setminus_Subq X A).
We prove the intermediate claim HcompPower: (X ∖ A) ∈ 𝒫 X.
An exact proof term for the current goal is (PowerI X (X ∖ A) HcompSubX).
We prove the intermediate claim Hdisjoint: A ∩ (X ∖ A) = Empty.
Apply Empty_eq to the current goal.
Let x be given.
Assume Hx: x ∈ A ∩ (X ∖ A).
Apply (binintersectE A (X ∖ A) x Hx) to the current goal.
Assume HxA: x ∈ A.
Assume HxComp: x ∈ X ∖ A.
Apply (setminusE X A x HxComp) to the current goal.
Assume _.
Assume HxNotA: x ∉ A.
An exact proof term for the current goal is (HxNotA HxA).
We prove the intermediate claim HcompNe: (X ∖ A) ≠ Empty.
Assume Heq: X ∖ A = Empty.
We prove the intermediate claim HAeqX: A = X.
Apply set_ext to the current goal.
An exact proof term for the current goal is HAsubX.
Let x be given.
Assume HxX: x ∈ X.
Apply (xm (x ∈ A)) to the current goal.
Assume HxA.
An exact proof term for the current goal is HxA.
Assume HxNotA.
We prove the intermediate claim Hxcomp: x ∈ X ∖ A.
An exact proof term for the current goal is (setminusI X A x HxX HxNotA).
We prove the intermediate claim HxEmpty: x ∈ Empty.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hxcomp.
We will prove x ∈ A.
An exact proof term for the current goal is (FalseE (EmptyE x HxEmpty) (x ∈ A)).
An exact proof term for the current goal is (HAneX HAeqX).
We prove the intermediate claim Hunion: A ∪ (X ∖ A) = X.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ A ∪ (X ∖ A).
Apply (binunionE A (X ∖ A) x Hx) to the current goal.
Assume HxA.
An exact proof term for the current goal is (HAsubX x HxA).
Assume HxComp.
An exact proof term for the current goal is (setminusE1 X A x HxComp).
Let x be given.
Assume HxX: x ∈ X.
Apply (xm (x ∈ A)) to the current goal.
Assume HxA.
An exact proof term for the current goal is (binunionI1 A (X ∖ A) x HxA).
Assume HxNotA.
An exact proof term for the current goal is (binunionI2 A (X ∖ A) x (setminusI X A x HxX HxNotA)).
We will prove (((((A ∈ 𝒫 X ∧ (X ∖ A) ∈ 𝒫 X) ∧ A ∩ (X ∖ A) = Empty) ∧ A ≠ Empty) ∧ (X ∖ A) ≠ Empty) ∧ A ∪ (X ∖ A) = X).
Apply andI to the current goal.
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 HApower.
An exact proof term for the current goal is HcompPower.
An exact proof term for the current goal is Hdisjoint.
An exact proof term for the current goal is HAne.
An exact proof term for the current goal is HcompNe.
An exact proof term for the current goal is Hunion.
∎