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

## Theorem

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

Let $\BB$ be a basis of $T$.

Then there exists a basis $\BB_0$ of $T$ such that

- $\BB_0 \subseteq \BB$ and $\card {\BB_0} = \map w T$

where:

- $\card {\BB_0}$ denotes the cardinality of $\BB_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 $\BB_1$ of $T$ such that:

- $(1): \quad \card {\BB_1} = \map w T$

We will prove:

- $(2): \quad \ds \forall U \in \BB_1: \exists \AA \subseteq \BB: U = \bigcup \AA \land \card \AA \le \map w T$

Let $U \in \BB_1$.

Let $S = \set {W \in \BB: W \subseteq U}$.

By definition of subset:

- $S \subseteq \BB$

By definition of basis: $\ds \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 $\AA \subseteq S$ such that:

- $\ds \bigcup \AA = \bigcup S$ and $\card \AA \le \map w T$

Thus by Subset Relation is Transitive:

- $\AA \subseteq \BB$.

Thus:

- $\ds U = \bigcup \AA \land \card \AA \le \map w T$

This ends proof of $(2)$.

By $(2)$ and Axiom of Choice there exists a mapping $f: \BB_1 \to \powerset \BB$ such that:

- $(3): \quad \ds \forall U \in \BB_1: U = \bigcup \map f U \land \card {\map f U} \le \map w T$

By Union is Smallest Superset, because $\forall U \in \BB_1: \map f U \subseteq \BB$:

- $\ds \bigcup_{U \mathop \in \BB_1} \map f U \subseteq \BB$

Set $\BB_0 := \ds \bigcup_{U \mathop \in \BB_1} \map f U = \bigcup \Img f$

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

By definition of basis:

- $\BB \subseteq \tau$

Thus by Subset Relation is Transitive:

- $\BB_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 \BB_1$ such that:

- $p \in U \subseteq A$.

By $(3)$, $U = \ds \bigcup \map f U$.

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

- $p \in D \in \map f U$

- $D \subseteq U$

By definition of union:

- $D \in \BB_0$

Thus by Subset Relation is Transitive:

- $\exists D \in \BB_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:

- $\card {\Img f} \le \map w T$

For every $U \in \BB_1$:

- $\card {\map f U} \le \map w T$

Then by Cardinality of Union not greater than Product:

- $\card {\BB_0} \le \card {\map w T \times \map w T}$

Thus by Cardinal Product Equal to Maximum, because $\map w T$ is infinite :

- $\card {\BB_0} \le \map w T$.

Thus by definition of weight:

- $\card {\BB_0} = \map w T$.

$\Box$

### Case when Weight is Finite

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

- $\BB_0 = \Img f)$

and:

- $\forall x \in X: \paren {x \in \map f x \land \forall U \in \tau: x \in U \implies \map f x \subseteq U}$

Thus by Image of Mapping of Intersections is Smallest Basis:

- $\BB_0 \subseteq \BB$

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

- $\card {\BB_0} \le \map w T$

Thus by definition of weight:

- $\card {\BB_0} = \map w T$

$\blacksquare$

## Sources

- Mizar article TOPGEN_2:18