Theorem negscut

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

	Ref	Expression
Assertion	negscut	Could not format assertion : No typesetting found for |- ( A e. No -> ( ( -us ` A ) e. No /\ ( -us " ( _Right ` A ) ) <

Proof

Step	Hyp	Ref	Expression
1		negsprop	Could not format ( ( x e. No /\ y e. No ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( -us ` x ) e. No /\ ( x ( -us ` y )
2	1	a1d	Could not format ( ( x e. No /\ y e. No ) -> ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` 0s ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` 0s ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
3	2	rgen2	Could not format 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 ) ( ( -us ` x ) e. No /\ ( x ( -us ` y )
4	3	a1i	Could not format ( 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 ) 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\in \mathrm{No}\to A\in \mathrm{No}$$
6	4 5	negsproplem3	Could not format ( A e. No -> ( ( -us ` A ) e. No /\ ( -us " ( _Right ` A ) ) < ( ( -us ` A ) e. No /\ ( -us " ( _Right ` A ) ) <