Theorem cardom

Description: The set of natural numbers is a cardinal number. Theorem 18.11 of Monk1 p. 133. (Contributed by NM, 28-Oct-2003)

	Ref	Expression
Assertion	cardom	$$⊢\mathrm{card}\left(\mathrm{\omega }\right)=\mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		omelon	$$⊢\mathrm{\omega }\in \mathrm{On}$$
2		oncardid	$$⊢\mathrm{\omega }\in \mathrm{On}\to \mathrm{card}\left(\mathrm{\omega }\right)\approx \mathrm{\omega }$$
3	1 2	ax-mp	$$⊢\mathrm{card}\left(\mathrm{\omega }\right)\approx \mathrm{\omega }$$
4		nnsdom	$$⊢\mathrm{card}\left(\mathrm{\omega }\right)\in \mathrm{\omega }\to \mathrm{card}\left(\mathrm{\omega }\right)\prec \mathrm{\omega }$$
5		sdomnen	$$⊢\mathrm{card}\left(\mathrm{\omega }\right)\prec \mathrm{\omega }\to \neg \mathrm{card}\left(\mathrm{\omega }\right)\approx \mathrm{\omega }$$
6	4 5	syl	$$⊢\mathrm{card}\left(\mathrm{\omega }\right)\in \mathrm{\omega }\to \neg \mathrm{card}\left(\mathrm{\omega }\right)\approx \mathrm{\omega }$$
7	3 6	mt2	$$⊢\neg \mathrm{card}\left(\mathrm{\omega }\right)\in \mathrm{\omega }$$
8		cardonle	$$⊢\mathrm{\omega }\in \mathrm{On}\to \mathrm{card}\left(\mathrm{\omega }\right)\subseteq \mathrm{\omega }$$
9	1 8	ax-mp	$$⊢\mathrm{card}\left(\mathrm{\omega }\right)\subseteq \mathrm{\omega }$$
10		cardon	$$⊢\mathrm{card}\left(\mathrm{\omega }\right)\in \mathrm{On}$$
11	10 1	onsseli	$$⊢\mathrm{card}\left(\mathrm{\omega }\right)\subseteq \mathrm{\omega }\leftrightarrow \left(\mathrm{card}\left(\mathrm{\omega }\right)\in \mathrm{\omega }\vee \mathrm{card}\left(\mathrm{\omega }\right)=\mathrm{\omega }\right)$$
12	9 11	mpbi	$$⊢\left(\mathrm{card}\left(\mathrm{\omega }\right)\in \mathrm{\omega }\vee \mathrm{card}\left(\mathrm{\omega }\right)=\mathrm{\omega }\right)$$
13	7 12	mtpor	$$⊢\mathrm{card}\left(\mathrm{\omega }\right)=\mathrm{\omega }$$