Metamath Proof Explorer

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	$⊢ (A \in ω \land B \in ω) \to (A +_{𝑜} B \in ω \land A \cdot_{𝑜} B \in ω \land A ↑_{𝑜} B \in ω)$

Proof

Step	Hyp	Ref	Expression
1		nnacl	$⊢ (A \in ω \land B \in ω) \to A +_{𝑜} B \in ω$
2		nnmcl	$⊢ (A \in ω \land B \in ω) \to A \cdot_{𝑜} B \in ω$
3		nnecl	$⊢ (A \in ω \land B \in ω) \to A ↑_{𝑜} B \in ω$
4	1 2 3	3jca	$⊢ (A \in ω \land B \in ω) \to (A +_{𝑜} B \in ω \land A \cdot_{𝑜} B \in ω \land A ↑_{𝑜} B \in ω)$