Theorem negscut

Description: The cut properties of surreal negation. (Contributed by Scott Fenton, 3-Feb-2025)

	Ref	Expression
Assertion	negscut	|- ( A e. No -> ( ( -us ` A ) e. No /\ ( -us " ( _Right ` A ) ) <

Proof

Step	Hyp	Ref	Expression
1		negsprop	|- ( ( x e. No /\ y e. No ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
2	1	a1d	|- ( ( x e. No /\ y e. No ) -> ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` 0s ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
3	2	rgen2	|- A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` 0s ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
4	3	a1i	|- ( A e. No -> A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` 0s ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
5		id	|- ( A e. No -> A e. No )
6	4 5	negsproplem3	|- ( A e. No -> ( ( -us ` A ) e. No /\ ( -us " ( _Right ` A ) ) <