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 \in ω \to N +_{𝑜} 1_{𝑜} \in ran card$

Step	Hyp	Ref	Expression
1		nnon	$⊢ N \in ω \to N \in On$
2		oa1suc	$⊢ N \in On \to N +_{𝑜} 1_{𝑜} = suc N$
3	1 2	syl	$⊢ N \in ω \to N +_{𝑜} 1_{𝑜} = suc N$
4		peano2	$⊢ N \in ω \to suc N \in ω$
5	3 4	jca	$⊢ N \in ω \to (N +_{𝑜} 1_{𝑜} = suc N \land suc N \in ω)$
6		simpl	$⊢ (N +_{𝑜} 1_{𝑜} = suc N \land suc N \in ω) \to N +_{𝑜} 1_{𝑜} = suc N$
7		simpr	$⊢ (N +_{𝑜} 1_{𝑜} = suc N \land suc N \in ω) \to suc N \in ω$
8	6 7	eqeltrd	$⊢ (N +_{𝑜} 1_{𝑜} = suc N \land suc N \in ω) \to N +_{𝑜} 1_{𝑜} \in ω$
9		omssrncard	$⊢ ω \subseteq ran card$
10	9	sseli	$⊢ N +_{𝑜} 1_{𝑜} \in ω \to N +_{𝑜} 1_{𝑜} \in ran card$
11	5 8 10	3syl	$⊢ N \in ω \to N +_{𝑜} 1_{𝑜} \in ran card$

Metamath Proof Explorer