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\left(\mathrm{No}\times \mathrm{No}\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-adds	$$⊢{+}_s={norec2}_s\#A\#\left(\left(x\in \mathrm{V},a\in \mathrm{V}⟼\left(\left\{y|\exists l\in L\left(1^{st}\left(x\right)\right)y=la{2}^{nd}\left(x\right)\right\}\cup \left\{z|\exists l\in L\left(2^{nd}\left(x\right)\right)z=1^{st}\left(x\right)al\right\}\right){|}_s\left(\left\{y|\exists r\in R\left(1^{st}\left(x\right)\right)y=ra{2}^{nd}\left(x\right)\right\}\cup \left\{z|\exists r\in R\left(2^{nd}\left(x\right)\right)z=1^{st}\left(x\right)ar\right\}\right)\right)\right)$$
2	1	norec2fn	$$⊢{+}_{s}Fn\left(\mathrm{No}\times \mathrm{No}\right)$$