Metamath Proof Explorer


Theorem subsfo

Description: Surreal subtraction is an onto function. (Contributed by Scott Fenton, 17-May-2025)

Ref Expression
Assertion subsfo - s : No × No onto No

Proof

Step Hyp Ref Expression
1 subsf - s : No × No No
2 0sno 0 s No
3 opelxpi x No 0 s No x 0 s No × No
4 2 3 mpan2 x No x 0 s No × No
5 subsval x No 0 s No x - s 0 s = x + s + s 0 s
6 2 5 mpan2 x No x - s 0 s = x + s + s 0 s
7 negs0s + s 0 s = 0 s
8 7 oveq2i x + s + s 0 s = x + s 0 s
9 addsrid x No x + s 0 s = x
10 8 9 eqtrid x No x + s + s 0 s = x
11 6 10 eqtr2d x No x = x - s 0 s
12 fveq2 y = x 0 s - s y = - s x 0 s
13 df-ov x - s 0 s = - s x 0 s
14 12 13 eqtr4di y = x 0 s - s y = x - s 0 s
15 14 rspceeqv x 0 s No × No x = x - s 0 s y No × No x = - s y
16 4 11 15 syl2anc x No y No × No x = - s y
17 16 rgen x No y No × No x = - s y
18 dffo3 - s : No × No onto No - s : No × No No x No y No × No x = - s y
19 1 17 18 mpbir2an - s : No × No onto No