Let X and Tx be given.
Assume Hreg: regular_space X Tx.
We will prove (Michael_cond41_3_1 X Tx → Michael_cond41_3_2 X Tx) ∧ (Michael_cond41_3_2 X Tx → Michael_cond41_3_3 X Tx) ∧ (Michael_cond41_3_3 X Tx → Michael_cond41_3_4 X Tx) ∧ (Michael_cond41_3_4 X Tx → Michael_cond41_3_1 X Tx).
Apply and4I to the current goal.
Assume H1: Michael_cond41_3_1 X Tx.
We will prove Michael_cond41_3_2 X Tx.
Let U be given.
Assume HU: open_cover X Tx U.
We will prove ∃V : set, covers X V ∧ locally_finite_family X Tx V ∧ refine_of V U.
We prove the intermediate claim HexV: ∃V : set, open_cover X Tx V ∧ sigma_locally_finite_family X Tx V ∧ refine_of V U.
An exact proof term for the current goal is (H1 U HU).
Apply HexV to the current goal.
Let V be given.
Assume HV: open_cover X Tx V ∧ sigma_locally_finite_family X Tx V ∧ refine_of V U.
We prove the intermediate claim Hcovsigma: open_cover X Tx V ∧ sigma_locally_finite_family X Tx V.
An exact proof term for the current goal is (andEL (open_cover X Tx V ∧ sigma_locally_finite_family X Tx V) (refine_of V U) HV).
We prove the intermediate claim Hcov: open_cover X Tx V.
An exact proof term for the current goal is (andEL (open_cover X Tx V) (sigma_locally_finite_family X Tx V) Hcovsigma).
We prove the intermediate claim Hsigma: sigma_locally_finite_family X Tx V.
An exact proof term for the current goal is (andER (open_cover X Tx V) (sigma_locally_finite_family X Tx V) Hcovsigma).
We prove the intermediate claim Href: refine_of V U.
An exact proof term for the current goal is (andER (open_cover X Tx V ∧ sigma_locally_finite_family X Tx V) (refine_of V U) HV).
We prove the intermediate claim HexC: ∃C : set, covers X C ∧ locally_finite_family X Tx C ∧ refine_of C V.
An exact proof term for the current goal is (sigma_locally_finite_open_cover_imp_locally_finite_refinement X Tx V Hreg Hcov Hsigma).
Apply HexC to the current goal.
Let C be given.
Assume HC: covers X C ∧ locally_finite_family X Tx C ∧ refine_of C V.
We prove the intermediate claim HCcovlf: covers X C ∧ locally_finite_family X Tx C.
An exact proof term for the current goal is (andEL (covers X C ∧ locally_finite_family X Tx C) (refine_of C V) HC).
We prove the intermediate claim HcovC: covers X C.
An exact proof term for the current goal is (andEL (covers X C) (locally_finite_family X Tx C) HCcovlf).
We prove the intermediate claim HlfC: locally_finite_family X Tx C.
An exact proof term for the current goal is (andER (covers X C) (locally_finite_family X Tx C) HCcovlf).
We prove the intermediate claim HrefCV: refine_of C V.
An exact proof term for the current goal is (andER (covers X C ∧ locally_finite_family X Tx C) (refine_of C V) HC).
We prove the intermediate claim HrefCU: refine_of C U.
An exact proof term for the current goal is (refine_trans U V C HrefCV Href).
We use C 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 HcovC.
An exact proof term for the current goal is HlfC.
An exact proof term for the current goal is HrefCU.
Assume H2: Michael_cond41_3_2 X Tx.
We will prove Michael_cond41_3_3 X Tx.
Let U be given.
Assume HU: open_cover X Tx U.
An exact proof term for the current goal is (Michael_lemma_41_3_closed_cover_from_locally_finite_refinement X Tx U Hreg HU H2).
Assume H3: Michael_cond41_3_3 X Tx.
We will prove Michael_cond41_3_4 X Tx.
Let U be given.
Assume HU: open_cover X Tx U.
An exact proof term for the current goal is (Michael_lemma_41_3_closed_refinement_to_open_refinement X Tx U Hreg HU H3).
Assume H4: Michael_cond41_3_4 X Tx.
We will prove Michael_cond41_3_1 X Tx.
Let U be given.
Assume HU: open_cover X Tx U.
We will prove ∃V : set, open_cover X Tx V ∧ sigma_locally_finite_family X Tx V ∧ refine_of V U.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (regular_space_topology_on X Tx Hreg).
We prove the intermediate claim HexV: ∃V : set, open_cover X Tx V ∧ locally_finite_family X Tx V ∧ refine_of V U.
An exact proof term for the current goal is (H4 U 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.
We prove the intermediate claim Hcovlf: 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) HV).
We prove the intermediate claim Hcov: 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) Hcovlf).
We prove the intermediate claim Hlf: 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) Hcovlf).
We prove the intermediate claim Href: 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) HV).
We prove the intermediate claim HVsubPow: V ⊆ 𝒫 X.
An exact proof term for the current goal is (open_cover_family_sub X Tx V HTx Hcov).
We prove the intermediate claim Hsigma: sigma_locally_finite_family X Tx V.
An exact proof term for the current goal is (locally_finite_family_imp_sigma_locally_finite_family X Tx V HTx HVsubPow Hlf).
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 Hcov.
An exact proof term for the current goal is Hsigma.
An exact proof term for the current goal is Href.
∎