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	⊢ ( 𝑁 ∈ ω → ( 𝑁 +o 1o ) ∈ ran card )

Proof

Step	Hyp	Ref	Expression
1		nnon	⊢ ( 𝑁 ∈ ω → 𝑁 ∈ On )
2		oa1suc	⊢ ( 𝑁 ∈ On → ( 𝑁 +o 1o ) = suc 𝑁 )
3	1 2	syl	⊢ ( 𝑁 ∈ ω → ( 𝑁 +o 1o ) = suc 𝑁 )
4		peano2	⊢ ( 𝑁 ∈ ω → suc 𝑁 ∈ ω )
5	3 4	jca	⊢ ( 𝑁 ∈ ω → ( ( 𝑁 +o 1o ) = suc 𝑁 ∧ suc 𝑁 ∈ ω ) )
6		simpl	⊢ ( ( ( 𝑁 +o 1o ) = suc 𝑁 ∧ suc 𝑁 ∈ ω ) → ( 𝑁 +o 1o ) = suc 𝑁 )
7		simpr	⊢ ( ( ( 𝑁 +o 1o ) = suc 𝑁 ∧ suc 𝑁 ∈ ω ) → suc 𝑁 ∈ ω )
8	6 7	eqeltrd	⊢ ( ( ( 𝑁 +o 1o ) = suc 𝑁 ∧ suc 𝑁 ∈ ω ) → ( 𝑁 +o 1o ) ∈ ω )
9		omssrncard	⊢ ω ⊆ ran card
10	9	sseli	⊢ ( ( 𝑁 +o 1o ) ∈ ω → ( 𝑁 +o 1o ) ∈ ran card )
11	5 8 10	3syl	⊢ ( 𝑁 ∈ ω → ( 𝑁 +o 1o ) ∈ ran card )