Theorem omnaddcl

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

	Ref	Expression
Assertion	omnaddcl	|- ( ( A e. _om /\ B e. _om ) -> ( A +no B ) e. _om )

Proof

Step	Hyp	Ref	Expression
1		nnon	|- ( A e. _om -> A e. On )
2		naddoa	|- ( ( A e. On /\ B e. _om ) -> ( A +no B ) = ( A +o B ) )
3	1 2	sylan	|- ( ( A e. _om /\ B e. _om ) -> ( A +no B ) = ( A +o B ) )
4		nnacl	|- ( ( A e. _om /\ B e. _om ) -> ( A +o B ) e. _om )
5	3 4	eqeltrd	|- ( ( A e. _om /\ B e. _om ) -> ( A +no B ) e. _om )