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 X. No ) -onto-> No

Proof

Step Hyp Ref Expression
1 subsf 
 |-  -s : ( No X. No ) --> No
2 0sno 
 |-  0s e. No
3 opelxpi 
 |-  ( ( x e. No /\ 0s e. No ) -> <. x , 0s >. e. ( No X. No ) )
4 2 3 mpan2 
 |-  ( x e. No -> <. x , 0s >. e. ( No X. No ) )
5 subsval 
 |-  ( ( x e. No /\ 0s e. No ) -> ( x -s 0s ) = ( x +s ( -us ` 0s ) ) )
6 2 5 mpan2 
 |-  ( x e. No -> ( x -s 0s ) = ( x +s ( -us ` 0s ) ) )
7 negs0s 
 |-  ( -us ` 0s ) = 0s
8 7 oveq2i 
 |-  ( x +s ( -us ` 0s ) ) = ( x +s 0s )
9 addsrid 
 |-  ( x e. No -> ( x +s 0s ) = x )
10 8 9 eqtrid 
 |-  ( x e. No -> ( x +s ( -us ` 0s ) ) = x )
11 6 10 eqtr2d 
 |-  ( x e. No -> x = ( x -s 0s ) )
12 fveq2 
 |-  ( y = <. x , 0s >. -> ( -s ` y ) = ( -s ` <. x , 0s >. ) )
13 df-ov 
 |-  ( x -s 0s ) = ( -s ` <. x , 0s >. )
14 12 13 eqtr4di 
 |-  ( y = <. x , 0s >. -> ( -s ` y ) = ( x -s 0s ) )
15 14 rspceeqv 
 |-  ( ( <. x , 0s >. e. ( No X. No ) /\ x = ( x -s 0s ) ) -> E. y e. ( No X. No ) x = ( -s ` y ) )
16 4 11 15 syl2anc 
 |-  ( x e. No -> E. y e. ( No X. No ) x = ( -s ` y ) )
17 16 rgen 
 |-  A. x e. No E. y e. ( No X. No ) x = ( -s ` y )
18 dffo3 
 |-  ( -s : ( No X. No ) -onto-> No <-> ( -s : ( No X. No ) --> No /\ A. x e. No E. y e. ( No X. No ) x = ( -s ` y ) ) )
19 1 17 18 mpbir2an 
 |-  -s : ( No X. No ) -onto-> No