Let X be given.
Assume HinfX: infinite X.
Assume Htop: topology_on X (infinite_complement_family X).
We will prove False.
We prove the intermediate claim H1: ((infinite_complement_family X ⊆ 𝒫 X ∧ Empty ∈ infinite_complement_family X) ∧ X ∈ infinite_complement_family X) ∧ (∀UFam ∈ 𝒫 (infinite_complement_family X), ⋃ UFam ∈ infinite_complement_family X).
An exact proof term for the current goal is (andEL (((infinite_complement_family X ⊆ 𝒫 X ∧ Empty ∈ infinite_complement_family X) ∧ X ∈ infinite_complement_family X) ∧ (∀UFam ∈ 𝒫 (infinite_complement_family X), ⋃ UFam ∈ infinite_complement_family X)) (∀U ∈ infinite_complement_family X, ∀V ∈ infinite_complement_family X, U ∩ V ∈ infinite_complement_family X) Htop).
We prove the intermediate claim HUnionClosure: ∀UFam ∈ 𝒫 (infinite_complement_family X), ⋃ UFam ∈ infinite_complement_family X.
An exact proof term for the current goal is (andER ((infinite_complement_family X ⊆ 𝒫 X ∧ Empty ∈ infinite_complement_family X) ∧ X ∈ infinite_complement_family X) (∀UFam ∈ 𝒫 (infinite_complement_family X), ⋃ UFam ∈ infinite_complement_family X) H1).
Apply (infinite_nonempty X HinfX) to the current goal.
Let p be given.
Assume HpX: p ∈ X.
Set Y to be the term X ∖ {p}.
Set Fam to be the term {F ∈ 𝒫 Y|finite F}.
We prove the intermediate claim HFamSub: Fam ⊆ infinite_complement_family X.
Let F be given.
Assume HF: F ∈ Fam.
We prove the intermediate claim HFpowY: F ∈ 𝒫 Y.
An exact proof term for the current goal is (SepE1 (𝒫 Y) (λF0 : set ⇒ finite F0) F HF).
We prove the intermediate claim HFsubY: F ⊆ Y.
An exact proof term for the current goal is (PowerE Y F HFpowY).
We prove the intermediate claim HYsubX: Y ⊆ X.
Let x be given.
Assume HxY: x ∈ Y.
An exact proof term for the current goal is (setminusE1 X {p} x HxY).
We prove the intermediate claim HFsubX: F ⊆ X.
An exact proof term for the current goal is (Subq_tra F Y X HFsubY HYsubX).
We prove the intermediate claim HFpowX: F ∈ 𝒫 X.
An exact proof term for the current goal is (PowerI X F HFsubX).
We prove the intermediate claim HfinF: finite F.
An exact proof term for the current goal is (SepE2 (𝒫 Y) (λF0 : set ⇒ finite F0) F HF).
We prove the intermediate claim HinfComp: infinite (X ∖ F).
An exact proof term for the current goal is (infinite_setminus_finite X F HinfX HfinF).
We prove the intermediate claim Hpred: infinite (X ∖ F) ∨ F = Empty ∨ F = X.
Apply orIL to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is HinfComp.
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ infinite (X ∖ U0) ∨ U0 = Empty ∨ U0 = X) F HFpowX Hpred).
We prove the intermediate claim HFamPow: Fam ∈ 𝒫 (infinite_complement_family X).
Apply PowerI to the current goal.
An exact proof term for the current goal is HFamSub.
We prove the intermediate claim HUnionEq: ⋃ Fam = Y.
Apply set_ext to the current goal.
Let x be given.
Assume HxU: x ∈ ⋃ Fam.
We will prove x ∈ Y.
Apply UnionE_impred Fam x HxU to the current goal.
Let F be given.
Assume HxF: x ∈ F.
Assume HF: F ∈ Fam.
We prove the intermediate claim HFpowY: F ∈ 𝒫 Y.
An exact proof term for the current goal is (SepE1 (𝒫 Y) (λF0 : set ⇒ finite F0) F HF).
We prove the intermediate claim HFsubY: F ⊆ Y.
An exact proof term for the current goal is (PowerE Y F HFpowY).
An exact proof term for the current goal is (HFsubY x HxF).
Let x be given.
Assume HxY: x ∈ Y.
We will prove x ∈ ⋃ Fam.
We prove the intermediate claim HxYsub: {x} ⊆ Y.
Let z be given.
Assume Hz: z ∈ {x}.
We will prove z ∈ Y.
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 HxY.
We prove the intermediate claim HxPowY: {x} ∈ 𝒫 Y.
An exact proof term for the current goal is (PowerI Y {x} HxYsub).
We prove the intermediate claim HxFin: finite {x}.
An exact proof term for the current goal is (Sing_finite x).
We prove the intermediate claim HsingFam: {x} ∈ Fam.
An exact proof term for the current goal is (SepI (𝒫 Y) (λF0 : set ⇒ finite F0) {x} HxPowY HxFin).
An exact proof term for the current goal is (UnionI Fam x {x} (SingI x) HsingFam).
We prove the intermediate claim HYneX: ¬ (Y = X).
Assume Heq: Y = X.
We prove the intermediate claim HpY: p ∈ Y.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HpX.
We prove the intermediate claim Hpnot: p ∉ {p}.
An exact proof term for the current goal is (setminusE2 X {p} p HpY).
An exact proof term for the current goal is (Hpnot (SingI p)).
We prove the intermediate claim HYneEmpty: ¬ (Y = Empty).
Assume Heq: Y = Empty.
We prove the intermediate claim HyEx: ∃x : set, x ∈ Y.
An exact proof term for the current goal is (infinite_setminus_finite_nonempty X {p} HinfX (Sing_finite p)).
Apply HyEx to the current goal.
Let x be given.
Assume HxY.
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HxY.
An exact proof term for the current goal is (EmptyE x HxE).
We prove the intermediate claim HnotOpenY: ¬ (Y ∈ infinite_complement_family X).
Assume HYopen: Y ∈ infinite_complement_family X.
We prove the intermediate claim HYdisj: infinite (X ∖ Y) ∨ Y = Empty ∨ Y = X.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ infinite (X ∖ U0) ∨ U0 = Empty ∨ U0 = X) Y HYopen).
Apply HYdisj to the current goal.
Assume Hleft: infinite (X ∖ Y) ∨ Y = Empty.
Apply Hleft to the current goal.
Assume HinfComp: infinite (X ∖ Y).
We prove the intermediate claim HcompEq: X ∖ Y = {p}.
We prove the intermediate claim HYdef: Y = X ∖ {p}.
Use reflexivity.
rewrite the current goal using HYdef (from left to right).
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ X ∖ (X ∖ {p}).
We will prove x ∈ {p}.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X (X ∖ {p}) x Hx).
We prove the intermediate claim HxnotY: x ∉ X ∖ {p}.
An exact proof term for the current goal is (setminusE2 X (X ∖ {p}) x Hx).
Apply (xm (x ∈ {p})) to the current goal.
Assume HxS.
An exact proof term for the current goal is HxS.
Assume HxnotS: ¬ (x ∈ {p}).
Apply FalseE to the current goal.
Apply HxnotY to the current goal.
An exact proof term for the current goal is (setminusI X {p} x HxX HxnotS).
Let x be given.
Assume Hx: x ∈ {p}.
We will prove x ∈ X ∖ (X ∖ {p}).
We prove the intermediate claim Hxeq: x = p.
An exact proof term for the current goal is (SingE p x Hx).
rewrite the current goal using Hxeq (from left to right).
Apply setminusI to the current goal.
An exact proof term for the current goal is HpX.
Assume HpY: p ∈ X ∖ {p}.
We prove the intermediate claim HpnotS: p ∉ {p}.
An exact proof term for the current goal is (setminusE2 X {p} p HpY).
An exact proof term for the current goal is (HpnotS (SingI p)).
We prove the intermediate claim HinfSing: infinite {p}.
rewrite the current goal using HcompEq (from right to left).
An exact proof term for the current goal is HinfComp.
An exact proof term for the current goal is (HinfSing (Sing_finite p)).
Assume HYemp.
An exact proof term for the current goal is (HYneEmpty HYemp).
Assume HYX.
An exact proof term for the current goal is (HYneX HYX).
We prove the intermediate claim HUnionIn: ⋃ Fam ∈ infinite_complement_family X.
An exact proof term for the current goal is (HUnionClosure Fam HFamPow).
We prove the intermediate claim HYopen: Y ∈ infinite_complement_family X.
rewrite the current goal using HUnionEq (from right to left).
An exact proof term for the current goal is HUnionIn.
An exact proof term for the current goal is (HnotOpenY HYopen).
∎