Theorem alephsson

Description: The class of transfinite cardinals (the range of the aleph function) is a subclass of the class of ordinal numbers. (Contributed by NM, 11-Nov-2003)

	Ref	Expression
Assertion	alephsson	$$⊢\mathrm{ran}\aleph \subseteq \mathrm{On}$$

Proof

Step	Hyp	Ref	Expression
1		isinfcard	$$⊢\left(\mathrm{\omega }\subseteq x\wedge \mathrm{card}\left(x\right)=x\right)\leftrightarrow x\in \mathrm{ran}\aleph$$
2		cardon	$$⊢\mathrm{card}\left(x\right)\in \mathrm{On}$$
3		eleq1	$$⊢\mathrm{card}\left(x\right)=x\to \left(\mathrm{card}\left(x\right)\in \mathrm{On}\leftrightarrow x\in \mathrm{On}\right)$$
4	2 3	mpbii	$$⊢\mathrm{card}\left(x\right)=x\to x\in \mathrm{On}$$
5	4	adantl	$$⊢\left(\mathrm{\omega }\subseteq x\wedge \mathrm{card}\left(x\right)=x\right)\to x\in \mathrm{On}$$
6	1 5	sylbir	$$⊢x\in \mathrm{ran}\aleph \to x\in \mathrm{On}$$
7	6	ssriv	$$⊢\mathrm{ran}\aleph \subseteq \mathrm{On}$$