Theorem addsfo

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

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

Proof

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