Theorem addsfo

Description: Surreal addition is onto. (Contributed by Scott Fenton, 21-Jan-2025)

	Ref	Expression
Assertion	addsfo	$$⊢{+}_s:\mathrm{No}\times \mathrm{No}\underset{onto}{⟶}\mathrm{No}$$

Proof

Step	Hyp	Ref	Expression
1		addsf	$$⊢{+}_s:\mathrm{No}\times \mathrm{No}⟶\mathrm{No}$$
2		0sno	$$⊢0_s\in \mathrm{No}$$
3		opelxpi	$$⊢\left(z\in \mathrm{No}\wedge 0_s\in \mathrm{No}\right)\to ⟨z,0_s⟩\in \left(\mathrm{No}\times \mathrm{No}\right)$$
4	2 3	mpan2	$$⊢z\in \mathrm{No}\to ⟨z,0_s⟩\in \left(\mathrm{No}\times \mathrm{No}\right)$$
5		addsrid	$$⊢z\in \mathrm{No}\to z{+}_s{0}_s=z$$
6	5	eqcomd	$$⊢z\in \mathrm{No}\to z=z{+}_s{0}_s$$
7		fveq2	$$⊢x=⟨z,0_s⟩\to {+}_s\left(x\right)={+}_s\left(⟨z,0_s⟩\right)$$
8		df-ov	$$⊢z{+}_s{0}_s={+}_s\left(⟨z,0_s⟩\right)$$
9	7 8	eqtr4di	$$⊢x=⟨z,0_s⟩\to {+}_s\left(x\right)=z{+}_s{0}_s$$
10	9	rspceeqv	$$⊢\left(⟨z,0_s⟩\in \left(\mathrm{No}\times \mathrm{No}\right)\wedge z=z{+}_s{0}_s\right)\to \exists x\in \left(\mathrm{No}\times \mathrm{No}\right)z={+}_s\left(x\right)$$
11	4 6 10	syl2anc	$$⊢z\in \mathrm{No}\to \exists x\in \left(\mathrm{No}\times \mathrm{No}\right)z={+}_s\left(x\right)$$
12	11	rgen	$$⊢\forall z\in \mathrm{No}\exists x\in \left(\mathrm{No}\times \mathrm{No}\right)z={+}_s\left(x\right)$$
13		dffo3	$$⊢{+}_s:\mathrm{No}\times \mathrm{No}\underset{onto}{⟶}\mathrm{No}\leftrightarrow \left({+}_s:\mathrm{No}\times \mathrm{No}⟶\mathrm{No}\wedge \forall z\in \mathrm{No}\exists x\in \left(\mathrm{No}\times \mathrm{No}\right)z={+}_s\left(x\right)\right)$$
14	1 12 13	mpbir2an	$$⊢{+}_s:\mathrm{No}\times \mathrm{No}\underset{onto}{⟶}\mathrm{No}$$