This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )