Theorem finona1cl

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

	Ref	Expression
Assertion	finona1cl	⊢ ( 𝑁 ∈ ( On ∩ Fin ) → ( 𝑁 +o 1o ) ∈ ( On ∩ Fin ) )

Proof

Step	Hyp	Ref	Expression
1		1onn	⊢ 1o ∈ ω
2		nnacl	⊢ ( ( 𝑁 ∈ ω ∧ 1o ∈ ω ) → ( 𝑁 +o 1o ) ∈ ω )
3	1 2	mpan2	⊢ ( 𝑁 ∈ ω → ( 𝑁 +o 1o ) ∈ ω )
4		onfin2	⊢ ω = ( On ∩ Fin )
5	4	eleq2i	⊢ ( 𝑁 ∈ ω ↔ 𝑁 ∈ ( On ∩ Fin ) )
6	4	eleq2i	⊢ ( ( 𝑁 +o 1o ) ∈ ω ↔ ( 𝑁 +o 1o ) ∈ ( On ∩ Fin ) )
7	3 5 6	3imtr3i	⊢ ( 𝑁 ∈ ( On ∩ Fin ) → ( 𝑁 +o 1o ) ∈ ( On ∩ Fin ) )