Metamath Proof Explorer


Theorem negsf1o

Description: Surreal negation is a bijection. (Contributed by Scott Fenton, 3-Feb-2025)

Ref Expression
Assertion negsf1o + s : No 1-1 onto No

Proof

Step Hyp Ref Expression
1 negsf + s : No No
2 negs11 x No y No + s x = + s y x = y
3 2 biimpd x No y No + s x = + s y x = y
4 3 rgen2 x No y No + s x = + s y x = y
5 dff13 + s : No 1-1 No + s : No No x No y No + s x = + s y x = y
6 1 4 5 mpbir2an + s : No 1-1 No
7 negsfo + s : No onto No
8 df-f1o + s : No 1-1 onto No + s : No 1-1 No + s : No onto No
9 6 7 8 mpbir2an + s : No 1-1 onto No