Metamath Proof Explorer

Theorem addsproplem4

Description: Lemma for surreal addition properties. Show the second half of the inductive hypothesis when Y is older than Z . (Contributed by Scott Fenton, 21-Jan-2025)

Ref Expression
Hypotheses addsproplem.1 
|- ( ph -> A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )
addspropord.2 
|- ( ph -> X e. No )
addspropord.3 
|- ( ph -> Y e. No )
addspropord.4 
|- ( ph -> Z e. No )
addspropord.5 
|- ( ph -> Y
addsproplem4.6 
|- ( ph -> ( bday ` Y ) e. ( bday ` Z ) )
Assertion addsproplem4 
|- ( ph -> ( Y +s X )

Proof

Step Hyp Ref Expression
1 addsproplem.1 
 |-  ( ph -> A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )
2 addspropord.2 
 |-  ( ph -> X e. No )
3 addspropord.3 
 |-  ( ph -> Y e. No )
4 addspropord.4 
 |-  ( ph -> Z e. No )
5 addspropord.5 
 |-  ( ph -> Y
6 addsproplem4.6 
 |-  ( ph -> ( bday ` Y ) e. ( bday ` Z ) )
7 uncom 
 |-  ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) = ( ( ( bday ` X ) +no ( bday ` Z ) ) u. ( ( bday ` X ) +no ( bday ` Y ) ) )
8 7 eleq2i 
 |-  ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) <-> ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Z ) ) u. ( ( bday ` X ) +no ( bday ` Y ) ) ) )
9 8 imbi1i 
 |-  ( ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )  ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Z ) ) u. ( ( bday ` X ) +no ( bday ` Y ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )
10 9 ralbii 
 |-  ( A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )  A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Z ) ) u. ( ( bday ` X ) +no ( bday ` Y ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )
11 10 2ralbii 
 |-  ( A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )  A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Z ) ) u. ( ( bday ` X ) +no ( bday ` Y ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )
12 1 11 sylib 
 |-  ( ph -> A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Z ) ) u. ( ( bday ` X ) +no ( bday ` Y ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )
13 12 2 4 addsproplem3 
 |-  ( ph -> ( ( X +s Z ) e. No /\ ( { a | E. c e. ( _Left ` X ) a = ( c +s Z ) } u. { b | E. d e. ( _Left ` Z ) b = ( X +s d ) } ) <
14 13 simp2d 
 |-  ( ph -> ( { a | E. c e. ( _Left ` X ) a = ( c +s Z ) } u. { b | E. d e. ( _Left ` Z ) b = ( X +s d ) } ) <
15 bdayelon 
 |-  ( bday ` Z ) e. On
16 oldbday 
 |-  ( ( ( bday ` Z ) e. On /\ Y e. No ) -> ( Y e. ( _Old ` ( bday ` Z ) ) <-> ( bday ` Y ) e. ( bday ` Z ) ) )
17 15 3 16 sylancr 
 |-  ( ph -> ( Y e. ( _Old ` ( bday ` Z ) ) <-> ( bday ` Y ) e. ( bday ` Z ) ) )
18 6 17 mpbird 
 |-  ( ph -> Y e. ( _Old ` ( bday ` Z ) ) )
19 breq1 
 |-  ( y = Y -> ( y  Y
20 leftval 
 |-  ( _Left ` Z ) = { y e. ( _Old ` ( bday ` Z ) ) | y
21 19 20 elrab2 
 |-  ( Y e. ( _Left ` Z ) <-> ( Y e. ( _Old ` ( bday ` Z ) ) /\ Y
22 18 5 21 sylanbrc 
 |-  ( ph -> Y e. ( _Left ` Z ) )
23 eqid 
 |-  ( X +s Y ) = ( X +s Y )
24 oveq2 
 |-  ( d = Y -> ( X +s d ) = ( X +s Y ) )
25 24 rspceeqv 
 |-  ( ( Y e. ( _Left ` Z ) /\ ( X +s Y ) = ( X +s Y ) ) -> E. d e. ( _Left ` Z ) ( X +s Y ) = ( X +s d ) )
26 22 23 25 sylancl 
 |-  ( ph -> E. d e. ( _Left ` Z ) ( X +s Y ) = ( X +s d ) )
27 ovex 
 |-  ( X +s Y ) e. _V
28 eqeq1 
 |-  ( b = ( X +s Y ) -> ( b = ( X +s d ) <-> ( X +s Y ) = ( X +s d ) ) )
29 28 rexbidv 
 |-  ( b = ( X +s Y ) -> ( E. d e. ( _Left ` Z ) b = ( X +s d ) <-> E. d e. ( _Left ` Z ) ( X +s Y ) = ( X +s d ) ) )
30 27 29 elab 
 |-  ( ( X +s Y ) e. { b | E. d e. ( _Left ` Z ) b = ( X +s d ) } <-> E. d e. ( _Left ` Z ) ( X +s Y ) = ( X +s d ) )
31 26 30 sylibr 
 |-  ( ph -> ( X +s Y ) e. { b | E. d e. ( _Left ` Z ) b = ( X +s d ) } )
32 elun2 
 |-  ( ( X +s Y ) e. { b | E. d e. ( _Left ` Z ) b = ( X +s d ) } -> ( X +s Y ) e. ( { a | E. c e. ( _Left ` X ) a = ( c +s Z ) } u. { b | E. d e. ( _Left ` Z ) b = ( X +s d ) } ) )
33 31 32 syl 
 |-  ( ph -> ( X +s Y ) e. ( { a | E. c e. ( _Left ` X ) a = ( c +s Z ) } u. { b | E. d e. ( _Left ` Z ) b = ( X +s d ) } ) )
34 ovex 
 |-  ( X +s Z ) e. _V
35 34 snid 
 |-  ( X +s Z ) e. { ( X +s Z ) }
36 35 a1i 
 |-  ( ph -> ( X +s Z ) e. { ( X +s Z ) } )
37 14 33 36 ssltsepcd 
 |-  ( ph -> ( X +s Y )
38 3 2 addscomd 
 |-  ( ph -> ( Y +s X ) = ( X +s Y ) )
39 4 2 addscomd 
 |-  ( ph -> ( Z +s X ) = ( X +s Z ) )
40 37 38 39 3brtr4d 
 |-  ( ph -> ( Y +s X )