TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-22‡ rests on unproved material (inherited)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

‡ Rests on 2 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Under choice, every metric space has a σ-discrete basis and ‡ Under choice, a regular T₁ space with a σ-locally-finite basis has a compatible normal sequence. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Collectionwise normal Moore spaces are metrizable

Statement

In $Z F C$ , every collectionwise normal Moore space is metrizable (Normalized families and collectionwise normality, Moore spaces and developments, Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not).

Facts & Assumptions

Given: A collectionwise normal Moore space $X$ .

[F1]

Collectionwise normality implies normality: for disjoint closed $A, B$ the two-member family ${A, B}$ is discrete, and separating it gives disjoint open sets containing $A$ and $B$ (Normalized families and collectionwise normality, Normal spaces and $T_{4}$ spaces, with the source disagreement over whether normality includes $T_{1}$ stated explicitly, Discrete families and $σ$ -locally-finite and $σ$ -discrete bases).

[F2]

Every collectionwise normal Moore space is screenable (Collectionwise normal Moore spaces are screenable).

[F3]

Every normal screenable Moore space is metrizable (Normal screenable Moore spaces are metrizable).

Proof

technique · direct

1.1

The space $X$ is normal by [F1] and screenable by [F2]; it is a Moore space by hypothesis.

givenF1F2

2.1

By [F3] applied to the normal screenable Moore space $X$ , the space is metrizable.

step 1.1F3∎

Remarks

This is Bing's Theorem 10 through Theorem 8. The separate screenability lemma is the combinatorial half of Bing's Theorem 10, and the metrization theorem is his Theorem 8 with the metrization criterion of Theorem 3; the two items are kept apart because the first carries the well-ordering argument and the second carries the metric construction.
No recorded result is used. Both suppliers are items of this page, proved before this one; the argument is short only because the work sits in those two items.

Depends on

Used by

PMEA implies the normal Moore space conjecture Theorem

Dependency tree · two levels

42 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

R. H. Bing, Metrization of topological spaces (standard reference, not scraped)