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	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 +o 𝐵 ) ∈ On ∧ ( 𝐴 ·o 𝐵 ) ∈ On ∧ ( 𝐴 ↑o 𝐵 ) ∈ On ) )

Proof

Step	Hyp	Ref	Expression
1		oacl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o 𝐵 ) ∈ On )
2		omcl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o 𝐵 ) ∈ On )
3		oecl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ↑o 𝐵 ) ∈ On )
4	1 2 3	3jca	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 +o 𝐵 ) ∈ On ∧ ( 𝐴 ·o 𝐵 ) ∈ On ∧ ( 𝐴 ↑o 𝐵 ) ∈ On ) )