Metamath Proof Explorer

Theorem oaomoecl

Description: The operations of addition, multiplication, and exponentiation are closed. Remark 2.8 of Schloeder p. 5. See oacl , omcl , oecl . (Contributed by RP, 18-Jan-2025)

		Ref	Expression
	Assertion	oaomoecl	$⊢ (A \in On \land B \in On) \to (A +_{𝑜} B \in On \land A \cdot_{𝑜} B \in On \land A ↑_{𝑜} B \in On)$

Proof

Step	Hyp	Ref	Expression
1		oacl	$⊢ (A \in On \land B \in On) \to A +_{𝑜} B \in On$
2		omcl	$⊢ (A \in On \land B \in On) \to A \cdot_{𝑜} B \in On$
3		oecl	$⊢ (A \in On \land B \in On) \to A ↑_{𝑜} B \in On$
4	1 2 3	3jca	$⊢ (A \in On \land B \in On) \to (A +_{𝑜} B \in On \land A \cdot_{𝑜} B \in On \land A ↑_{𝑜} B \in On)$