Theorem oa1cl

Description: A +o 1o is in On . (Contributed by RP, 27-Sep-2023)

	Ref	Expression
Assertion	oa1cl	⊢ ( 𝐴 ∈ On → ( 𝐴 +o 1o ) ∈ On )

Proof

Step	Hyp	Ref	Expression
1		1on	⊢ 1o ∈ On
2		oacl	⊢ ( ( 𝐴 ∈ On ∧ 1o ∈ On ) → ( 𝐴 +o 1o ) ∈ On )
3	1 2	mpan2	⊢ ( 𝐴 ∈ On → ( 𝐴 +o 1o ) ∈ On )