Theorem naddfn

Description: Natural addition is a function over pairs of ordinals. (Contributed by Scott Fenton, 26-Aug-2024)

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

Proof

Step	Hyp	Ref	Expression
1		df-nadd	|- +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 ) , ( z e. _V , a e. _V |-> |^| { w e. On | ( ( a " ( { ( 1st ` z ) } X. ( 2nd ` z ) ) ) C_ w /\ ( a " ( ( 1st ` z ) X. { ( 2nd ` z ) } ) ) C_ w ) } ) )
2	1	on2recsfn	|- +no Fn ( On X. On )