Theorem nnamecl

Description: Natural numbers are closed under ordinal addition, multiplication, and exponentiation. Theorem 2.20 of Schloeder p. 6. See nnacl , nnmcl , nnecl . (Contributed by RP, 29-Jan-2025)

	Ref	Expression
Assertion	nnamecl	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( 𝐴 +o 𝐵 ) ∈ ω ∧ ( 𝐴 ·o 𝐵 ) ∈ ω ∧ ( 𝐴 ↑o 𝐵 ) ∈ ω ) )

Proof

Step	Hyp	Ref	Expression
1		nnacl	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 +o 𝐵 ) ∈ ω )
2		nnmcl	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ·o 𝐵 ) ∈ ω )
3		nnecl	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ↑o 𝐵 ) ∈ ω )
4	1 2 3	3jca	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( 𝐴 +o 𝐵 ) ∈ ω ∧ ( 𝐴 ·o 𝐵 ) ∈ ω ∧ ( 𝐴 ↑o 𝐵 ) ∈ ω ) )