Let X and Tx be given.
Assume Hmet: metrizable X Tx.
We will prove perfectly_normal_space X Tx.
Apply Hmet to the current goal.
Let d be given.
Assume Hdpack: metric_on X d ∧ metric_topology X d = Tx.
We prove the intermediate claim Hd: metric_on X d.
An exact proof term for the current goal is (andEL (metric_on X d) (metric_topology X d = Tx) Hdpack).
We prove the intermediate claim HTxeq: metric_topology X d = Tx.
An exact proof term for the current goal is (andER (metric_on X d) (metric_topology X d = Tx) Hdpack).
We will prove normal_space X Tx ∧ (∀A : set, closed_in X Tx A → Gdelta_in X Tx A).
Apply andI to the current goal.
rewrite the current goal using HTxeq (from right to left).
An exact proof term for the current goal is (metrizable_spaces_normal X d Hd).
Let A be given.
Assume HAcl: closed_in X Tx A.
We will prove Gdelta_in X Tx A.
We prove the intermediate claim HAclMT: closed_in X (metric_topology X d) A.
rewrite the current goal using HTxeq (from left to right).
An exact proof term for the current goal is HAcl.
We prove the intermediate claim HGdMT: Gdelta_in X (metric_topology X d) A.
An exact proof term for the current goal is (metric_closed_is_Gdelta X d A Hd HAclMT).
rewrite the current goal using HTxeq (from right to left).
An exact proof term for the current goal is HGdMT.
∎