Metamath Proof Explorer

Theorem addsfo

Description: Surreal addition is onto. (Contributed by Scott Fenton, 21-Jan-2025)

Ref Expression
Assertion addsfo 
|- +s : ( No X. No ) -onto-> No

Proof

Step Hyp Ref Expression
1 addsf 
 |-  +s : ( No X. No ) --> No
2 0sno 
 |-  0s e. No
3 opelxpi 
 |-  ( ( z e. No /\ 0s e. No ) -> <. z , 0s >. e. ( No X. No ) )
4 2 3 mpan2 
 |-  ( z e. No -> <. z , 0s >. e. ( No X. No ) )
5 addsrid 
 |-  ( z e. No -> ( z +s 0s ) = z )
6 5 eqcomd 
 |-  ( z e. No -> z = ( z +s 0s ) )
7 fveq2 
 |-  ( x = <. z , 0s >. -> ( +s ` x ) = ( +s ` <. z , 0s >. ) )
8 df-ov 
 |-  ( z +s 0s ) = ( +s ` <. z , 0s >. )
9 7 8 eqtr4di 
 |-  ( x = <. z , 0s >. -> ( +s ` x ) = ( z +s 0s ) )
10 9 rspceeqv 
 |-  ( ( <. z , 0s >. e. ( No X. No ) /\ z = ( z +s 0s ) ) -> E. x e. ( No X. No ) z = ( +s ` x ) )
11 4 6 10 syl2anc 
 |-  ( z e. No -> E. x e. ( No X. No ) z = ( +s ` x ) )
12 11 rgen 
 |-  A. z e. No E. x e. ( No X. No ) z = ( +s ` x )
13 dffo3 
 |-  ( +s : ( No X. No ) -onto-> No <-> ( +s : ( No X. No ) --> No /\ A. z e. No E. x e. ( No X. No ) z = ( +s ` x ) ) )
14 1 12 13 mpbir2an 
 |-  +s : ( No X. No ) -onto-> No