Metamath Proof Explorer


Theorem negsfo

Description: Function statement for surreal negation. (Contributed by Scott Fenton, 3-Feb-2025)

Ref Expression
Assertion negsfo + s : No onto No

Proof

Step Hyp Ref Expression
1 negsf + s : No No
2 negscl x No + s x No
3 negnegs x No + s + s x = x
4 3 eqcomd x No x = + s + s x
5 fveq2 y = + s x + s y = + s + s x
6 5 eqeq2d y = + s x x = + s y x = + s + s x
7 6 rspcev + s x No x = + s + s x y No x = + s y
8 2 4 7 syl2anc x No y No x = + s y
9 8 rgen x No y No x = + s y
10 dffo3 + s : No onto No + s : No No x No y No x = + s y
11 1 9 10 mpbir2an + s : No onto No