Metamath Proof Explorer

Theorem oa1cl

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

		Ref	Expression
	Assertion	oa1cl	$⊢ A \in On \to A +_{𝑜} 1_{𝑜} \in On$

Step	Hyp	Ref	Expression
1		1on	$⊢ 1_{𝑜} \in On$
2		oacl	$⊢ (A \in On \land 1_{𝑜} \in On) \to A +_{𝑜} 1_{𝑜} \in On$
3	1 2	mpan2	$⊢ A \in On \to A +_{𝑜} 1_{𝑜} \in On$