Let X, Tx and U be given.
Assume Hpara: paracompact_space X Tx.
Assume HH: Hausdorff_space X Tx.
Assume HU: open_cover X Tx U.
We prove the intermediate claim HexV: ∃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.
An exact proof term for the current goal is (shrinking_lemma_41_6 X Tx U Hpara HH HU).
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 U ∧ ∀v : set, v ∈ V → ∃u : set, u ∈ U ∧ closure_of X Tx v ⊆ u.
We prove the intermediate claim HV1: (open_cover X Tx V ∧ locally_finite_family X Tx V) ∧ refine_of V U.
An exact proof term for the current goal is (andEL ((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) HV).
We prove the intermediate claim HVcovlf: 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 U) HV1).
We prove the intermediate claim HVcov: 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) HVcovlf).
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) HVcovlf).
We prove the intermediate claim HVref: refine_of V U.
An exact proof term for the current goal is (andER (open_cover X Tx V ∧ locally_finite_family X Tx V) (refine_of V U) HV1).
We prove the intermediate claim HVcl: ∀v : set, v ∈ V → ∃u : set, u ∈ U ∧ closure_of X Tx v ⊆ u.
An exact proof term for the current goal is (andER ((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) HV).
We prove the intermediate claim HexW: ∃W : set, open_cover X Tx W ∧ locally_finite_family X Tx W ∧ refine_of W V ∧ ∀w : set, w ∈ W → ∃v : set, v ∈ V ∧ closure_of X Tx w ⊆ v.
An exact proof term for the current goal is (shrinking_lemma_41_6 X Tx V Hpara HH HVcov).
Apply HexW to the current goal.
Let W be given.
Assume HW: open_cover X Tx W ∧ locally_finite_family X Tx W ∧ refine_of W V ∧ ∀w : set, w ∈ W → ∃v : set, v ∈ V ∧ closure_of X Tx w ⊆ v.
We prove the intermediate claim HW1: (open_cover X Tx W ∧ locally_finite_family X Tx W) ∧ refine_of W V.
An exact proof term for the current goal is (andEL ((open_cover X Tx W ∧ locally_finite_family X Tx W) ∧ refine_of W V) (∀w : set, w ∈ W → ∃v : set, v ∈ V ∧ closure_of X Tx w ⊆ v) HW).
We prove the intermediate claim HWcovlf: open_cover X Tx W ∧ locally_finite_family X Tx W.
An exact proof term for the current goal is (andEL (open_cover X Tx W ∧ locally_finite_family X Tx W) (refine_of W V) HW1).
We prove the intermediate claim HWcov: open_cover X Tx W.
An exact proof term for the current goal is (andEL (open_cover X Tx W) (locally_finite_family X Tx W) HWcovlf).
We prove the intermediate claim HWlf: locally_finite_family X Tx W.
An exact proof term for the current goal is (andER (open_cover X Tx W) (locally_finite_family X Tx W) HWcovlf).
We prove the intermediate claim HWref: refine_of W V.
An exact proof term for the current goal is (andER (open_cover X Tx W ∧ locally_finite_family X Tx W) (refine_of W V) HW1).
We prove the intermediate claim HWcl: ∀w : set, w ∈ W → ∃v : set, v ∈ V ∧ closure_of X Tx w ⊆ v.
An exact proof term for the current goal is (andER ((open_cover X Tx W ∧ locally_finite_family X Tx W) ∧ refine_of W V) (∀w : set, w ∈ W → ∃v : set, v ∈ V ∧ closure_of X Tx w ⊆ v) HW).
We use V to witness the existential quantifier.
We use W to witness the existential quantifier.
Apply andI to the current goal.
We will prove 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) ∧ open_cover X Tx W ∧ locally_finite_family X Tx W ∧ refine_of W V.
Apply and7I to the current goal.
An exact proof term for the current goal is HVcov.
An exact proof term for the current goal is HVlf.
An exact proof term for the current goal is HVref.
An exact proof term for the current goal is HVcl.
An exact proof term for the current goal is HWcov.
An exact proof term for the current goal is HWlf.
An exact proof term for the current goal is HWref.
An exact proof term for the current goal is HWcl.
∎