Theorem finona1cl

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

	Ref	Expression
Assertion	finona1cl	|- ( N e. ( On i^i Fin ) -> ( N +o 1o ) e. ( On i^i Fin ) )

Proof

Step	Hyp	Ref	Expression
1		1onn	|- 1o e. _om
2		nnacl	|- ( ( N e. _om /\ 1o e. _om ) -> ( N +o 1o ) e. _om )
3	1 2	mpan2	|- ( N e. _om -> ( N +o 1o ) e. _om )
4		onfin2	|- _om = ( On i^i Fin )
5	4	eleq2i	|- ( N e. _om <-> N e. ( On i^i Fin ) )
6	4	eleq2i	|- ( ( N +o 1o ) e. _om <-> ( N +o 1o ) e. ( On i^i Fin ) )
7	3 5 6	3imtr3i	|- ( N e. ( On i^i Fin ) -> ( N +o 1o ) e. ( On i^i Fin ) )