Let X, Tx and m be given.
Assume Hloc: locally_m_euclidean X Tx m.
Assume Hman: m_manifold X Tx m.
We will prove metrizable X Tx.
We prove the intermediate claim H12m: ((Hausdorff_space X Tx ∧ second_countable_space X Tx) ∧ m ∈ ω) ∧ ∀x : set, x ∈ X → ∃U : set, U ∈ Tx ∧ x ∈ U ∧ ∃V : set, V ∈ (euclidean_topology m) ∧ ∃f : set, homeomorphism U (subspace_topology X Tx U) V (subspace_topology (euclidean_space m) (euclidean_topology m) V) f.
An exact proof term for the current goal is Hman.
We prove the intermediate claim H12: (Hausdorff_space X Tx ∧ second_countable_space X Tx) ∧ m ∈ ω.
An exact proof term for the current goal is (andEL ((Hausdorff_space X Tx ∧ second_countable_space X Tx) ∧ m ∈ ω) (∀x : set, x ∈ X → ∃U : set, U ∈ Tx ∧ x ∈ U ∧ ∃V : set, V ∈ (euclidean_topology m) ∧ ∃f : set, homeomorphism U (subspace_topology X Tx U) V (subspace_topology (euclidean_space m) (euclidean_topology m) V) f) H12m).
We prove the intermediate claim Hpair: Hausdorff_space X Tx ∧ second_countable_space X Tx.
An exact proof term for the current goal is (andEL (Hausdorff_space X Tx ∧ second_countable_space X Tx) (m ∈ ω) H12).
We prove the intermediate claim HH: Hausdorff_space X Tx.
An exact proof term for the current goal is (andEL (Hausdorff_space X Tx) (second_countable_space X Tx) Hpair).
We prove the intermediate claim Hscc: second_countable_space X Tx.
An exact proof term for the current goal is (andER (Hausdorff_space X Tx) (second_countable_space X Tx) Hpair).
We prove the intermediate claim Hlc_pair: locally_compact X Tx ∧ locally_metrizable_space X Tx.
An exact proof term for the current goal is (supp_ex_locally_euclidean_1 X Tx m Hloc).
We prove the intermediate claim Hlc: locally_compact X Tx.
An exact proof term for the current goal is (andEL (locally_compact X Tx) (locally_metrizable_space X Tx) Hlc_pair).
We prove the intermediate claim Hreg: regular_space X Tx.
An exact proof term for the current goal is (locally_compact_Hausdorff_regular_early X Tx Hlc HH).
An exact proof term for the current goal is (Urysohn_metrization_theorem X Tx Hreg Hscc).
∎