Metamath Proof Explorer

Theorem nna1iscard

Description: For any natural number, the add one operation is results in a cardinal number. (Contributed by RP, 1-Oct-2023)

Ref Expression
Assertion nna1iscard 
|- ( N e. _om -> ( N +o 1o ) e. ran card )

Proof

Step Hyp Ref Expression
1 nnon 
 |-  ( N e. _om -> N e. On )
2 oa1suc 
 |-  ( N e. On -> ( N +o 1o ) = suc N )
3 1 2 syl 
 |-  ( N e. _om -> ( N +o 1o ) = suc N )
4 peano2 
 |-  ( N e. _om -> suc N e. _om )
5 3 4 jca 
 |-  ( N e. _om -> ( ( N +o 1o ) = suc N /\ suc N e. _om ) )
6 simpl 
 |-  ( ( ( N +o 1o ) = suc N /\ suc N e. _om ) -> ( N +o 1o ) = suc N )
7 simpr 
 |-  ( ( ( N +o 1o ) = suc N /\ suc N e. _om ) -> suc N e. _om )
8 6 7 eqeltrd 
 |-  ( ( ( N +o 1o ) = suc N /\ suc N e. _om ) -> ( N +o 1o ) e. _om )
9 omssrncard 
 |-  _om C_ ran card
10 9 sseli 
 |-  ( ( N +o 1o ) e. _om -> ( N +o 1o ) e. ran card )
11 5 8 10 3syl 
 |-  ( N e. _om -> ( N +o 1o ) e. ran card )