Metamath Proof Explorer

Theorem sucomisnotcard

Description: _om +o 1o is not a cardinal number. (Contributed by RP, 1-Oct-2023)

Ref Expression
Assertion sucomisnotcard 
|- -. ( _om +o 1o ) e. ran card

Proof

Step Hyp Ref Expression
1 omelon 
 |-  _om e. On
2 sucidg 
 |-  ( _om e. On -> _om e. suc _om )
3 1 2 ax-mp 
 |-  _om e. suc _om
4 omensuc 
 |-  _om ~~ suc _om
5 breq1 
 |-  ( x = _om -> ( x ~~ suc _om <-> _om ~~ suc _om ) )
6 5 rspcev 
 |-  ( ( _om e. suc _om /\ _om ~~ suc _om ) -> E. x e. suc _om x ~~ suc _om )
7 3 4 6 mp2an 
 |-  E. x e. suc _om x ~~ suc _om
8 dfrex2 
 |-  ( E. x e. suc _om x ~~ suc _om <-> -. A. x e. suc _om -. x ~~ suc _om )
9 7 8 mpbi 
 |-  -. A. x e. suc _om -. x ~~ suc _om
10 9 intnan 
 |-  -. ( suc _om e. On /\ A. x e. suc _om -. x ~~ suc _om )
11 oa1suc 
 |-  ( _om e. On -> ( _om +o 1o ) = suc _om )
12 1 11 ax-mp 
 |-  ( _om +o 1o ) = suc _om
13 12 eleq1i 
 |-  ( ( _om +o 1o ) e. ran card <-> suc _om e. ran card )
14 elrncard 
 |-  ( suc _om e. ran card <-> ( suc _om e. On /\ A. x e. suc _om -. x ~~ suc _om ) )
15 13 14 sylbb 
 |-  ( ( _om +o 1o ) e. ran card -> ( suc _om e. On /\ A. x e. suc _om -. x ~~ suc _om ) )
16 10 15 mto 
 |-  -. ( _om +o 1o ) e. ran card