Metamath Proof Explorer

Theorem addsproplem5

Description: Lemma for surreal addition properties. Show the second half of the inductive hypothesis when Z is older than Y . (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
addsproplem5.6 
|- ( ph -> ( bday ` Z ) e. ( bday ` Y ) )
Assertion addsproplem5 
|- ( 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 addsproplem5.6 
 |-  ( ph -> ( bday ` Z ) e. ( bday ` Y ) )
7 1 2 3 addsproplem3 
 |-  ( ph -> ( ( X +s Y ) e. No /\ ( { e | E. f e. ( _Left ` X ) e = ( f +s Y ) } u. { g | E. h e. ( _Left ` Y ) g = ( X +s h ) } ) <
8 7 simp3d 
 |-  ( ph -> { ( X +s Y ) } <
9 ovex 
 |-  ( X +s Y ) e. _V
10 9 snid 
 |-  ( X +s Y ) e. { ( X +s Y ) }
11 10 a1i 
 |-  ( ph -> ( X +s Y ) e. { ( X +s Y ) } )
12 bdayelon 
 |-  ( bday ` Y ) e. On
13 oldbday 
 |-  ( ( ( bday ` Y ) e. On /\ Z e. No ) -> ( Z e. ( _Old ` ( bday ` Y ) ) <-> ( bday ` Z ) e. ( bday ` Y ) ) )
14 12 4 13 sylancr 
 |-  ( ph -> ( Z e. ( _Old ` ( bday ` Y ) ) <-> ( bday ` Z ) e. ( bday ` Y ) ) )
15 6 14 mpbird 
 |-  ( ph -> Z e. ( _Old ` ( bday ` Y ) ) )
16 breq2 
 |-  ( z = Z -> ( Y  Y
17 rightval 
 |-  ( _Right ` Y ) = { z e. ( _Old ` ( bday ` Y ) ) | Y
18 16 17 elrab2 
 |-  ( Z e. ( _Right ` Y ) <-> ( Z e. ( _Old ` ( bday ` Y ) ) /\ Y
19 15 5 18 sylanbrc 
 |-  ( ph -> Z e. ( _Right ` Y ) )
20 eqid 
 |-  ( X +s Z ) = ( X +s Z )
21 oveq2 
 |-  ( d = Z -> ( X +s d ) = ( X +s Z ) )
22 21 rspceeqv 
 |-  ( ( Z e. ( _Right ` Y ) /\ ( X +s Z ) = ( X +s Z ) ) -> E. d e. ( _Right ` Y ) ( X +s Z ) = ( X +s d ) )
23 19 20 22 sylancl 
 |-  ( ph -> E. d e. ( _Right ` Y ) ( X +s Z ) = ( X +s d ) )
24 ovex 
 |-  ( X +s Z ) e. _V
25 eqeq1 
 |-  ( b = ( X +s Z ) -> ( b = ( X +s d ) <-> ( X +s Z ) = ( X +s d ) ) )
26 25 rexbidv 
 |-  ( b = ( X +s Z ) -> ( E. d e. ( _Right ` Y ) b = ( X +s d ) <-> E. d e. ( _Right ` Y ) ( X +s Z ) = ( X +s d ) ) )
27 24 26 elab 
 |-  ( ( X +s Z ) e. { b | E. d e. ( _Right ` Y ) b = ( X +s d ) } <-> E. d e. ( _Right ` Y ) ( X +s Z ) = ( X +s d ) )
28 23 27 sylibr 
 |-  ( ph -> ( X +s Z ) e. { b | E. d e. ( _Right ` Y ) b = ( X +s d ) } )
29 elun2 
 |-  ( ( X +s Z ) e. { b | E. d e. ( _Right ` Y ) b = ( X +s d ) } -> ( X +s Z ) e. ( { a | E. c e. ( _Right ` X ) a = ( c +s Y ) } u. { b | E. d e. ( _Right ` Y ) b = ( X +s d ) } ) )
30 28 29 syl 
 |-  ( ph -> ( X +s Z ) e. ( { a | E. c e. ( _Right ` X ) a = ( c +s Y ) } u. { b | E. d e. ( _Right ` Y ) b = ( X +s d ) } ) )
31 8 11 30 ssltsepcd 
 |-  ( ph -> ( X +s Y )
32 3 2 addscomd 
 |-  ( ph -> ( Y +s X ) = ( X +s Y ) )
33 4 2 addscomd 
 |-  ( ph -> ( Z +s X ) = ( X +s Z ) )
34 31 32 33 3brtr4d 
 |-  ( ph -> ( Y +s X )