Let X and U be given.
Assume HUsub: U ⊆ X.
Assume HUne: U ≠ Empty.
Assume HUnX: U ≠ X.
We will prove separation_of X U (X ∖ U).
We prove the intermediate claim HUpow: U ∈ 𝒫 X.
An exact proof term for the current goal is (PowerI X U HUsub).
We prove the intermediate claim HcompSubX: X ∖ U ⊆ X.
An exact proof term for the current goal is (setminus_Subq X U).
We prove the intermediate claim HcompPower: (X ∖ U) ∈ 𝒫 X.
An exact proof term for the current goal is (PowerI X (X ∖ U) HcompSubX).
We prove the intermediate claim Hdisjoint: U ∩ (X ∖ U) = Empty.
Apply Empty_eq to the current goal.
Let x be given.
Assume Hx: x ∈ U ∩ (X ∖ U).
Apply (binintersectE U (X ∖ U) x Hx) to the current goal.
Assume HxU: x ∈ U.
Assume HxComp: x ∈ X ∖ U.
Apply (setminusE X U x HxComp) to the current goal.
Assume _.
Assume HxNotU: x ∉ U.
An exact proof term for the current goal is (HxNotU HxU).
We prove the intermediate claim HcompNe: (X ∖ U) ≠ Empty.
Assume Heq: X ∖ U = Empty.
We prove the intermediate claim HUeqX: U = X.
Apply set_ext to the current goal.
An exact proof term for the current goal is HUsub.
Let x be given.
Assume HxX: x ∈ X.
Apply (xm (x ∈ U)) to the current goal.
Assume HxU.
An exact proof term for the current goal is HxU.
Assume HxNotU.
We prove the intermediate claim Hxcomp: x ∈ X ∖ U.
An exact proof term for the current goal is (setminusI X U x HxX HxNotU).
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 ∈ U.
An exact proof term for the current goal is (FalseE (EmptyE x HxEmpty) (x ∈ U)).
An exact proof term for the current goal is (HUnX HUeqX).
We prove the intermediate claim Hunion: U ∪ (X ∖ U) = X.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ U ∪ (X ∖ U).
Apply (binunionE U (X ∖ U) x Hx) to the current goal.
Assume HxU.
An exact proof term for the current goal is (HUsub x HxU).
Assume HxComp.
An exact proof term for the current goal is (setminusE1 X U x HxComp).
Let x be given.
Assume HxX: x ∈ X.
Apply (xm (x ∈ U)) to the current goal.
Assume HxU.
An exact proof term for the current goal is (binunionI1 U (X ∖ U) x HxU).
Assume HxNotU.
An exact proof term for the current goal is (binunionI2 U (X ∖ U) x (setminusI X U x HxX HxNotU)).
We will prove U ∈ 𝒫 X ∧ (X ∖ U) ∈ 𝒫 X ∧ U ∩ (X ∖ U) = Empty ∧ U ≠ Empty ∧ (X ∖ U) ≠ Empty ∧ U ∪ (X ∖ U) = 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 HUpow.
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 HUne.
An exact proof term for the current goal is HcompNe.
An exact proof term for the current goal is Hunion.
∎