Let X, Tx and Fam be given.
Assume HLF: locally_finite_family X Tx Fam.
Assume Hcl: ∀A : set, A ∈ Fam → closed_in X Tx A.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (∀x : set, x ∈ X → ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ Fam ∧ ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S) HLF).
We prove the intermediate claim HTsub: Tx ⊆ 𝒫 X.
An exact proof term for the current goal is (topology_subset_axiom X Tx HTx).
We prove the intermediate claim HUnionSubX: ⋃ Fam ⊆ X.
Let x be given.
Assume HxU: x ∈ ⋃ Fam.
Apply (UnionE Fam x HxU) to the current goal.
Let A be given.
Assume HA: x ∈ A ∧ A ∈ Fam.
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (andEL (x ∈ A) (A ∈ Fam) HA).
We prove the intermediate claim HAFam: A ∈ Fam.
An exact proof term for the current goal is (andER (x ∈ A) (A ∈ Fam) HA).
We prove the intermediate claim HAcl: closed_in X Tx A.
An exact proof term for the current goal is (Hcl A HAFam).
We prove the intermediate claim HAsubX: A ⊆ X.
An exact proof term for the current goal is (andEL (A ⊆ X) (∃U ∈ Tx, A = X ∖ U) (closed_in_package X Tx A HAcl)).
An exact proof term for the current goal is (HAsubX x HxA).
Set U to be the term X ∖ ⋃ Fam.
We prove the intermediate claim Hnbhd: ∀x : set, x ∈ U → ∃V : set, V ∈ Tx ∧ x ∈ V ∧ V ⊆ U.
Let x be given.
Assume HxU: x ∈ U.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X (⋃ Fam) x HxU).
We prove the intermediate claim HexN: ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ Fam ∧ ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀x0 : set, x0 ∈ X → ∃N : set, N ∈ Tx ∧ x0 ∈ N ∧ ∃S : set, finite S ∧ S ⊆ Fam ∧ ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S) HLF x HxX).
Apply HexN to the current goal.
Let N be given.
Assume HNpack: N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ Fam ∧ ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S.
We prove the intermediate claim HNcore: N ∈ Tx ∧ x ∈ N.
An exact proof term for the current goal is (andEL (N ∈ Tx ∧ x ∈ N) (∃S : set, finite S ∧ S ⊆ Fam ∧ ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S) HNpack).
We prove the intermediate claim HNTx: N ∈ Tx.
An exact proof term for the current goal is (andEL (N ∈ Tx) (x ∈ N) HNcore).
We prove the intermediate claim HxN: x ∈ N.
An exact proof term for the current goal is (andER (N ∈ Tx) (x ∈ N) HNcore).
We prove the intermediate claim HexS: ∃S : set, finite S ∧ S ⊆ Fam ∧ ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S.
An exact proof term for the current goal is (andER (N ∈ Tx ∧ x ∈ N) (∃S : set, finite S ∧ S ⊆ Fam ∧ ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S) HNpack).
Apply HexS to the current goal.
Let S be given.
Assume HS: finite S ∧ S ⊆ Fam ∧ ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S.
We prove the intermediate claim HSleft: finite S ∧ S ⊆ Fam.
An exact proof term for the current goal is (andEL (finite S ∧ S ⊆ Fam) (∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S) HS).
We prove the intermediate claim HSfin: finite S.
An exact proof term for the current goal is (andEL (finite S) (S ⊆ Fam) HSleft).
We prove the intermediate claim HSsubFam: S ⊆ Fam.
An exact proof term for the current goal is (andER (finite S) (S ⊆ Fam) HSleft).
We prove the intermediate claim HSprop: ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S.
An exact proof term for the current goal is (andER (finite S ∧ S ⊆ Fam) (∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S) HS).
Set sep_open to be the term λA : set ⇒ Eps_i (λV0 : set ⇒ V0 ∈ Tx ∧ A = X ∖ V0).
Set F to be the term Repl S sep_open.
We prove the intermediate claim HFfin: finite F.
An exact proof term for the current goal is (Repl_finite sep_open S HSfin).
We prove the intermediate claim HFsubTx: F ⊆ Tx.
Let V0 be given.
Assume HV0: V0 ∈ F.
Apply (ReplE_impred S sep_open V0 HV0) to the current goal.
Let A be given.
Assume HA: A ∈ S.
Assume Heq: V0 = sep_open A.
We prove the intermediate claim HAFam: A ∈ Fam.
An exact proof term for the current goal is (HSsubFam A HA).
We prove the intermediate claim HAcl: closed_in X Tx A.
An exact proof term for the current goal is (Hcl A HAFam).
We prove the intermediate claim HexU0: ∃U0 ∈ Tx, A = X ∖ U0.
An exact proof term for the current goal is (closed_in_exists_open_complement X Tx A HAcl).
We prove the intermediate claim Hsep: sep_open A ∈ Tx ∧ A = X ∖ (sep_open A).
An exact proof term for the current goal is (Eps_i_ex (λV1 : set ⇒ V1 ∈ Tx ∧ A = X ∖ V1) HexU0).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (andEL (sep_open A ∈ Tx) (A = X ∖ (sep_open A)) Hsep).
We prove the intermediate claim HFNpow: (F ∪ {N}) ∈ 𝒫 Tx.
Apply PowerI to the current goal.
Let V0 be given.
Assume HV0: V0 ∈ F ∪ {N}.
Apply (binunionE F {N} V0 HV0) to the current goal.
Assume HVF: V0 ∈ F.
An exact proof term for the current goal is (HFsubTx V0 HVF).
Assume HVN: V0 ∈ {N}.
We prove the intermediate claim HeqN: V0 = N.
An exact proof term for the current goal is (SingE N V0 HVN).
rewrite the current goal using HeqN (from left to right).
An exact proof term for the current goal is HNTx.
Set V to be the term intersection_of_family X (F ∪ {N}).
We prove the intermediate claim HVTx: V ∈ Tx.
An exact proof term for the current goal is (finite_intersection_in_topology X Tx (F ∪ {N}) HTx HFNpow (binunion_finite F HFfin {N} (Sing_finite N))).
We prove the intermediate claim HxV: x ∈ V.
Apply (intersection_of_familyI X (F ∪ {N}) x) to the current goal.
An exact proof term for the current goal is HxX.
Let T be given.
Assume HT: T ∈ F ∪ {N}.
Apply (binunionE F {N} T HT) to the current goal.
Assume HTF: T ∈ F.
Apply (ReplE_impred S sep_open T HTF) to the current goal.
Let A be given.
Assume HA: A ∈ S.
Assume HeqT: T = sep_open A.
We prove the intermediate claim HAFam: A ∈ Fam.
An exact proof term for the current goal is (HSsubFam A HA).
We prove the intermediate claim HnotxA: x ∉ A.
Assume HxA: x ∈ A.
We prove the intermediate claim HxUFam: x ∈ ⋃ Fam.
An exact proof term for the current goal is (UnionI Fam x A HxA HAFam).
An exact proof term for the current goal is ((setminusE2 X (⋃ Fam) x HxU) HxUFam False).
We prove the intermediate claim HAcl: closed_in X Tx A.
An exact proof term for the current goal is (Hcl A HAFam).
We prove the intermediate claim HexU0: ∃U0 ∈ Tx, A = X ∖ U0.
An exact proof term for the current goal is (closed_in_exists_open_complement X Tx A HAcl).
We prove the intermediate claim Hsep: sep_open A ∈ Tx ∧ A = X ∖ (sep_open A).
An exact proof term for the current goal is (Eps_i_ex (λV1 : set ⇒ V1 ∈ Tx ∧ A = X ∖ V1) HexU0).
We prove the intermediate claim HAeq: A = X ∖ (sep_open A).
An exact proof term for the current goal is (andER (sep_open A ∈ Tx) (A = X ∖ (sep_open A)) Hsep).
We prove the intermediate claim HxIn: x ∈ sep_open A.
Apply (xm (x ∈ sep_open A)) to the current goal.
Assume HxIn.
An exact proof term for the current goal is HxIn.
Assume HxNot.
Apply FalseE to the current goal.
We prove the intermediate claim HxInA: x ∈ A.
rewrite the current goal using HAeq (from left to right).
An exact proof term for the current goal is (setminusI X (sep_open A) x HxX HxNot).
An exact proof term for the current goal is (HnotxA HxInA False).
rewrite the current goal using HeqT (from left to right).
An exact proof term for the current goal is HxIn.
Assume HTN: T ∈ {N}.
We prove the intermediate claim Heq: T = N.
An exact proof term for the current goal is (SingE N T HTN).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HxN.
We prove the intermediate claim HVsubU: V ⊆ U.
Let y be given.
Assume HyV: y ∈ V.
We will prove y ∈ U.
We prove the intermediate claim HyN: y ∈ N.
We prove the intermediate claim HyT: y ∈ N ∧ N ∈ (F ∪ {N}).
We prove the intermediate claim HNin: N ∈ F ∪ {N}.
An exact proof term for the current goal is (binunionI2 F {N} N (SingI N)).
An exact proof term for the current goal is (andI (y ∈ N) (N ∈ (F ∪ {N})) (intersection_of_familyE2 X (F ∪ {N}) y HyV N HNin) HNin).
An exact proof term for the current goal is (andEL (y ∈ N) (N ∈ (F ∪ {N})) HyT).
Apply (xm (y ∈ ⋃ Fam)) to the current goal.
Assume HyUFam: y ∈ ⋃ Fam.
Apply FalseE to the current goal.
Apply (UnionE Fam y HyUFam) to the current goal.
Let A be given.
Assume HApack: y ∈ A ∧ A ∈ Fam.
We prove the intermediate claim HyA: y ∈ A.
An exact proof term for the current goal is (andEL (y ∈ A) (A ∈ Fam) HApack).
We prove the intermediate claim HAFam: A ∈ Fam.
An exact proof term for the current goal is (andER (y ∈ A) (A ∈ Fam) HApack).
We prove the intermediate claim HyAN: y ∈ A ∩ N.
An exact proof term for the current goal is (binintersectI A N y HyA HyN).
We prove the intermediate claim HAnN: A ∩ N ≠ Empty.
An exact proof term for the current goal is (elem_implies_nonempty (A ∩ N) y HyAN).
We prove the intermediate claim HAinS: A ∈ S.
An exact proof term for the current goal is (HSprop A HAFam HAnN).
We prove the intermediate claim HySep: y ∈ sep_open A.
We prove the intermediate claim HSepIn: sep_open A ∈ F.
An exact proof term for the current goal is (ReplI S sep_open A HAinS).
We prove the intermediate claim HSepInU: sep_open A ∈ (F ∪ {N}).
An exact proof term for the current goal is (binunionI1 F {N} (sep_open A) HSepIn).
An exact proof term for the current goal is (intersection_of_familyE2 X (F ∪ {N}) y HyV (sep_open A) HSepInU).
We prove the intermediate claim HAFam2: A ∈ Fam.
An exact proof term for the current goal is HAFam.
We prove the intermediate claim HAcl: closed_in X Tx A.
An exact proof term for the current goal is (Hcl A HAFam2).
We prove the intermediate claim HexU0: ∃U0 ∈ Tx, A = X ∖ U0.
An exact proof term for the current goal is (closed_in_exists_open_complement X Tx A HAcl).
We prove the intermediate claim Hsep: sep_open A ∈ Tx ∧ A = X ∖ (sep_open A).
An exact proof term for the current goal is (Eps_i_ex (λV1 : set ⇒ V1 ∈ Tx ∧ A = X ∖ V1) HexU0).
We prove the intermediate claim HAeq: A = X ∖ (sep_open A).
An exact proof term for the current goal is (andER (sep_open A ∈ Tx) (A = X ∖ (sep_open A)) Hsep).
We prove the intermediate claim HyNotSep: y ∉ sep_open A.
We prove the intermediate claim HyA': y ∈ X ∖ (sep_open A).
rewrite the current goal using HAeq (from right to left).
An exact proof term for the current goal is HyA.
An exact proof term for the current goal is (setminusE2 X (sep_open A) y HyA').
An exact proof term for the current goal is (HyNotSep HySep False).
Assume HyNotUFam: y ∉ ⋃ Fam.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (intersection_of_familyE1 X (F ∪ {N}) y HyV).
An exact proof term for the current goal is (setminusI X (⋃ Fam) y HyX HyNotUFam).
We use V 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 HVTx.
An exact proof term for the current goal is HxV.
An exact proof term for the current goal is HVsubU.
We prove the intermediate claim HUopen: U ∈ Tx.
Set FamU to be the term {V ∈ Tx|V ⊆ U}.
We prove the intermediate claim HFamU: FamU ∈ 𝒫 Tx.
Apply PowerI to the current goal.
Let V be given.
Assume HV: V ∈ FamU.
An exact proof term for the current goal is (SepE1 Tx (λV0 : set ⇒ V0 ⊆ U) V HV).
We prove the intermediate claim HUeq: U = ⋃ FamU.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ U.
We will prove x ∈ ⋃ FamU.
We prove the intermediate claim HexV: ∃V : set, V ∈ Tx ∧ x ∈ V ∧ V ⊆ U.
An exact proof term for the current goal is (Hnbhd x Hx).
Apply HexV to the current goal.
Let V be given.
Assume HVpack: V ∈ Tx ∧ x ∈ V ∧ V ⊆ U.
We prove the intermediate claim HVleft: V ∈ Tx ∧ x ∈ V.
An exact proof term for the current goal is (andEL (V ∈ Tx ∧ x ∈ V) (V ⊆ U) HVpack).
We prove the intermediate claim HVTx: V ∈ Tx.
An exact proof term for the current goal is (andEL (V ∈ Tx) (x ∈ V) HVleft).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (andER (V ∈ Tx) (x ∈ V) HVleft).
We prove the intermediate claim HVsub: V ⊆ U.
An exact proof term for the current goal is (andER (V ∈ Tx ∧ x ∈ V) (V ⊆ U) HVpack).
We prove the intermediate claim HVFamU: V ∈ FamU.
An exact proof term for the current goal is (SepI Tx (λV0 : set ⇒ V0 ⊆ U) V HVTx HVsub).
An exact proof term for the current goal is (UnionI FamU x V HxV HVFamU).
Let x be given.
Assume Hx: x ∈ ⋃ FamU.
We will prove x ∈ U.
Apply UnionE_impred FamU x Hx to the current goal.
Let V be given.
Assume HxV HVFamU.
We prove the intermediate claim HVsub: V ⊆ U.
An exact proof term for the current goal is (SepE2 Tx (λV0 : set ⇒ V0 ⊆ U) V HVFamU).
An exact proof term for the current goal is (HVsub x HxV).
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (topology_union_axiom X Tx HTx FamU HFamU).
We will prove closed_in X Tx (⋃ Fam).
Apply (closed_inI X Tx (⋃ Fam) HTx HUnionSubX) 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 HUopen.
rewrite the current goal using (setminus_setminus_eq X (⋃ Fam) HUnionSubX) (from left to right).
Use reflexivity.
∎