Theorem cardnn

Description: The cardinality of a natural number is the number. Corollary 10.23 of TakeutiZaring p. 90. (Contributed by Mario Carneiro, 7-Jan-2013)

	Ref	Expression
Assertion	cardnn	$$⊢A\in \mathrm{\omega }\to \mathrm{card}\left(A\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		nnon	$$⊢A\in \mathrm{\omega }\to A\in \mathrm{On}$$
2		onenon	$$⊢A\in \mathrm{On}\to A\in \mathrm{dom}\mathrm{card}$$
3		cardid2	$$⊢A\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left(A\right)\approx A$$
4	1 2 3	3syl	$$⊢A\in \mathrm{\omega }\to \mathrm{card}\left(A\right)\approx A$$
5		nnfi	$$⊢A\in \mathrm{\omega }\to A\in \mathrm{Fin}$$
6		ficardom	$$⊢A\in \mathrm{Fin}\to \mathrm{card}\left(A\right)\in \mathrm{\omega }$$
7	5 6	syl	$$⊢A\in \mathrm{\omega }\to \mathrm{card}\left(A\right)\in \mathrm{\omega }$$
8		nneneq	$$⊢\left(\mathrm{card}\left(A\right)\in \mathrm{\omega }\wedge A\in \mathrm{\omega }\right)\to \left(\mathrm{card}\left(A\right)\approx A\leftrightarrow \mathrm{card}\left(A\right)=A\right)$$
9	7 8	mpancom	$$⊢A\in \mathrm{\omega }\to \left(\mathrm{card}\left(A\right)\approx A\leftrightarrow \mathrm{card}\left(A\right)=A\right)$$
10	4 9	mpbid	$$⊢A\in \mathrm{\omega }\to \mathrm{card}\left(A\right)=A$$