Metamath Proof Explorer

Theorem addsf

Description: Function statement for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025)

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

Proof

Step Hyp Ref Expression
1 addsfn 
 |-  +s Fn ( No X. No )
2 addscl 
 |-  ( ( y e. No /\ z e. No ) -> ( y +s z ) e. No )
3 2 rgen2 
 |-  A. y e. No A. z e. No ( y +s z ) e. No
4 fveq2 
 |-  ( x = <. y , z >. -> ( +s ` x ) = ( +s ` <. y , z >. ) )
5 df-ov 
 |-  ( y +s z ) = ( +s ` <. y , z >. )
6 4 5 eqtr4di 
 |-  ( x = <. y , z >. -> ( +s ` x ) = ( y +s z ) )
7 6 eleq1d 
 |-  ( x = <. y , z >. -> ( ( +s ` x ) e. No <-> ( y +s z ) e. No ) )
8 7 ralxp 
 |-  ( A. x e. ( No X. No ) ( +s ` x ) e. No <-> A. y e. No A. z e. No ( y +s z ) e. No )
9 3 8 mpbir 
 |-  A. x e. ( No X. No ) ( +s ` x ) e. No
10 ffnfv 
 |-  ( +s : ( No X. No ) --> No <-> ( +s Fn ( No X. No ) /\ A. x e. ( No X. No ) ( +s ` x ) e. No ) )
11 1 9 10 mpbir2an 
 |-  +s : ( No X. No ) --> No