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 e. _om -> ( card ` A ) = A )

Proof

Step	Hyp	Ref	Expression
1		nnon	|- ( A e. _om -> A e. On )
2		onenon	|- ( A e. On -> A e. dom card )
3		cardid2	|- ( A e. dom card -> ( card ` A ) ~~ A )
4	1 2 3	3syl	|- ( A e. _om -> ( card ` A ) ~~ A )
5		nnfi	|- ( A e. _om -> A e. Fin )
6		ficardom	|- ( A e. Fin -> ( card ` A ) e. _om )
7	5 6	syl	|- ( A e. _om -> ( card ` A ) e. _om )
8		nneneq	|- ( ( ( card ` A ) e. _om /\ A e. _om ) -> ( ( card ` A ) ~~ A <-> ( card ` A ) = A ) )
9	7 8	mpancom	|- ( A e. _om -> ( ( card ` A ) ~~ A <-> ( card ` A ) = A ) )
10	4 9	mpbid	|- ( A e. _om -> ( card ` A ) = A )