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 ∈ On ∧ B ∈ On → A + 𝑜 B ∈ On ∧ A ⋅ 𝑜 B ∈ On ∧ A ↑ 𝑜 B ∈ On

Proof

Step Hyp Ref Expression
1 oacl ⊢ A ∈ On ∧ B ∈ On → A + 𝑜 B ∈ On
2 omcl ⊢ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 B ∈ On
3 oecl ⊢ A ∈ On ∧ B ∈ On → A ↑ 𝑜 B ∈ On
4 1 2 3 3jca ⊢ A ∈ On ∧ B ∈ On → A + 𝑜 B ∈ On ∧ A ⋅ 𝑜 B ∈ On ∧ A ↑ 𝑜 B ∈ On