Metamath Proof Explorer

Theorem negsf1o

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

Ref Expression
Assertion negsf1o 
|- -us : No -1-1-onto-> No

Proof

Step Hyp Ref Expression
1 negsf 
 |-  -us : No --> No
2 negs11 
 |-  ( ( x e. No /\ y e. No ) -> ( ( -us ` x ) = ( -us ` y ) <-> x = y ) )
3 2 biimpd 
 |-  ( ( x e. No /\ y e. No ) -> ( ( -us ` x ) = ( -us ` y ) -> x = y ) )
4 3 rgen2 
 |-  A. x e. No A. y e. No ( ( -us ` x ) = ( -us ` y ) -> x = y )
5 dff13 
 |-  ( -us : No -1-1-> No <-> ( -us : No --> No /\ A. x e. No A. y e. No ( ( -us ` x ) = ( -us ` y ) -> x = y ) ) )
6 1 4 5 mpbir2an 
 |-  -us : No -1-1-> No
7 negsfo 
 |-  -us : No -onto-> No
8 df-f1o 
 |-  ( -us : No -1-1-onto-> No <-> ( -us : No -1-1-> No /\ -us : No -onto-> No ) )
9 6 7 8 mpbir2an 
 |-  -us : No -1-1-onto-> No