Let X and Tx be given.
Assume Hnorm: normal_space X Tx.
Let F be given.
Assume HFfin: finite F.
Assume HFsubR: F ⊆ R.
Let Uof be given.
Assume HUof: ∀p : set, p ∈ F → Uof p ∈ Tx.
Assume Hnest: ∀p q : set, p ∈ F → q ∈ F → Rlt p q → closure_of X Tx (Uof p) ⊆ Uof q.
Let r be given.
Assume HrR: r ∈ R.
We will prove ∃Ur : set, Ur ∈ Tx ∧ (∀p : set, p ∈ F → Rlt p r → closure_of X Tx (Uof p) ⊆ Ur) ∧ (∀q : set, q ∈ F → Rlt r q → closure_of X Tx Ur ⊆ Uof q).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (normal_space_topology_on X Tx Hnorm).
We prove the intermediate claim HFltFin: finite {x ∈ F|Rlt x r}.
We prove the intermediate claim HFltSubF: {x ∈ F|Rlt x r} ⊆ F.
Let p be given.
Assume Hp: p ∈ {x ∈ F|Rlt x r}.
An exact proof term for the current goal is (SepE1 F (λp0 : set ⇒ Rlt p0 r) p Hp).
An exact proof term for the current goal is (Subq_finite F HFfin {x ∈ F|Rlt x r} HFltSubF).
Set ClFam to be the term {closure_of X Tx (Uof p)|p ∈ {x ∈ F|Rlt x r}}.
We prove the intermediate claim HClFamFin: finite ClFam.
An exact proof term for the current goal is (Repl_finite (λp : set ⇒ closure_of X Tx (Uof p)) {x ∈ F|Rlt x r} HFltFin).
We prove the intermediate claim HClFamClosed: ∀C : set, C ∈ ClFam → closed_in X Tx C.
Let C be given.
Assume HC: C ∈ ClFam.
Apply (ReplE_impred {x ∈ F|Rlt x r} (λp : set ⇒ closure_of X Tx (Uof p)) C HC (closed_in X Tx C)) to the current goal.
Let p be given.
Assume HpFlt: p ∈ {x ∈ F|Rlt x r}.
Assume HCeq: C = closure_of X Tx (Uof p).
rewrite the current goal using HCeq (from left to right).
We prove the intermediate claim HpF: p ∈ F.
An exact proof term for the current goal is (SepE1 F (λp0 : set ⇒ Rlt p0 r) p HpFlt).
We prove the intermediate claim HUpTx: Uof p ∈ Tx.
An exact proof term for the current goal is (HUof p HpF).
We prove the intermediate claim HUpSubX: Uof p ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx (Uof p) HTx HUpTx).
An exact proof term for the current goal is (closure_is_closed X Tx (Uof p) HTx HUpSubX).
Set Lower to be the term ⋃ ClFam.
We prove the intermediate claim HLowerClosed: closed_in X Tx Lower.
An exact proof term for the current goal is (finite_union_closed_in X Tx ClFam HTx HClFamFin HClFamClosed).
We prove the intermediate claim HFgtFin: finite {x ∈ F|Rlt r x}.
We prove the intermediate claim HFgtSubF: {x ∈ F|Rlt r x} ⊆ F.
Let q be given.
Assume Hq: q ∈ {x ∈ F|Rlt r x}.
An exact proof term for the current goal is (SepE1 F (λq0 : set ⇒ Rlt r q0) q Hq).
An exact proof term for the current goal is (Subq_finite F HFfin {x ∈ F|Rlt r x} HFgtSubF).
Set UpFam to be the term {Uof q|q ∈ {x ∈ F|Rlt r x}}.
We prove the intermediate claim HUpFamFin: finite UpFam.
An exact proof term for the current goal is (Repl_finite (λq : set ⇒ Uof q) {x ∈ F|Rlt r x} HFgtFin).
We prove the intermediate claim HUpFamSubTx: UpFam ⊆ Tx.
Let U be given.
Assume HU: U ∈ UpFam.
Apply (ReplE_impred {x ∈ F|Rlt r x} (λq : set ⇒ Uof q) U HU (U ∈ Tx)) to the current goal.
Let q be given.
Assume HqFgt: q ∈ {x ∈ F|Rlt r x}.
Assume HUeq: U = Uof q.
rewrite the current goal using HUeq (from left to right).
We prove the intermediate claim HqF: q ∈ F.
An exact proof term for the current goal is (SepE1 F (λq0 : set ⇒ Rlt r q0) q HqFgt).
An exact proof term for the current goal is (HUof q HqF).
We prove the intermediate claim HUpFamPow: UpFam ∈ 𝒫 Tx.
An exact proof term for the current goal is (PowerI Tx UpFam HUpFamSubTx).
Set Upper to be the term intersection_of_family X UpFam.
We prove the intermediate claim HUpperTx: Upper ∈ Tx.
An exact proof term for the current goal is (finite_intersection_in_topology X Tx UpFam HTx HUpFamPow HUpFamFin).
We prove the intermediate claim HLowerSubUpper: Lower ⊆ Upper.
Let x be given.
Assume Hx: x ∈ Lower.
We will prove x ∈ Upper.
Apply (UnionE ClFam x Hx) to the current goal.
Let C be given.
Assume HCpair: x ∈ C ∧ C ∈ ClFam.
Apply HCpair to the current goal.
Assume HxC: x ∈ C.
Assume HCin: C ∈ ClFam.
Apply (ReplE_impred {x ∈ F|Rlt x r} (λp0 : set ⇒ closure_of X Tx (Uof p0)) C HCin (x ∈ Upper)) to the current goal.
Let p be given.
Assume HpFlt: p ∈ {x ∈ F|Rlt x r}.
Assume HCeq: C = closure_of X Tx (Uof p).
We prove the intermediate claim HxCl: x ∈ closure_of X Tx (Uof p).
rewrite the current goal using HCeq (from right to left).
An exact proof term for the current goal is HxC.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (closed_in_subset X Tx Lower HLowerClosed x Hx).
We prove the intermediate claim HallU: ∀U : set, U ∈ UpFam → x ∈ U.
Let U be given.
Assume HU: U ∈ UpFam.
Apply (ReplE_impred {x ∈ F|Rlt r x} (λq0 : set ⇒ Uof q0) U HU (x ∈ U)) to the current goal.
Let q be given.
Assume HqFgt: q ∈ {x ∈ F|Rlt r x}.
Assume HUeq: U = Uof q.
rewrite the current goal using HUeq (from left to right).
We prove the intermediate claim HpF: p ∈ F.
An exact proof term for the current goal is (SepE1 F (λp0 : set ⇒ Rlt p0 r) p HpFlt).
We prove the intermediate claim HqF: q ∈ F.
An exact proof term for the current goal is (SepE1 F (λq0 : set ⇒ Rlt r q0) q HqFgt).
We prove the intermediate claim Hpr: Rlt p r.
An exact proof term for the current goal is (SepE2 F (λp0 : set ⇒ Rlt p0 r) p HpFlt).
We prove the intermediate claim Hrq: Rlt r q.
An exact proof term for the current goal is (SepE2 F (λq0 : set ⇒ Rlt r q0) q HqFgt).
We prove the intermediate claim Hpq: Rlt p q.
An exact proof term for the current goal is (Rlt_tra p r q Hpr Hrq).
We prove the intermediate claim Hsub: closure_of X Tx (Uof p) ⊆ Uof q.
An exact proof term for the current goal is (Hnest p q HpF HqF Hpq).
An exact proof term for the current goal is (Hsub x HxCl).
An exact proof term for the current goal is (intersection_of_familyI X UpFam x HxX HallU).
We prove the intermediate claim HUpperOpen: Upper ∈ Tx.
An exact proof term for the current goal is HUpperTx.
Apply (normal_space_shrink_closed X Tx Lower Upper Hnorm HLowerClosed HUpperOpen HLowerSubUpper) to the current goal.
Let Ur be given.
Assume HUr: Ur ∈ Tx ∧ Lower ⊆ Ur ∧ closure_of X Tx Ur ⊆ Upper.
We use Ur to witness the existential quantifier.
We prove the intermediate claim HUr12: Ur ∈ Tx ∧ Lower ⊆ Ur.
An exact proof term for the current goal is (andEL (Ur ∈ Tx ∧ Lower ⊆ Ur) (closure_of X Tx Ur ⊆ Upper) HUr).
We prove the intermediate claim HUr1: Ur ∈ Tx.
An exact proof term for the current goal is (andEL (Ur ∈ Tx) (Lower ⊆ Ur) HUr12).
We prove the intermediate claim HLowerSubUr: Lower ⊆ Ur.
An exact proof term for the current goal is (andER (Ur ∈ Tx) (Lower ⊆ Ur) HUr12).
We prove the intermediate claim HUr3: closure_of X Tx Ur ⊆ Upper.
An exact proof term for the current goal is (andER (Ur ∈ Tx ∧ Lower ⊆ Ur) (closure_of X Tx Ur ⊆ Upper) HUr).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HUr1.
Let p be given.
Assume HpF: p ∈ F.
Assume Hpr: Rlt p r.
We will prove closure_of X Tx (Uof p) ⊆ Ur.
Let x be given.
Assume Hx: x ∈ closure_of X Tx (Uof p).
We will prove x ∈ Ur.
We prove the intermediate claim HpFlt: p ∈ {x ∈ F|Rlt x r}.
An exact proof term for the current goal is (SepI F (λp0 : set ⇒ Rlt p0 r) p HpF Hpr).
We prove the intermediate claim HCin: closure_of X Tx (Uof p) ∈ ClFam.
An exact proof term for the current goal is (ReplI {x ∈ F|Rlt x r} (λp0 : set ⇒ closure_of X Tx (Uof p0)) p HpFlt).
We prove the intermediate claim HxLower: x ∈ Lower.
An exact proof term for the current goal is (UnionI ClFam x (closure_of X Tx (Uof p)) Hx HCin).
An exact proof term for the current goal is (HLowerSubUr x HxLower).
Let q be given.
Assume HqF: q ∈ F.
Assume Hrq: Rlt r q.
We will prove closure_of X Tx Ur ⊆ Uof q.
We prove the intermediate claim HUin: Uof q ∈ UpFam.
We prove the intermediate claim HqFgt: q ∈ {x ∈ F|Rlt r x}.
An exact proof term for the current goal is (SepI F (λq0 : set ⇒ Rlt r q0) q HqF Hrq).
An exact proof term for the current goal is (ReplI {x ∈ F|Rlt r x} (λq0 : set ⇒ Uof q0) q HqFgt).
Let x be given.
Assume Hx: x ∈ closure_of X Tx Ur.
We prove the intermediate claim HxU: x ∈ Upper.
An exact proof term for the current goal is (HUr3 x Hx).
An exact proof term for the current goal is (intersection_of_familyE2 X UpFam x HxU (Uof q) HUin).
∎