Metamath Proof Explorer

Theorem omnaddcl

Description: The naturals are closed under natural addition. (Contributed by Scott Fenton, 20-Aug-2025)

		Ref	Expression
	Assertion	omnaddcl	$⊢ (A \in ω \land B \in ω) \to A + B \in ω$

Step	Hyp	Ref	Expression
1		nnon	$⊢ A \in ω \to A \in On$
2		naddoa	$⊢ (A \in On \land B \in ω) \to A + B = A +_{𝑜} B$
3	1 2	sylan	$⊢ (A \in ω \land B \in ω) \to A + B = A +_{𝑜} B$
4		nnacl	$⊢ (A \in ω \land B \in ω) \to A +_{𝑜} B \in ω$
5	3 4	eqeltrd	$⊢ (A \in ω \land B \in ω) \to A + B \in ω$