Let X and d be given.
Assume Hc: complete_metric_space X d.
We will prove Baire_space_closed X (metric_topology X d).
We will prove topology_on X (metric_topology X d) ∧ ∀Fam : set, countable_set Fam → (∀A : set, A ∈ Fam → closed_in X (metric_topology X d) A ∧ interior_of X (metric_topology X d) A = Empty) → interior_of X (metric_topology X d) (⋃ Fam) = Empty.
Apply andI to the current goal.
We prove the intermediate claim Hm: metric_on X d.
An exact proof term for the current goal is (andEL (metric_on X d) (∀seq : set, sequence_on seq X → cauchy_sequence X d seq → ∃x : set, converges_to X (metric_topology X d) seq x) Hc).
An exact proof term for the current goal is (metric_topology_is_topology X d Hm).
Let Fam be given.
Assume Hcount: countable_set Fam.
Assume Hclint: ∀A : set, A ∈ Fam → closed_in X (metric_topology X d) A ∧ interior_of X (metric_topology X d) A = Empty.
We will prove interior_of X (metric_topology X d) (⋃ Fam) = Empty.
An exact proof term for the current goal is (Baire_category_complete_metric_closed_core X d Fam Hc Hcount Hclint).
∎