finona1cl

Description: The finite ordinals are closed under the add one operation. (Contributed by RP, 27-Sep-2023)

		Ref	Expression
	Assertion	finona1cl	$⊢ N \in (On \cap Fin) \to N +_{𝑜} 1_{𝑜} \in (On \cap Fin)$

Step	Hyp	Ref	Expression
1		1onn	$⊢ 1_{𝑜} \in ω$
2		nnacl	$⊢ (N \in ω \land 1_{𝑜} \in ω) \to N +_{𝑜} 1_{𝑜} \in ω$
3	1 2	mpan2	$⊢ N \in ω \to N +_{𝑜} 1_{𝑜} \in ω$
4		onfin2	$⊢ ω = On \cap Fin$
5	4	eleq2i	$⊢ N \in ω \leftrightarrow N \in (On \cap Fin)$
6	4	eleq2i	$⊢ N +_{𝑜} 1_{𝑜} \in ω \leftrightarrow N +_{𝑜} 1_{𝑜} \in (On \cap Fin)$
7	3 5 6	3imtr3i	$⊢ N \in (On \cap Fin) \to N +_{𝑜} 1_{𝑜} \in (On \cap Fin)$

Metamath Proof Explorer