Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 omelon 
 |-  _om e. On
2 oncardid 
 |-  ( _om e. On -> ( card ` _om ) ~~ _om )
3 1 2 ax-mp 
 |-  ( card ` _om ) ~~ _om
4 nnsdom 
 |-  ( ( card ` _om ) e. _om -> ( card ` _om ) ~< _om )
5 sdomnen 
 |-  ( ( card ` _om ) ~< _om -> -. ( card ` _om ) ~~ _om )
6 4 5 syl 
 |-  ( ( card ` _om ) e. _om -> -. ( card ` _om ) ~~ _om )
7 3 6 mt2 
 |-  -. ( card ` _om ) e. _om
8 cardonle 
 |-  ( _om e. On -> ( card ` _om ) C_ _om )
9 1 8 ax-mp 
 |-  ( card ` _om ) C_ _om
10 cardon 
 |-  ( card ` _om ) e. On
11 10 1 onsseli 
 |-  ( ( card ` _om ) C_ _om <-> ( ( card ` _om ) e. _om \/ ( card ` _om ) = _om ) )
12 9 11 mpbi 
 |-  ( ( card ` _om ) e. _om \/ ( card ` _om ) = _om )
13 7 12 mtpor 
 |-  ( card ` _om ) = _om