Subset implies Cardinal Inequality
Let $S$ and $T$ be sets such that $S \subseteq T$.
- $T \sim \card T$
where $\card T$ denotes the cardinality of $T$.
- $\card S \le \card T$
For the proof:
- the ordering relation $\le$ for ordinals
- the subset relation $\subseteq$
shall be used interchangeably.
Let $f: T \to \card T$ be a bijection.
It follows that $f \restriction_S : S \to \card T$ is an injection.
It follows that $S \sim x$ by the definition of order isomorphism.
|\(\ds y\)||\(\in\)||\(\ds x\)|
|\(\ds \leadsto \ \ \)||\(\ds y\)||\(\le\)||\(\ds \map \phi y\)||Strictly Increasing Ordinal Mapping Inequality|
|\(\ds \)||\(\in\)||\(\ds f \sqbrk S\)||Definition of $\phi$|
|\(\ds \)||\(\subseteq\)||\(\ds \card T\)||Image Preserves Subsets|
|\(\ds \leadsto \ \ \)||\(\ds y\)||\(\in\)||\(\ds \card T\)||Cardinal Number is Ordinal|
Therefore, $y \in x \implies y \in \card T$ and $x \le \card T$ by the definition of subset.
But $\card S \le x$ by Cardinal Number Less than Ordinal.
So $\card S \le \card T$ by the fact that Subset Relation is Transitive.
- Mizar article CARD_1:11