Theorem negsfo

Description: Function statement for surreal negation. (Contributed by Scott Fenton, 3-Feb-2025)

	Ref	Expression
Assertion	negsfo	|- -us : No -onto-> No

Proof

Step	Hyp	Ref	Expression
1		negsf	|- -us : No --> No
2		negscl	|- ( x e. No -> ( -us ` x ) e. No )
3		negnegs	|- ( x e. No -> ( -us ` ( -us ` x ) ) = x )
4	3	eqcomd	|- ( x e. No -> x = ( -us ` ( -us ` x ) ) )
5		fveq2	|- ( y = ( -us ` x ) -> ( -us ` y ) = ( -us ` ( -us ` x ) ) )
6	5	eqeq2d	|- ( y = ( -us ` x ) -> ( x = ( -us ` y ) <-> x = ( -us ` ( -us ` x ) ) ) )
7	6	rspcev	|- ( ( ( -us ` x ) e. No /\ x = ( -us ` ( -us ` x ) ) ) -> E. y e. No x = ( -us ` y ) )
8	2 4 7	syl2anc	|- ( x e. No -> E. y e. No x = ( -us ` y ) )
9	8	rgen	|- A. x e. No E. y e. No x = ( -us ` y )
10		dffo3	|- ( -us : No -onto-> No <-> ( -us : No --> No /\ A. x e. No E. y e. No x = ( -us ` y ) ) )
11	1 9 10	mpbir2an	|- -us : No -onto-> No