Theorem nmulfn

Description: Natural multiplication is a function over pairs of ordinals. (Contributed by Scott Fenton, 2-Jun-2026)

	Ref	Expression
Assertion	nmulfn	|- .no Fn ( On X. On )

Proof

Step	Hyp	Ref	Expression
1		df-nmul	|- .no = frecs ( { <. x , y >. | ( x e. ( On X. On ) /\ y e. ( On X. On ) /\ ( ( ( 1st ` x ) _E ( 1st ` y ) \/ ( 1st ` x ) = ( 1st ` y ) ) /\ ( ( 2nd ` x ) _E ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) /\ x =/= y ) ) } , ( On X. On ) , ( p e. _V , m e. _V |-> [_ ( 1st ` p ) / a ]_ [_ ( 2nd ` p ) / b ]_ |^| { z e. On | A. c e. a A. d e. b ( ( c m b ) +no ( a m d ) ) e. ( z +no ( c m d ) ) } ) )
2	1	on2recsfn	|- .no Fn ( On X. On )