Theorem nmulfn

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

	Ref	Expression
Assertion	nmulfn	Could not format assertion : No typesetting found for |- .no Fn ( On X. On ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-nmul	Could not format .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 ) ) } ) ) : No typesetting found for |- .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 ) ) } ) ) with typecode |-
2	1	on2recsfn	Could not format .no Fn ( On X. On ) : No typesetting found for |- .no Fn ( On X. On ) with typecode |-