Theorem subsfo

Description: Surreal subtraction is an onto function. (Contributed by Scott Fenton, 17-May-2025)

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

Proof

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