We prove the intermediate claim HXomega: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We use ω to witness the existential quantifier.
We use (finite_complement_topology ω) to witness the existential quantifier.
Set X to be the term ω.
Set Tx to be the term finite_complement_topology ω.
Set Fam to be the term {{n}|n ∈ X ∖ {0}}.
We use Fam to witness the existential quantifier.
We will prove topology_on X Tx ∧ (∀A : set, A ∈ Fam → A ⊆ X) ∧ ¬ (closure_of X Tx (⋃ Fam) ⊆ ⋃ {closure_of X Tx A|A ∈ Fam}).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (finite_complement_topology_on X).
Let A be given.
Assume HA: A ∈ Fam.
We will prove A ⊆ X.
Apply (ReplE (X ∖ {0}) (λn : set ⇒ {n}) A HA) to the current goal.
Let n be given.
Assume Hnconj.
We prove the intermediate claim HninX0: n ∈ X ∖ {0}.
An exact proof term for the current goal is (andEL (n ∈ X ∖ {0}) (A = {n}) Hnconj).
We prove the intermediate claim HAeq: A = {n}.
An exact proof term for the current goal is (andER (n ∈ X ∖ {0}) (A = {n}) Hnconj).
rewrite the current goal using HAeq (from left to right).
Let x be given.
Assume Hx: x ∈ {n}.
We prove the intermediate claim HxEq: x = n.
An exact proof term for the current goal is (SingE n x Hx).
rewrite the current goal using HxEq (from left to right).
An exact proof term for the current goal is (setminusE1 X {0} n HninX0).
We will prove ¬ (closure_of X Tx (⋃ Fam) ⊆ ⋃ {closure_of X Tx A|A ∈ Fam}).
Assume Hsub: closure_of X Tx (⋃ Fam) ⊆ ⋃ {closure_of X Tx A|A ∈ Fam}.
Set ClFam to be the term {closure_of X Tx A|A ∈ Fam}.
We prove the intermediate claim Htop: topology_on X Tx.
An exact proof term for the current goal is (finite_complement_topology_on X).
We prove the intermediate claim HUnionEq: ⋃ Fam = X ∖ {0}.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ ⋃ Fam.
We will prove x ∈ X ∖ {0}.
Apply (UnionE_impred Fam x Hx) to the current goal.
Let A be given.
Assume HxA.
Assume HAFam.
Apply (ReplE (X ∖ {0}) (λn : set ⇒ {n}) A HAFam) to the current goal.
Let n be given.
Assume Hnconj.
We prove the intermediate claim HninX0: n ∈ X ∖ {0}.
An exact proof term for the current goal is (andEL (n ∈ X ∖ {0}) (A = {n}) Hnconj).
We prove the intermediate claim HAeq: A = {n}.
An exact proof term for the current goal is (andER (n ∈ X ∖ {0}) (A = {n}) Hnconj).
We prove the intermediate claim HxEq: x = n.
We prove the intermediate claim HxSing: x ∈ {n}.
rewrite the current goal using HAeq (from right to left).
An exact proof term for the current goal is HxA.
An exact proof term for the current goal is (SingE n x HxSing).
rewrite the current goal using HxEq (from left to right).
An exact proof term for the current goal is HninX0.
Let x be given.
Assume Hx: x ∈ X ∖ {0}.
We will prove x ∈ ⋃ Fam.
We prove the intermediate claim HSingFam: {x} ∈ Fam.
An exact proof term for the current goal is (ReplI (X ∖ {0}) (λn : set ⇒ {n}) x Hx).
An exact proof term for the current goal is (UnionI Fam x {x} (SingI x) HSingFam).
We prove the intermediate claim HsubXX: X ⊆ X.
Let x be given.
Assume Hx: x ∈ X.
An exact proof term for the current goal is Hx.
We prove the intermediate claim Hatleast: atleastp ω X.
An exact proof term for the current goal is (Subq_atleastp ω X HsubXX).
We prove the intermediate claim HinfX: infinite X.
An exact proof term for the current goal is (atleastp_omega_infinite X Hatleast).
We prove the intermediate claim HinfUnion: infinite (⋃ Fam).
rewrite the current goal using HUnionEq (from left to right).
An exact proof term for the current goal is (infinite_remove1 X HinfX 0).
We prove the intermediate claim H0in_closure: 0 ∈ closure_of X Tx (⋃ Fam).
Apply (iffER (0 ∈ closure_of X Tx (⋃ Fam)) (∀U ∈ Tx, 0 ∈ U → U ∩ (⋃ Fam) ≠ Empty) (closure_characterization X Tx (⋃ Fam) 0 Htop HXomega)) to the current goal.
Let U be given.
Assume HU: U ∈ Tx.
Assume H0U: 0 ∈ U.
We will prove U ∩ (⋃ Fam) ≠ Empty.
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).
Apply HUdata (U ∩ (⋃ Fam) ≠ Empty) to the current goal.
Assume HUfin: finite (X ∖ U).
We will prove U ∩ (⋃ Fam) ≠ Empty.
Assume Hinter: U ∩ (⋃ Fam) = Empty.
We prove the intermediate claim Hsub: ⋃ Fam ⊆ X ∖ U.
Let x be given.
Assume HxUFam: x ∈ ⋃ Fam.
We will prove x ∈ X ∖ U.
We prove the intermediate claim HxX: x ∈ X.
Apply (UnionE_impred Fam x HxUFam) to the current goal.
Let A be given.
Assume HxA.
Assume HAFam.
Apply (ReplE (X ∖ {0}) (λn : set ⇒ {n}) A HAFam) to the current goal.
Let n be given.
Assume Hnconj.
We prove the intermediate claim HninX0: n ∈ X ∖ {0}.
An exact proof term for the current goal is (andEL (n ∈ X ∖ {0}) (A = {n}) Hnconj).
We prove the intermediate claim HAeq: A = {n}.
An exact proof term for the current goal is (andER (n ∈ X ∖ {0}) (A = {n}) Hnconj).
We prove the intermediate claim HxEq: x = n.
We prove the intermediate claim HxSing: x ∈ {n}.
rewrite the current goal using HAeq (from right to left).
An exact proof term for the current goal is HxA.
An exact proof term for the current goal is (SingE n x HxSing).
rewrite the current goal using HxEq (from left to right).
An exact proof term for the current goal is (setminusE1 X {0} n HninX0).
We prove the intermediate claim HxnotU: x ∉ U.
Assume HxU: x ∈ U.
We prove the intermediate claim HxInter: x ∈ U ∩ (⋃ Fam).
Apply binintersectI to the current goal.
An exact proof term for the current goal is HxU.
An exact proof term for the current goal is HxUFam.
We prove the intermediate claim HxEmpty: x ∈ Empty.
rewrite the current goal using Hinter (from right to left).
An exact proof term for the current goal is HxInter.
An exact proof term for the current goal is (EmptyE x HxEmpty).
An exact proof term for the current goal is (setminusI X U x HxX HxnotU).
We prove the intermediate claim HfinUFam: finite (⋃ Fam).
An exact proof term for the current goal is (Subq_finite (X ∖ U) HUfin (⋃ Fam) Hsub).
Apply HinfUnion to the current goal.
An exact proof term for the current goal is HfinUFam.
Assume HUempty: U = Empty.
We will prove U ∩ (⋃ Fam) ≠ Empty.
Assume Hinter: U ∩ (⋃ Fam) = Empty.
We prove the intermediate claim HUne: U ≠ Empty.
An exact proof term for the current goal is (elem_implies_nonempty U 0 H0U).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HUne HUempty).
We prove the intermediate claim H0not_union_closures: 0 ∉ ⋃ ClFam.
Assume H0in: 0 ∈ ⋃ ClFam.
Apply (UnionE_impred ClFam 0 H0in) to the current goal.
Let W be given.
Assume H0W: 0 ∈ W.
Assume HWCl: W ∈ ClFam.
Apply (ReplE Fam (λA : set ⇒ closure_of X Tx A) W HWCl) to the current goal.
Let A be given.
Assume HAconj.
We prove the intermediate claim HAFam: A ∈ Fam.
An exact proof term for the current goal is (andEL (A ∈ Fam) (W = closure_of X Tx A) HAconj).
We prove the intermediate claim HWeq: W = closure_of X Tx A.
An exact proof term for the current goal is (andER (A ∈ Fam) (W = closure_of X Tx A) HAconj).
We prove the intermediate claim H0clA: 0 ∈ closure_of X Tx A.
rewrite the current goal using HWeq (from right to left).
An exact proof term for the current goal is H0W.
Apply (ReplE (X ∖ {0}) (λn : set ⇒ {n}) A HAFam) to the current goal.
Let n be given.
Assume Hnconj.
We prove the intermediate claim HninX0: n ∈ X ∖ {0}.
An exact proof term for the current goal is (andEL (n ∈ X ∖ {0}) (A = {n}) Hnconj).
We prove the intermediate claim HAeq: A = {n}.
An exact proof term for the current goal is (andER (n ∈ X ∖ {0}) (A = {n}) Hnconj).
We prove the intermediate claim HninX: n ∈ X.
An exact proof term for the current goal is (setminusE1 X {0} n HninX0).
We prove the intermediate claim HSingSub: {n} ⊆ X.
Let x be given.
Assume Hx: x ∈ {n}.
We prove the intermediate claim HxEq: x = n.
An exact proof term for the current goal is (SingE n x Hx).
rewrite the current goal using HxEq (from left to right).
An exact proof term for the current goal is HninX.
We prove the intermediate claim Hclosed: closed_in X Tx {n}.
We will prove topology_on X Tx ∧ ({n} ⊆ X ∧ ∃U ∈ Tx, {n} = X ∖ U).
Apply andI to the current goal.
An exact proof term for the current goal is Htop.
Apply andI to the current goal.
An exact proof term for the current goal is HSingSub.
We use (X ∖ {n}) to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HUpow: (X ∖ {n}) ∈ 𝒫 X.
An exact proof term for the current goal is (setminus_In_Power X {n}).
We prove the intermediate claim HfinComp: finite (X ∖ (X ∖ {n})).
rewrite the current goal using (setminus_setminus_eq X {n} HSingSub) (from left to right).
An exact proof term for the current goal is (Sing_finite n).
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ finite (X ∖ U0) ∨ U0 = Empty) (X ∖ {n}) HUpow (orIL (finite (X ∖ (X ∖ {n}))) ((X ∖ {n}) = Empty) HfinComp)).
rewrite the current goal using (setminus_setminus_eq X {n} HSingSub) (from left to right).
Use reflexivity.
We prove the intermediate claim Heq_cl: closure_of X Tx {n} = {n}.
An exact proof term for the current goal is (closed_closure_eq X Tx {n} Htop Hclosed).
We prove the intermediate claim H0clSing: 0 ∈ closure_of X Tx {n}.
rewrite the current goal using HAeq (from right to left).
An exact proof term for the current goal is H0clA.
We prove the intermediate claim H0inSing: 0 ∈ {n}.
rewrite the current goal using Heq_cl (from right to left).
An exact proof term for the current goal is H0clSing.
We prove the intermediate claim H0eqn: 0 = n.
An exact proof term for the current goal is (SingE n 0 H0inSing).
We prove the intermediate claim Hn0: n = 0.
rewrite the current goal using H0eqn (from right to left).
Use reflexivity.
We prove the intermediate claim Hnnot0: n ∉ {0}.
An exact proof term for the current goal is (setminusE2 X {0} n HninX0).
We prove the intermediate claim Hnin0: n ∈ {0}.
rewrite the current goal using Hn0 (from left to right).
An exact proof term for the current goal is (SingI 0).
An exact proof term for the current goal is (Hnnot0 Hnin0).
We prove the intermediate claim H0in_right: 0 ∈ ⋃ ClFam.
An exact proof term for the current goal is (Hsub 0 H0in_closure).
An exact proof term for the current goal is (H0not_union_closures H0in_right).
∎