# Basis has Subset Basis of Cardinality equal to Weight of Space

## Contents

## Theorem

Let $T = \struct {X, \tau}$ be a topological space.

Let $\mathcal B$ be a basis of $T$.

Then there exists a basis $\mathcal B_0$ of $T$ such that

- $\mathcal B_0 \subseteq \mathcal B$ and $\card {\mathcal B_0} = \map w T$

where:

- $\card {\mathcal B_0}$ denotes the cardinality of $\mathcal B_0$
- $\map w T$ denotes the weight of $T$.

## Proof

There are two cases:

### Case when Weight is Infinite

By definition of weight there exists a basis $\mathcal B_1$ of $T$ such that

- $(1): \quad \left\vert{\mathcal B_1}\right\vert = w \left({T}\right)$

We will prove:

- $(2): \quad \forall U \in \mathcal B_1: \exists \mathcal A \subseteq \mathcal B: U = \bigcup \mathcal A \land \left\vert{\mathcal A}\right\vert \le w \left({T}\right)$

Let $U \in \mathcal B_1$.

Let $S = \left\{ {W \in \mathcal B: W \subseteq U}\right\}$.

By definition of subset:

- $S \subseteq \mathcal B$

By definition of basis: $\bigcup S = U$

By definition of set $S$, $S$ is set of open subset of $T$.

Then by Existence of Subfamily of Cardinality not greater than Weight of Space and Unions Equal there exists a subset $\mathcal A \subseteq S$ such that:

- $\bigcup \mathcal A = \bigcup S$ and $\left\vert{\mathcal A}\right\vert \le w \left({T}\right)$

Thus by Subset Relation is Transitive:

- $\mathcal A \subseteq \mathcal B$.

Thus:

- $\displaystyle U = \bigcup \mathcal A \land \left\vert{\mathcal A}\right\vert \le w \left({T}\right)$

This ends proof of $(2)$.

By $(2)$ and Axiom of Choice there exists a mapping $f: \mathcal B_1 \to \mathcal P \left({\mathcal B}\right)$ such that:

- $(3): \quad \forall U \in \mathcal B_1: U = \bigcup f \left({U}\right) \land \left\vert{f \left({U}\right)}\right\vert \le w \left({T}\right)$

By Union is Smallest Superset because $\forall U \in \mathcal B_1: f \left({U}\right) \subseteq \mathcal B$:

- $\bigcup_{U \in \mathcal B_1} f \left({U}\right) \subseteq \mathcal B$

Set $\mathcal B_0 := \bigcup_{U \in \mathcal B_1} f \left({U}\right) = \bigcup \operatorname{Im} \left({f}\right)$

Now we will show that $\mathcal B_0$ is basis of $T$.

By definition of basis:

- $\mathcal B \subseteq \tau$

Thus by Subset Relation is Transitive:

- $\mathcal B_0 \subseteq \tau$

Let $A$ be an open subset of $X$.

Let $p$ be a point of $X$ such that $p \in A$.

Then by definition of basis there exists $U \in \mathcal B_1$ such that:

- $p \in U \subseteq A$.

By $(3)$, $U = \bigcup f \left({U}\right)$.

Then by definition of union there exists a set $D$ such that:

- $p \in D \in f \left({U}\right)$

- $D \subseteq U$

by definition of union:

- $D \in \mathcal B_0$

Thus by Subset Relation is Transitive:

- $\exists D \in \mathcal B_0: p \in D \subseteq A$

This by definition of basis ends a proof of basis.

By $(1)$ and Cardinality of Image of Mapping not greater than Cardinality of Domain:

- $\left\vert \operatorname{Im}\left( f \right) \right\vert \leq w \left( T \right)$.

For every $U \in \mathcal B_1$, $\left\vert f \left( U \right) \right\vert \leq w \left( T \right)$.

Then by Cardinality of Union not greater than Product:

- $\left\vert \mathcal B_0 \right\vert \leq \left\vert w \left( T \right) \times w \left( T \right) \right\vert$.

Thus by Cardinal Product Equal to Maximum because $w \left( T \right)$ is infinite

- $\left\vert \mathcal B_0 \right\vert \leq w \left( T \right)$.

Thus by definition of weight:

- $\left\vert \mathcal B_0 \right\vert = w \left( T \right)$.

$\Box$

### Case when Weight is Finite

By Finite Weight Space has Basis equal Image of Mapping of Intersections there exist a basis $\mathcal B_0$ of $T$ and a mapping $f:X \to \tau$ such that

- $\mathcal B_0 = \operatorname{Im} \left({f}\right)$ and
- $\forall x \in X: \left({x \in f \left({x}\right) \land \forall U \in \tau: x \in U \implies f \left({x}\right) \subseteq U}\right)$.

Thus by Image of Mapping of Intersections is Smallest Basis:

- $\mathcal B_0 \subseteq \mathcal B$.

Thus by Cardinality of Image of Mapping of Intersections is not greater than Weight of Space:

- $\left\vert{\mathcal B_0}\right\vert \leq w \left({T}\right)$.

Thus by definition of weight:

- $\left\vert \mathcal B_0 \right\vert = w \left( T \right)$.

$\blacksquare$

## Sources

- Mizar article TOPGEN_2:18