Let X be given.
We prove the intermediate claim HEmptyOpen: Empty ∈ finite_complement_topology X.
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ finite (X ∖ U0) ∨ U0 = Empty) Empty (Empty_In_Power X) (orIR (finite (X ∖ Empty)) (Empty = Empty) (λP H ⇒ H))).
We will prove finite_complement_topology X ⊆ 𝒫 X ∧ Empty ∈ finite_complement_topology X ∧ X ∈ finite_complement_topology X ∧ (∀UFam ∈ 𝒫 (finite_complement_topology X), ⋃ UFam ∈ finite_complement_topology X) ∧ (∀U ∈ finite_complement_topology X, ∀V ∈ finite_complement_topology X, U ∩ V ∈ finite_complement_topology X).
Apply and5I to the current goal.
Let U be given.
Assume HU: U ∈ finite_complement_topology X.
An exact proof term for the current goal is (SepE1 (𝒫 X) (λU0 : set ⇒ finite (X ∖ U0) ∨ U0 = Empty) U HU).
An exact proof term for the current goal is HEmptyOpen.
We prove the intermediate claim Hdiff_empty: X ∖ X = Empty.
Apply Empty_Subq_eq to the current goal.
Let x be given.
Assume Hx.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X X x Hx).
We prove the intermediate claim Hxnot: x ∉ X.
An exact proof term for the current goal is (setminusE2 X X x Hx).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hxnot HxX).
We prove the intermediate claim HfinDiff: finite (X ∖ X).
rewrite the current goal using Hdiff_empty (from left to right).
An exact proof term for the current goal is finite_Empty.
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ finite (X ∖ U0) ∨ U0 = Empty) X (Self_In_Power X) (orIL (finite (X ∖ X)) (X = Empty) HfinDiff)).
We will prove ∀UFam ∈ 𝒫 (finite_complement_topology X), ⋃ UFam ∈ finite_complement_topology X.
Let UFam be given.
Assume Hfam: UFam ∈ 𝒫 (finite_complement_topology X).
We prove the intermediate claim Hsub: UFam ⊆ finite_complement_topology X.
An exact proof term for the current goal is (PowerE (finite_complement_topology X) UFam Hfam).
Apply xm (∃U : set, U ∈ UFam ∧ finite (X ∖ U)) to the current goal.
Assume Hex: ∃U : set, U ∈ UFam ∧ finite (X ∖ U).
We prove the intermediate claim HUnionInPower: ⋃ UFam ∈ 𝒫 X.
Apply PowerI X (⋃ UFam) to the current goal.
Let x be given.
Assume HxUnion.
Apply UnionE_impred UFam x HxUnion to the current goal.
Let U be given.
Assume HxU HUin.
We prove the intermediate claim HUinPow: U ∈ 𝒫 X.
An exact proof term for the current goal is (SepE1 (𝒫 X) (λU0 : set ⇒ finite (X ∖ U0) ∨ U0 = Empty) U (Hsub U HUin)).
We prove the intermediate claim HUsub: U ⊆ X.
An exact proof term for the current goal is (PowerE X U HUinPow).
An exact proof term for the current goal is (HUsub x HxU).
We prove the intermediate claim HUnionPred: finite (X ∖ ⋃ UFam) ∨ ⋃ UFam = Empty.
Apply orIL to the current goal.
Apply Hex to the current goal.
Let U be given.
Assume Hpair: U ∈ UFam ∧ finite (X ∖ U).
We prove the intermediate claim HUin: U ∈ UFam.
An exact proof term for the current goal is (andEL (U ∈ UFam) (finite (X ∖ U)) Hpair).
We prove the intermediate claim HUfin: finite (X ∖ U).
An exact proof term for the current goal is (andER (U ∈ UFam) (finite (X ∖ U)) Hpair).
We prove the intermediate claim Hsubset: X ∖ ⋃ UFam ⊆ X ∖ U.
Let x be given.
Assume Hx.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X (⋃ UFam) x Hx).
We prove the intermediate claim HnotUnion: x ∉ ⋃ UFam.
An exact proof term for the current goal is (setminusE2 X (⋃ UFam) x Hx).
We prove the intermediate claim HnotU: x ∉ U.
Assume HxU.
Apply HnotUnion to the current goal.
Apply UnionI UFam x U HxU HUin to the current goal.
Apply setminusI X U x HxX HnotU to the current goal.
An exact proof term for the current goal is (Subq_finite (X ∖ U) HUfin (X ∖ ⋃ UFam) Hsubset).
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ finite (X ∖ U0) ∨ U0 = Empty) (⋃ UFam) HUnionInPower HUnionPred).
Assume Hnone: ¬ ∃U : set, U ∈ UFam ∧ finite (X ∖ U).
We prove the intermediate claim HUnionEmpty: ⋃ UFam = Empty.
Apply Empty_Subq_eq to the current goal.
Let x be given.
Assume HxUnion.
Apply UnionE_impred UFam x HxUnion to the current goal.
Let U be given.
Assume HxU HUin.
We prove the intermediate claim HUdata: finite (X ∖ U) ∨ U = Empty.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ finite (X ∖ U0) ∨ U0 = Empty) U (Hsub U HUin)).
Apply HUdata (x ∈ Empty) to the current goal.
Assume HUfin.
Apply FalseE to the current goal.
Apply Hnone to the current goal.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HUin.
An exact proof term for the current goal is HUfin.
Assume HUempty: U = Empty.
rewrite the current goal using HUempty (from right to left).
An exact proof term for the current goal is HxU.
rewrite the current goal using HUnionEmpty (from left to right).
An exact proof term for the current goal is HEmptyOpen.
We will prove ∀U ∈ finite_complement_topology X, ∀V ∈ finite_complement_topology X, U ∩ V ∈ finite_complement_topology X.
Let U be given.
Assume HU: U ∈ finite_complement_topology X.
Let V be given.
Assume HV: V ∈ finite_complement_topology X.
We prove the intermediate claim HUdata: finite (X ∖ U) ∨ U = Empty.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ finite (X ∖ U0) ∨ U0 = Empty) U HU).
We prove the intermediate claim HVdata: finite (X ∖ V) ∨ V = Empty.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ finite (X ∖ U0) ∨ U0 = Empty) V HV).
Apply HUdata (U ∩ V ∈ finite_complement_topology X) to the current goal.
Assume HUfin.
Apply HVdata (U ∩ V ∈ finite_complement_topology X) to the current goal.
Assume HVfin.
We prove the intermediate claim HcapInPower: U ∩ V ∈ 𝒫 X.
We prove the intermediate claim HUsub: U ⊆ X.
An exact proof term for the current goal is (PowerE X U (SepE1 (𝒫 X) (λU0 : set ⇒ finite (X ∖ U0) ∨ U0 = Empty) U HU)).
Apply PowerI X (U ∩ V) to the current goal.
Let x be given.
Assume HxCap.
Apply binintersectE U V x HxCap to the current goal.
Assume HxU HxV.
An exact proof term for the current goal is (HUsub x HxU).
We prove the intermediate claim HcapPred: finite (X ∖ (U ∩ V)) ∨ U ∩ V = Empty.
Apply orIL to the current goal.
We prove the intermediate claim HfinUnion: finite ((X ∖ U) ∪ (X ∖ V)).
An exact proof term for the current goal is (binunion_finite (X ∖ U) HUfin (X ∖ V) HVfin).
We prove the intermediate claim Hsubset: X ∖ (U ∩ V) ⊆ (X ∖ U) ∪ (X ∖ V).
Let x be given.
Assume Hx.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X (U ∩ V) x Hx).
We prove the intermediate claim HnotCap: x ∉ U ∩ V.
An exact proof term for the current goal is (setminusE2 X (U ∩ V) x Hx).
Apply xm (x ∈ U) to the current goal.
Assume HxU.
We prove the intermediate claim HnotV: x ∉ V.
Assume HxV.
Apply HnotCap to the current goal.
An exact proof term for the current goal is (binintersectI U V x HxU HxV).
Apply binunionI2 (X ∖ U) (X ∖ V) to the current goal.
Apply setminusI X V x HxX HnotV to the current goal.
Assume HnotU.
Apply binunionI1 (X ∖ U) (X ∖ V) to the current goal.
Apply setminusI X U x HxX HnotU to the current goal.
An exact proof term for the current goal is (Subq_finite ((X ∖ U) ∪ (X ∖ V)) HfinUnion (X ∖ (U ∩ V)) Hsubset).
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ finite (X ∖ U0) ∨ U0 = Empty) (U ∩ V) HcapInPower HcapPred).
Assume HVempty: V = Empty.
We prove the intermediate claim Hcap_empty: U ∩ V = Empty.
rewrite the current goal using HVempty (from left to right).
Apply Empty_Subq_eq to the current goal.
An exact proof term for the current goal is (binintersect_Subq_2 U Empty).
rewrite the current goal using Hcap_empty (from left to right).
An exact proof term for the current goal is HEmptyOpen.
Assume HUempty: U = Empty.
We prove the intermediate claim Hcap_empty: U ∩ V = Empty.
rewrite the current goal using HUempty (from left to right).
Apply Empty_Subq_eq to the current goal.
An exact proof term for the current goal is (binintersect_Subq_1 Empty V).
rewrite the current goal using Hcap_empty (from left to right).
An exact proof term for the current goal is HEmptyOpen.
∎