Metamath Proof Explorer

Theorem nmulcl

Description: Closure law for natural multiplication. (Contributed by Scott Fenton, 10-Jun-2026)

		Ref	Expression
	Assertion	nmulcl	\|- ( ( A e. On /\ B e. On ) -> ( A .no B ) e. On )

Proof

Step	Hyp	Ref	Expression
1		nmulprop	\|- ( ( A e. On /\ B e. On ) -> ( ( A .no B ) e. On /\ ( A .no B ) = \|^\| { x e. On \| A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) )
2	1	simpld	\|- ( ( A e. On /\ B e. On ) -> ( A .no B ) e. On )

Step

Hyp

Ref

Expression

nmulprop

 |-  ( ( A e. On /\ B e. On ) -> ( ( A .no B ) e. On /\ ( A .no B ) = |^| { x e. On | A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) )

simpld

 |-  ( ( A e. On /\ B e. On ) -> ( A .no B ) e. On )