Let X, Tx and U be given.
Assume Hpara: paracompact_space X Tx.
Assume HH: Hausdorff_space X Tx.
Assume Hcover: open_cover X Tx U.
We will prove ∃V : set, open_cover X Tx V ∧ locally_finite_family X Tx V ∧ refine_of V U ∧ ∀v : set, v ∈ V → ∃u : set, u ∈ U ∧ closure_of X Tx v ⊆ u.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (∀U0 : set, open_cover X Tx U0 → ∃V0 : set, open_cover X Tx V0 ∧ locally_finite_family X Tx V0 ∧ refine_of V0 U0) Hpara).
We prove the intermediate claim Hreg: regular_space X Tx.
An exact proof term for the current goal is (paracompact_Hausdorff_regular X Tx Hpara HH).
We prove the intermediate claim HUTx: ∀u : set, u ∈ U → u ∈ Tx.
An exact proof term for the current goal is (andEL (∀u0 : set, u0 ∈ U → u0 ∈ Tx) (covers X U) Hcover).
We prove the intermediate claim HUcov: covers X U.
An exact proof term for the current goal is (andER (∀u0 : set, u0 ∈ U → u0 ∈ Tx) (covers X U) Hcover).
Set pickU to be the term λx : set ⇒ Eps_i (λu : set ⇒ u ∈ U ∧ x ∈ u).
We prove the intermediate claim HpickU: ∀x : set, x ∈ X → pickU x ∈ U ∧ x ∈ pickU x.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim Hex: ∃u : set, u ∈ U ∧ x ∈ u.
An exact proof term for the current goal is (HUcov x HxX).
Apply Hex to the current goal.
Let u be given.
Assume Hu: u ∈ U ∧ x ∈ u.
An exact proof term for the current goal is (Eps_i_ax (λu0 : set ⇒ u0 ∈ U ∧ x ∈ u0) u Hu).
We prove the intermediate claim HpickUTx: ∀x : set, x ∈ X → pickU x ∈ Tx.
Let x be given.
Assume HxX: x ∈ X.
An exact proof term for the current goal is (HUTx (pickU x) (andEL (pickU x ∈ U) (x ∈ pickU x) (HpickU x HxX))).
Set pickV to be the term λx : set ⇒ Eps_i (λV : set ⇒ V ∈ Tx ∧ x ∈ V ∧ closure_of X Tx V ⊆ pickU x).
We prove the intermediate claim HpickV: ∀x : set, x ∈ X → pickV x ∈ Tx ∧ x ∈ pickV x ∧ closure_of X Tx (pickV x) ⊆ pickU x.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim Hux: pickU x ∈ U ∧ x ∈ pickU x.
An exact proof term for the current goal is (HpickU x HxX).
We prove the intermediate claim HuxTx: pickU x ∈ Tx.
An exact proof term for the current goal is (HpickUTx x HxX).
We prove the intermediate claim Hxux: x ∈ pickU x.
An exact proof term for the current goal is (andER (pickU x ∈ U) (x ∈ pickU x) Hux).
We prove the intermediate claim HexV: ∃V : set, V ∈ Tx ∧ x ∈ V ∧ closure_of X Tx V ⊆ pickU x.
An exact proof term for the current goal is (regular_space_shrink_neighborhood X Tx x (pickU x) Hreg HxX HuxTx Hxux).
Apply HexV to the current goal.
Let V be given.
Assume HV: V ∈ Tx ∧ x ∈ V ∧ closure_of X Tx V ⊆ pickU x.
An exact proof term for the current goal is (Eps_i_ax (λV0 : set ⇒ V0 ∈ Tx ∧ x ∈ V0 ∧ closure_of X Tx V0 ⊆ pickU x) V HV).
Set W to be the term Repl X (λx : set ⇒ pickV x).
We prove the intermediate claim HcoverW: open_cover X Tx W.
We will prove (∀w : set, w ∈ W → w ∈ Tx) ∧ covers X W.
Apply andI to the current goal.
Let w be given.
Assume Hw: w ∈ W.
We prove the intermediate claim Hex: ∃x : set, x ∈ X ∧ w = pickV x.
An exact proof term for the current goal is (ReplE X (λx0 : set ⇒ pickV x0) w Hw).
Apply Hex to the current goal.
Let x be given.
Assume Hx: x ∈ X ∧ w = pickV x.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (andEL (x ∈ X) (w = pickV x) Hx).
We prove the intermediate claim Heq: w = pickV x.
An exact proof term for the current goal is (andER (x ∈ X) (w = pickV x) Hx).
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim Hpv: pickV x ∈ Tx ∧ x ∈ pickV x ∧ closure_of X Tx (pickV x) ⊆ pickU x.
An exact proof term for the current goal is (HpickV x HxX).
We prove the intermediate claim Hpvpair: pickV x ∈ Tx ∧ x ∈ pickV x.
An exact proof term for the current goal is (andEL (pickV x ∈ Tx ∧ x ∈ pickV x) (closure_of X Tx (pickV x) ⊆ pickU x) Hpv).
An exact proof term for the current goal is (andEL (pickV x ∈ Tx) (x ∈ pickV x) Hpvpair).
Let x be given.
Assume HxX: x ∈ X.
We use (pickV x) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (ReplI X (λx0 : set ⇒ pickV x0) x HxX).
We prove the intermediate claim Hpv: pickV x ∈ Tx ∧ x ∈ pickV x ∧ closure_of X Tx (pickV x) ⊆ pickU x.
An exact proof term for the current goal is (HpickV x HxX).
We prove the intermediate claim Hpvpair: pickV x ∈ Tx ∧ x ∈ pickV x.
An exact proof term for the current goal is (andEL (pickV x ∈ Tx ∧ x ∈ pickV x) (closure_of X Tx (pickV x) ⊆ pickU x) Hpv).
An exact proof term for the current goal is (andER (pickV x ∈ Tx) (x ∈ pickV x) Hpvpair).
We prove the intermediate claim HparaFor: ∀U0 : set, open_cover X Tx U0 → ∃V0 : set, open_cover X Tx V0 ∧ locally_finite_family X Tx V0 ∧ refine_of V0 U0.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀U0 : set, open_cover X Tx U0 → ∃V0 : set, open_cover X Tx V0 ∧ locally_finite_family X Tx V0 ∧ refine_of V0 U0) Hpara).
We prove the intermediate claim HexV: ∃V0 : set, open_cover X Tx V0 ∧ locally_finite_family X Tx V0 ∧ refine_of V0 W.
An exact proof term for the current goal is (HparaFor W HcoverW).
Apply HexV to the current goal.
Let V be given.
Assume HV: open_cover X Tx V ∧ locally_finite_family X Tx V ∧ refine_of V W.
We use V to witness the existential quantifier.
We prove the intermediate claim HVpair: open_cover X Tx V ∧ locally_finite_family X Tx V.
An exact proof term for the current goal is (andEL (open_cover X Tx V ∧ locally_finite_family X Tx V) (refine_of V W) HV).
We prove the intermediate claim HVrefW: refine_of V W.
An exact proof term for the current goal is (andER (open_cover X Tx V ∧ locally_finite_family X Tx V) (refine_of V W) HV).
We prove the intermediate claim HVcover: open_cover X Tx V.
An exact proof term for the current goal is (andEL (open_cover X Tx V) (locally_finite_family X Tx V) HVpair).
We prove the intermediate claim HVlf: locally_finite_family X Tx V.
An exact proof term for the current goal is (andER (open_cover X Tx V) (locally_finite_family X Tx V) HVpair).
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 HVTx: ∀v : set, v ∈ V → v ∈ Tx.
An exact proof term for the current goal is (andEL (∀v0 : set, v0 ∈ V → v0 ∈ Tx) (covers X V) HVcover).
We prove the intermediate claim Hcldom: ∀v : set, v ∈ V → ∃u : set, u ∈ U ∧ closure_of X Tx v ⊆ u.
Let v be given.
Assume HvV: v ∈ V.
We prove the intermediate claim Hexw: ∃w : set, w ∈ W ∧ v ⊆ w.
An exact proof term for the current goal is (HVrefW v HvV).
Apply Hexw to the current goal.
Let w be given.
Assume Hw: w ∈ W ∧ v ⊆ w.
We prove the intermediate claim HwW: w ∈ W.
An exact proof term for the current goal is (andEL (w ∈ W) (v ⊆ w) Hw).
We prove the intermediate claim Hvsubw: v ⊆ w.
An exact proof term for the current goal is (andER (w ∈ W) (v ⊆ w) Hw).
We prove the intermediate claim Hexx: ∃x : set, x ∈ X ∧ w = pickV x.
An exact proof term for the current goal is (ReplE X (λx0 : set ⇒ pickV x0) w HwW).
Apply Hexx to the current goal.
Let x be given.
Assume Hx: x ∈ X ∧ w = pickV x.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (andEL (x ∈ X) (w = pickV x) Hx).
We prove the intermediate claim Heqw: w = pickV x.
An exact proof term for the current goal is (andER (x ∈ X) (w = pickV x) Hx).
Set u to be the term pickU x.
We use u to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (u ∈ U) (x ∈ u) (HpickU x HxX)).
We will prove closure_of X Tx v ⊆ u.
We prove the intermediate claim HwTx: w ∈ Tx.
rewrite the current goal using Heqw (from left to right).
We prove the intermediate claim Hpv: pickV x ∈ Tx ∧ x ∈ pickV x ∧ closure_of X Tx (pickV x) ⊆ pickU x.
An exact proof term for the current goal is (HpickV x HxX).
We prove the intermediate claim Hpvpair: pickV x ∈ Tx ∧ x ∈ pickV x.
An exact proof term for the current goal is (andEL (pickV x ∈ Tx ∧ x ∈ pickV x) (closure_of X Tx (pickV x) ⊆ pickU x) Hpv).
An exact proof term for the current goal is (andEL (pickV x ∈ Tx) (x ∈ pickV x) Hpvpair).
We prove the intermediate claim HwPow: w ∈ 𝒫 X.
An exact proof term for the current goal is (HTsub w HwTx).
We prove the intermediate claim HwsubX: w ⊆ X.
An exact proof term for the current goal is (PowerE X w HwPow).
We prove the intermediate claim Hclvclw: closure_of X Tx v ⊆ closure_of X Tx w.
An exact proof term for the current goal is (closure_monotone X Tx v w HTx Hvsubw HwsubX).
We prove the intermediate claim Hclwsub: closure_of X Tx w ⊆ u.
rewrite the current goal using Heqw (from left to right).
We prove the intermediate claim Hpv: pickV x ∈ Tx ∧ x ∈ pickV x ∧ closure_of X Tx (pickV x) ⊆ pickU x.
An exact proof term for the current goal is (HpickV x HxX).
An exact proof term for the current goal is (andER (pickV x ∈ Tx ∧ x ∈ pickV x) (closure_of X Tx (pickV x) ⊆ pickU x) Hpv).
An exact proof term for the current goal is (Subq_tra (closure_of X Tx v) (closure_of X Tx w) u Hclvclw Hclwsub).
Apply and4I to the current goal.
An exact proof term for the current goal is HVcover.
An exact proof term for the current goal is HVlf.
Let v be given.
Assume HvV: v ∈ V.
We will prove ∃u : set, u ∈ U ∧ v ⊆ u.
We prove the intermediate claim Hexu: ∃u : set, u ∈ U ∧ closure_of X Tx v ⊆ u.
An exact proof term for the current goal is (Hcldom v HvV).
Apply Hexu to the current goal.
Let u be given.
Assume Hu: u ∈ U ∧ closure_of X Tx v ⊆ u.
We use u to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (u ∈ U) (closure_of X Tx v ⊆ u) Hu).
We prove the intermediate claim HvTx: v ∈ Tx.
An exact proof term for the current goal is (HVTx v HvV).
We prove the intermediate claim HvPow: v ∈ 𝒫 X.
An exact proof term for the current goal is (HTsub v HvTx).
We prove the intermediate claim HvsubX: v ⊆ X.
An exact proof term for the current goal is (PowerE X v HvPow).
We prove the intermediate claim Hvsubcl: v ⊆ closure_of X Tx v.
An exact proof term for the current goal is (subset_of_closure X Tx v HTx HvsubX).
An exact proof term for the current goal is (Subq_tra v (closure_of X Tx v) u Hvsubcl (andER (u ∈ U) (closure_of X Tx v ⊆ u) Hu)).
An exact proof term for the current goal is Hcldom.
∎