Metamath Proof Explorer

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 
|- ( 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 
|- ( ph -> A e. No )
Assertion negsproplem3 
|- ( ph -> ( ( -us ` A ) e. No /\ ( -us " ( _Right ` A ) ) <

Proof

Step Hyp Ref Expression
1 negsproplem.1 
 |-  ( 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 )
2 negsproplem2.1 
 |-  ( ph -> A e. No )
3 1 2 negsproplem2 
 |-  ( ph -> ( -us " ( _Right ` A ) ) <
4 scutcut 
 |-  ( ( -us " ( _Right ` A ) ) < ( ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) e. No /\ ( -us " ( _Right ` A ) ) <
5 3 4 syl 
 |-  ( ph -> ( ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) e. No /\ ( -us " ( _Right ` A ) ) <
6 negsval 
 |-  ( A e. No -> ( -us ` A ) = ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) )
7 2 6 syl 
 |-  ( ph -> ( -us ` A ) = ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) )
8 7 eleq1d 
 |-  ( ph -> ( ( -us ` A ) e. No <-> ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) e. No ) )
9 7 sneqd 
 |-  ( ph -> { ( -us ` A ) } = { ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) } )
10 9 breq2d 
 |-  ( ph -> ( ( -us " ( _Right ` A ) ) < ( -us " ( _Right ` A ) ) <
11 9 breq1d 
 |-  ( ph -> ( { ( -us ` A ) } < { ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) } <
12 8 10 11 3anbi123d 
 |-  ( ph -> ( ( ( -us ` A ) e. No /\ ( -us " ( _Right ` A ) ) < ( ( ( -us " ( _Right ` A ) ) |s ( -us " ( _Left ` A ) ) ) e. No /\ ( -us " ( _Right ` A ) ) <
13 5 12 mpbird 
 |-  ( ph -> ( ( -us ` A ) e. No /\ ( -us " ( _Right ` A ) ) <