Theorem addsf

Description: Function statement for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025)

	Ref	Expression
Assertion	addsf	$$⊢{+}_s:\mathrm{No}\times \mathrm{No}⟶\mathrm{No}$$

Proof

Step	Hyp	Ref	Expression
1		addsfn	$$⊢{+}_{s}Fn\left(\mathrm{No}\times \mathrm{No}\right)$$
2		addscl	$$⊢\left(y\in \mathrm{No}\wedge z\in \mathrm{No}\right)\to y{+}_{s}z\in \mathrm{No}$$
3	2	rgen2	$$⊢\forall y\in \mathrm{No}\forall z\in \mathrm{No}y{+}_{s}z\in \mathrm{No}$$
4		fveq2	$$⊢x=⟨y,z⟩\to {+}_s\left(x\right)={+}_s\left(⟨y,z⟩\right)$$
5		df-ov	$$⊢y{+}_{s}z={+}_s\left(⟨y,z⟩\right)$$
6	4 5	eqtr4di	$$⊢x=⟨y,z⟩\to {+}_s\left(x\right)=y{+}_{s}z$$
7	6	eleq1d	$$⊢x=⟨y,z⟩\to \left({+}_s\left(x\right)\in \mathrm{No}\leftrightarrow y{+}_{s}z\in \mathrm{No}\right)$$
8	7	ralxp	$$⊢\forall x\in \left(\mathrm{No}\times \mathrm{No}\right){+}_s\left(x\right)\in \mathrm{No}\leftrightarrow \forall y\in \mathrm{No}\forall z\in \mathrm{No}y{+}_{s}z\in \mathrm{No}$$
9	3 8	mpbir	$$⊢\forall x\in \left(\mathrm{No}\times \mathrm{No}\right){+}_s\left(x\right)\in \mathrm{No}$$
10		ffnfv	$$⊢{+}_s:\mathrm{No}\times \mathrm{No}⟶\mathrm{No}\leftrightarrow \left({+}_{s}Fn\left(\mathrm{No}\times \mathrm{No}\right)\wedge \forall x\in \left(\mathrm{No}\times \mathrm{No}\right){+}_s\left(x\right)\in \mathrm{No}\right)$$
11	1 9 10	mpbir2an	$$⊢{+}_s:\mathrm{No}\times \mathrm{No}⟶\mathrm{No}$$