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 elleft 
 |-  ( Y e. ( _Left ` Z ) <-> ( Y e. ( _Old ` ( bday ` Z ) ) /\ Y
20 18 5 19 sylanbrc 
 |-  ( ph -> Y e. ( _Left ` Z ) )
21 eqid 
 |-  ( X +s Y ) = ( X +s Y )
22 oveq2 
 |-  ( d = Y -> ( X +s d ) = ( X +s Y ) )
23 22 rspceeqv 
 |-  ( ( Y e. ( _Left ` Z ) /\ ( X +s Y ) = ( X +s Y ) ) -> E. d e. ( _Left ` Z ) ( X +s Y ) = ( X +s d ) )
24 20 21 23 sylancl 
 |-  ( ph -> E. d e. ( _Left ` Z ) ( X +s Y ) = ( X +s d ) )
25 ovex 
 |-  ( X +s Y ) e. _V
26 eqeq1 
 |-  ( b = ( X +s Y ) -> ( b = ( X +s d ) <-> ( X +s Y ) = ( X +s d ) ) )
27 26 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 ) ) )
28 25 27 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 ) )
29 24 28 sylibr 
 |-  ( ph -> ( X +s Y ) e. { b | E. d e. ( _Left ` Z ) b = ( X +s d ) } )
30 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 ) } ) )
31 29 30 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 ) } ) )
32 ovex 
 |-  ( X +s Z ) e. _V
33 32 snid 
 |-  ( X +s Z ) e. { ( X +s Z ) }
34 33 a1i 
 |-  ( ph -> ( X +s Z ) e. { ( X +s Z ) } )
35 14 31 34 ssltsepcd 
 |-  ( ph -> ( X +s Y )
36 3 2 addscomd 
 |-  ( ph -> ( Y +s X ) = ( X +s Y ) )
37 4 2 addscomd 
 |-  ( ph -> ( Z +s X ) = ( X +s Z ) )
38 35 36 37 3brtr4d 
 |-  ( ph -> ( Y +s X )