Theorem negsproplem3

Description: Lemma for surreal negation. Give the cut properties of surreal negation. (Contributed by Scott Fenton, 2-Feb-2025)

	Ref	Expression
Hypotheses	negsproplem.1	No typesetting found for |- ( ph -> A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
	negsproplem2.1	$$⊢\phi \to A\in \mathrm{No}$$
Assertion	negsproplem3	Could not format assertion : No typesetting found for |- ( ph -> ( ( -us ` A ) e. No /\ ( -us " ( _Right ` A ) ) <

Proof

Step	Hyp	Ref	Expression
1		negsproplem.1	Could not format ( ph -> A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -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 ` B ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
2		negsproplem2.1	$$⊢\phi \to A\in \mathrm{No}$$
3	1 2	negsproplem2	Could not format ( ph -> ( -us " ( _Right ` A ) ) < ( -us " ( _Right ` A ) ) <
4		scutcut	Could not format ( ( -us " ( _Right ` A ) ) < ( ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) e. No /\ ( -us " ( _Right ` A ) ) < ( ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) e. No /\ ( -us " ( _Right ` A ) ) <
5	3 4	syl	Could not format ( ph -> ( ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) e. No /\ ( -us " ( _Right ` A ) ) < ( ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) e. No /\ ( -us " ( _Right ` A ) ) <
6		negsval	Could not format ( A e. No -> ( -us ` A ) = ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) ) : No typesetting found for |- ( A e. No -> ( -us ` A ) = ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) ) with typecode |-
7	2 6	syl	Could not format ( ph -> ( -us ` A ) = ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) ) : No typesetting found for |- ( ph -> ( -us ` A ) = ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) ) with typecode |-
8	7	eleq1d	Could not format ( ph -> ( ( -us ` A ) e. No <-> ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) e. No ) ) : No typesetting found for |- ( ph -> ( ( -us ` A ) e. No <-> ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) e. No ) ) with typecode |-
9	7	sneqd	Could not format ( ph -> { ( -us ` A ) } = { ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) } ) : No typesetting found for |- ( ph -> { ( -us ` A ) } = { ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) } ) with typecode |-
10	9	breq2d	Could not format ( ph -> ( ( -us " ( _Right ` A ) ) < ( -us " ( _Right ` A ) ) < ( ( -us " ( _Right ` A ) ) < ( -us " ( _Right ` A ) ) <
11	9	breq1d	Could not format ( ph -> ( { ( -us ` A ) } < { ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) } < ( { ( -us ` A ) } < { ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) } <
12	8 10 11	3anbi123d	Could not format ( ph -> ( ( ( -us ` A ) e. No /\ ( -us " ( _Right ` A ) ) < ( ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) e. No /\ ( -us " ( _Right ` A ) ) < ( ( ( -us ` A ) e. No /\ ( -us " ( _Right ` A ) ) < ( ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) e. No /\ ( -us " ( _Right ` A ) ) <
13	5 12	mpbird	Could not format ( ph -> ( ( -us ` A ) e. No /\ ( -us " ( _Right ` A ) ) < ( ( -us ` A ) e. No /\ ( -us " ( _Right ` A ) ) <