Let X, Tx and Fam be given.
Assume HFsubX: ∀A : set, A ∈ Fam → A ⊆ X.
Assume HLF: locally_finite_family X Tx Fam.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (locally_finite_family_topology X Tx Fam HLF).
Set ClFam to be the term {closure_of X Tx A|A ∈ Fam}.
Let x be given.
Assume Hxcl: x ∈ closure_of X Tx (⋃ Fam).
We will prove x ∈ ⋃ ClFam.
Apply (xm (x ∈ ⋃ ClFam)) to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume Hnot: x ∉ ⋃ ClFam.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ (⋃ Fam) ≠ Empty) x Hxcl).
We prove the intermediate claim HxNbhd: ∀U : set, U ∈ Tx → x ∈ U → U ∩ (⋃ Fam) ≠ Empty.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ (⋃ Fam) ≠ Empty) x Hxcl).
We prove the intermediate claim HexLF: ∃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 (locally_finite_family_property X Tx Fam HLF x HxX).
Apply HexLF to the current goal.
Let N be given.
Assume HN: N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ Fam ∧ ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S.
We prove the intermediate claim HN1: 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) HN).
We prove the intermediate claim HNTx: N ∈ Tx.
An exact proof term for the current goal is (andEL (N ∈ Tx) (x ∈ N) HN1).
We prove the intermediate claim HxN: x ∈ N.
An exact proof term for the current goal is (andER (N ∈ Tx) (x ∈ N) HN1).
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) HN).
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 HS1: 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) HS1).
We prove the intermediate claim HSsubFam: S ⊆ Fam.
An exact proof term for the current goal is (andER (finite S) (S ⊆ Fam) HS1).
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 (λU : set ⇒ U ∈ Tx ∧ x ∈ U ∧ U ∩ A = Empty).
Set UFam to be the term {sep_open A|A ∈ S}.
We prove the intermediate claim HUFamFin: finite UFam.
An exact proof term for the current goal is (Repl_finite (λA : set ⇒ sep_open A) S HSfin).
We prove the intermediate claim HUFamSubTx: UFam ⊆ Tx.
Let U be given.
Assume HU: U ∈ UFam.
Apply (ReplE_impred S (λA : set ⇒ sep_open A) U HU (U ∈ Tx)) to the current goal.
Let A be given.
Assume HA: A ∈ S.
Assume HUeq: U = 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 HxNotClA: x ∉ closure_of X Tx A.
Assume HxClA: x ∈ closure_of X Tx A.
We prove the intermediate claim HclAin: closure_of X Tx A ∈ ClFam.
An exact proof term for the current goal is (ReplI Fam (λA0 : set ⇒ closure_of X Tx A0) A HAFam).
We prove the intermediate claim HxInUnion: x ∈ ⋃ ClFam.
An exact proof term for the current goal is (UnionI ClFam x (closure_of X Tx A) HxClA HclAin).
An exact proof term for the current goal is (Hnot HxInUnion).
We prove the intermediate claim HAX: A ⊆ X.
An exact proof term for the current goal is (HFsubX A HAFam).
We prove the intermediate claim HexU: ∃U0 : set, U0 ∈ Tx ∧ x ∈ U0 ∧ U0 ∩ A = Empty.
An exact proof term for the current goal is (not_in_closure_has_disjoint_open X Tx A x HTx HAX HxX HxNotClA).
We prove the intermediate claim Hsep: (sep_open A) ∈ Tx ∧ x ∈ (sep_open A) ∧ (sep_open A) ∩ A = Empty.
An exact proof term for the current goal is (Eps_i_ex (λU0 : set ⇒ U0 ∈ Tx ∧ x ∈ U0 ∧ U0 ∩ A = Empty) HexU).
rewrite the current goal using HUeq (from left to right).
We prove the intermediate claim HsepAB: (sep_open A) ∈ Tx ∧ x ∈ (sep_open A).
An exact proof term for the current goal is (andEL ((sep_open A) ∈ Tx ∧ x ∈ (sep_open A)) ((sep_open A) ∩ A = Empty) Hsep).
An exact proof term for the current goal is (andEL ((sep_open A) ∈ Tx) (x ∈ (sep_open A)) HsepAB).
We prove the intermediate claim HUFamPow: UFam ∈ 𝒫 Tx.
Apply PowerI to the current goal.
An exact proof term for the current goal is HUFamSubTx.
Set Uinter to be the term intersection_of_family X UFam.
We prove the intermediate claim HUinterTx: Uinter ∈ Tx.
An exact proof term for the current goal is (finite_intersection_in_topology X Tx UFam HTx HUFamPow HUFamFin).
Set M to be the term N ∩ Uinter.
We prove the intermediate claim HMTx: M ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_closed X Tx N Uinter HTx HNTx HUinterTx).
We prove the intermediate claim HxUinter: x ∈ Uinter.
We prove the intermediate claim HallUFam: ∀U : set, U ∈ UFam → x ∈ U.
Let U be given.
Assume HU: U ∈ UFam.
We will prove x ∈ U.
Apply (ReplE_impred S (λA : set ⇒ sep_open A) U HU (x ∈ U)) to the current goal.
Let A be given.
Assume HA: A ∈ S.
Assume HUeq: U = 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 HxNotClA: x ∉ closure_of X Tx A.
Assume HxClA: x ∈ closure_of X Tx A.
We prove the intermediate claim HclAin: closure_of X Tx A ∈ ClFam.
An exact proof term for the current goal is (ReplI Fam (λA0 : set ⇒ closure_of X Tx A0) A HAFam).
We prove the intermediate claim HxInUnion: x ∈ ⋃ ClFam.
An exact proof term for the current goal is (UnionI ClFam x (closure_of X Tx A) HxClA HclAin).
An exact proof term for the current goal is (Hnot HxInUnion).
We prove the intermediate claim HAX: A ⊆ X.
An exact proof term for the current goal is (HFsubX A HAFam).
We prove the intermediate claim HexU: ∃U0 : set, U0 ∈ Tx ∧ x ∈ U0 ∧ U0 ∩ A = Empty.
An exact proof term for the current goal is (not_in_closure_has_disjoint_open X Tx A x HTx HAX HxX HxNotClA).
We prove the intermediate claim Hsep: (sep_open A) ∈ Tx ∧ x ∈ (sep_open A) ∧ (sep_open A) ∩ A = Empty.
An exact proof term for the current goal is (Eps_i_ex (λU0 : set ⇒ U0 ∈ Tx ∧ x ∈ U0 ∧ U0 ∩ A = Empty) HexU).
rewrite the current goal using HUeq (from left to right).
We prove the intermediate claim HsepAB: (sep_open A) ∈ Tx ∧ x ∈ (sep_open A).
An exact proof term for the current goal is (andEL ((sep_open A) ∈ Tx ∧ x ∈ (sep_open A)) ((sep_open A) ∩ A = Empty) Hsep).
An exact proof term for the current goal is (andER ((sep_open A) ∈ Tx) (x ∈ (sep_open A)) HsepAB).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ ∀U : set, U ∈ UFam → x0 ∈ U) x HxX HallUFam).
We prove the intermediate claim HxM: x ∈ M.
An exact proof term for the current goal is (binintersectI N Uinter x HxN HxUinter).
We prove the intermediate claim HMEmpty: M ∩ (⋃ Fam) = Empty.
Apply Empty_Subq_eq to the current goal.
Let z be given.
Assume Hz: z ∈ M ∩ (⋃ Fam).
We will prove z ∈ Empty.
We prove the intermediate claim HzM: z ∈ M.
An exact proof term for the current goal is (binintersectE1 M (⋃ Fam) z Hz).
We prove the intermediate claim HzUF: z ∈ ⋃ Fam.
An exact proof term for the current goal is (binintersectE2 M (⋃ Fam) z Hz).
We prove the intermediate claim HzN: z ∈ N.
An exact proof term for the current goal is (binintersectE1 N Uinter z HzM).
We prove the intermediate claim HzUinter: z ∈ Uinter.
An exact proof term for the current goal is (binintersectE2 N Uinter z HzM).
Apply (UnionE_impred Fam z HzUF) to the current goal.
Let A0 be given.
Assume HzA0: z ∈ A0.
Assume HA0Fam: A0 ∈ Fam.
We prove the intermediate claim HA0Nnon: A0 ∩ N ≠ Empty.
An exact proof term for the current goal is (elem_implies_nonempty (A0 ∩ N) z (binintersectI A0 N z HzA0 HzN)).
We prove the intermediate claim HA0S: A0 ∈ S.
An exact proof term for the current goal is (HSprop A0 HA0Fam HA0Nnon).
We prove the intermediate claim HUA0: (sep_open A0) ∈ UFam.
An exact proof term for the current goal is (ReplI S (λA : set ⇒ sep_open A) A0 HA0S).
We prove the intermediate claim HzInSep: z ∈ sep_open A0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∀U : set, U ∈ UFam → x0 ∈ U) z HzUinter (sep_open A0) HUA0).
We prove the intermediate claim HxNotClA0: x ∉ closure_of X Tx A0.
Assume HxClA0: x ∈ closure_of X Tx A0.
We prove the intermediate claim HclAin: closure_of X Tx A0 ∈ ClFam.
An exact proof term for the current goal is (ReplI Fam (λA1 : set ⇒ closure_of X Tx A1) A0 HA0Fam).
We prove the intermediate claim HxInUnion: x ∈ ⋃ ClFam.
An exact proof term for the current goal is (UnionI ClFam x (closure_of X Tx A0) HxClA0 HclAin).
An exact proof term for the current goal is (Hnot HxInUnion).
We prove the intermediate claim HA0X: A0 ⊆ X.
An exact proof term for the current goal is (HFsubX A0 HA0Fam).
We prove the intermediate claim HexU: ∃U0 : set, U0 ∈ Tx ∧ x ∈ U0 ∧ U0 ∩ A0 = Empty.
An exact proof term for the current goal is (not_in_closure_has_disjoint_open X Tx A0 x HTx HA0X HxX HxNotClA0).
We prove the intermediate claim Hsep: (sep_open A0) ∈ Tx ∧ x ∈ (sep_open A0) ∧ (sep_open A0) ∩ A0 = Empty.
An exact proof term for the current goal is (Eps_i_ex (λU0 : set ⇒ U0 ∈ Tx ∧ x ∈ U0 ∧ U0 ∩ A0 = Empty) HexU).
We prove the intermediate claim HsepEq: (sep_open A0) ∩ A0 = Empty.
An exact proof term for the current goal is (andER ((sep_open A0) ∈ Tx ∧ x ∈ (sep_open A0)) ((sep_open A0) ∩ A0 = Empty) Hsep).
We prove the intermediate claim HzInInt: z ∈ (sep_open A0) ∩ A0.
An exact proof term for the current goal is (binintersectI (sep_open A0) A0 z HzInSep HzA0).
rewrite the current goal using HsepEq (from right to left).
An exact proof term for the current goal is HzInInt.
We prove the intermediate claim Hcontra: M ∩ (⋃ Fam) ≠ Empty.
An exact proof term for the current goal is (HxNbhd M HMTx HxM).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hcontra HMEmpty).
∎