Metamath Proof Explorer

Theorem addscut

Description: Demonstrate the cut properties of surreal addition. This gives us closure together with a pair of set-less-than relationships for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025)

Ref Expression
Hypotheses addscut.1 
|- ( ph -> X e. No )
addscut.2 
|- ( ph -> Y e. No )
Assertion 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 ) } ) <

Proof

Step Hyp Ref Expression
1 addscut.1 
 |-  ( ph -> X e. No )
2 addscut.2 
 |-  ( ph -> Y e. No )
3 1 2 addscutlem 
 |-  ( ph -> ( ( X +s Y ) e. No /\ ( { a | E. b e. ( _Left ` X ) a = ( b +s Y ) } u. { c | E. d e. ( _Left ` Y ) c = ( X +s d ) } ) <
4 biid 
 |-  ( ( X +s Y ) e. No <-> ( X +s Y ) e. No )
5 oveq1 
 |-  ( l = b -> ( l +s Y ) = ( b +s Y ) )
6 5 eqeq2d 
 |-  ( l = b -> ( p = ( l +s Y ) <-> p = ( b +s Y ) ) )
7 6 cbvrexvw 
 |-  ( E. l e. ( _Left ` X ) p = ( l +s Y ) <-> E. b e. ( _Left ` X ) p = ( b +s Y ) )
8 eqeq1 
 |-  ( p = a -> ( p = ( b +s Y ) <-> a = ( b +s Y ) ) )
9 8 rexbidv 
 |-  ( p = a -> ( E. b e. ( _Left ` X ) p = ( b +s Y ) <-> E. b e. ( _Left ` X ) a = ( b +s Y ) ) )
10 7 9 bitrid 
 |-  ( p = a -> ( E. l e. ( _Left ` X ) p = ( l +s Y ) <-> E. b e. ( _Left ` X ) a = ( b +s Y ) ) )
11 10 cbvabv 
 |-  { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } = { a | E. b e. ( _Left ` X ) a = ( b +s Y ) }
12 oveq2 
 |-  ( m = d -> ( X +s m ) = ( X +s d ) )
13 12 eqeq2d 
 |-  ( m = d -> ( q = ( X +s m ) <-> q = ( X +s d ) ) )
14 13 cbvrexvw 
 |-  ( E. m e. ( _Left ` Y ) q = ( X +s m ) <-> E. d e. ( _Left ` Y ) q = ( X +s d ) )
15 eqeq1 
 |-  ( q = c -> ( q = ( X +s d ) <-> c = ( X +s d ) ) )
16 15 rexbidv 
 |-  ( q = c -> ( E. d e. ( _Left ` Y ) q = ( X +s d ) <-> E. d e. ( _Left ` Y ) c = ( X +s d ) ) )
17 14 16 bitrid 
 |-  ( q = c -> ( E. m e. ( _Left ` Y ) q = ( X +s m ) <-> E. d e. ( _Left ` Y ) c = ( X +s d ) ) )
18 17 cbvabv 
 |-  { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } = { c | E. d e. ( _Left ` Y ) c = ( X +s d ) }
19 11 18 uneq12i 
 |-  ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) = ( { a | E. b e. ( _Left ` X ) a = ( b +s Y ) } u. { c | E. d e. ( _Left ` Y ) c = ( X +s d ) } )
20 19 breq1i 
 |-  ( ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) < ( { a | E. b e. ( _Left ` X ) a = ( b +s Y ) } u. { c | E. d e. ( _Left ` Y ) c = ( X +s d ) } ) <
21 oveq1 
 |-  ( r = f -> ( r +s Y ) = ( f +s Y ) )
22 21 eqeq2d 
 |-  ( r = f -> ( w = ( r +s Y ) <-> w = ( f +s Y ) ) )
23 22 cbvrexvw 
 |-  ( E. r e. ( _Right ` X ) w = ( r +s Y ) <-> E. f e. ( _Right ` X ) w = ( f +s Y ) )
24 eqeq1 
 |-  ( w = e -> ( w = ( f +s Y ) <-> e = ( f +s Y ) ) )
25 24 rexbidv 
 |-  ( w = e -> ( E. f e. ( _Right ` X ) w = ( f +s Y ) <-> E. f e. ( _Right ` X ) e = ( f +s Y ) ) )
26 23 25 bitrid 
 |-  ( w = e -> ( E. r e. ( _Right ` X ) w = ( r +s Y ) <-> E. f e. ( _Right ` X ) e = ( f +s Y ) ) )
27 26 cbvabv 
 |-  { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } = { e | E. f e. ( _Right ` X ) e = ( f +s Y ) }
28 oveq2 
 |-  ( s = h -> ( X +s s ) = ( X +s h ) )
29 28 eqeq2d 
 |-  ( s = h -> ( t = ( X +s s ) <-> t = ( X +s h ) ) )
30 29 cbvrexvw 
 |-  ( E. s e. ( _Right ` Y ) t = ( X +s s ) <-> E. h e. ( _Right ` Y ) t = ( X +s h ) )
31 eqeq1 
 |-  ( t = g -> ( t = ( X +s h ) <-> g = ( X +s h ) ) )
32 31 rexbidv 
 |-  ( t = g -> ( E. h e. ( _Right ` Y ) t = ( X +s h ) <-> E. h e. ( _Right ` Y ) g = ( X +s h ) ) )
33 30 32 bitrid 
 |-  ( t = g -> ( E. s e. ( _Right ` Y ) t = ( X +s s ) <-> E. h e. ( _Right ` Y ) g = ( X +s h ) ) )
34 33 cbvabv 
 |-  { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } = { g | E. h e. ( _Right ` Y ) g = ( X +s h ) }
35 27 34 uneq12i 
 |-  ( { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) = ( { e | E. f e. ( _Right ` X ) e = ( f +s Y ) } u. { g | E. h e. ( _Right ` Y ) g = ( X +s h ) } )
36 35 breq2i 
 |-  ( { ( X +s Y ) } < { ( X +s Y ) } <
37 4 20 36 3anbi123i 
 |-  ( ( ( 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 /\ ( { a | E. b e. ( _Left ` X ) a = ( b +s Y ) } u. { c | E. d e. ( _Left ` Y ) c = ( X +s d ) } ) <
38 3 37 sylibr 
 |-  ( 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 ) } ) <