Theorem addsf

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

	Ref	Expression
Assertion	addsf	Could not format assertion : No typesetting found for |- +s : ( No X. No ) --> No with typecode |-

Proof

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