Metamath Proof Explorer

Theorem addscut2

Description: Show that the cut involved in surreal addition is legitimate. (Contributed by Scott Fenton, 8-Mar-2025)

Ref Expression
Hypotheses addscut.1 
|- ( ph -> X e. No )
addscut.2 
|- ( ph -> Y e. No )
Assertion addscut2 
|- ( ph -> ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <

Proof

Step Hyp Ref Expression
1 addscut.1 
 |-  ( ph -> X e. No )
2 addscut.2 
 |-  ( ph -> Y e. No )
3 1 2 addscut 
 |-  ( ph -> ( ( X +s Y ) e. No /\ ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <
4 3anass 
 |-  ( ( ( X +s Y ) e. No /\ ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) < ( ( X +s Y ) e. No /\ ( ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <
5 3 4 sylib 
 |-  ( ph -> ( ( X +s Y ) e. No /\ ( ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <
6 5 simprd 
 |-  ( ph -> ( ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <
7 ovex 
 |-  ( X +s Y ) e. _V
8 7 snnz 
 |-  { ( X +s Y ) } =/= (/)
9 sslttr 
 |-  ( ( ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) < ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <
10 8 9 mp3an3 
 |-  ( ( ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) < ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <
11 6 10 syl 
 |-  ( ph -> ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <