Theorem addsfn

Description: Surreal addition is a function over pairs of surreals. (Contributed by Scott Fenton, 20-Aug-2024)

	Ref	Expression
Assertion	addsfn	|- +s Fn ( No X. No )

Proof

Step	Hyp	Ref	Expression
1		df-adds	|- +s = norec2 ( ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) )
2	1	norec2fn	|- +s Fn ( No X. No )