Metamath Proof Explorer

Theorem addsproplem6

Description: Lemma for surreal addition properties. Finally, we show the second half of the induction hypothesis when Y and Z are the same age. (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
addsproplem6.6 
|- ( ph -> ( bday ` Y ) = ( bday ` Z ) )
Assertion addsproplem6 
|- ( 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 addsproplem6.6 
 |-  ( ph -> ( bday ` Y ) = ( bday ` Z ) )
7 nodense 
 |-  ( ( ( Y e. No /\ Z e. No ) /\ ( ( bday ` Y ) = ( bday ` Z ) /\ Y  E. m e. No ( ( bday ` m ) e. ( bday ` Y ) /\ Y
8 3 4 6 5 7 syl22anc 
 |-  ( ph -> E. m e. No ( ( bday ` m ) e. ( bday ` Y ) /\ Y
9 1 2 3 addsproplem3 
 |-  ( 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 ) } ) <
10 9 simp1d 
 |-  ( ph -> ( X +s Y ) e. No )
11 10 adantr 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( X +s Y ) e. No )
12 1 adantr 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  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 )
13 2 adantr 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  X e. No )
14 simprl 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  m e. No )
15 unidm 
 |-  ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` m ) ) ) = ( ( bday ` X ) +no ( bday ` m ) )
16 simprr1 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( bday ` m ) e. ( bday ` Y ) )
17 bdayelon 
 |-  ( bday ` m ) e. On
18 bdayelon 
 |-  ( bday ` Y ) e. On
19 bdayelon 
 |-  ( bday ` X ) e. On
20 naddel2 
 |-  ( ( ( bday ` m ) e. On /\ ( bday ` Y ) e. On /\ ( bday ` X ) e. On ) -> ( ( bday ` m ) e. ( bday ` Y ) <-> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) )
21 17 18 19 20 mp3an 
 |-  ( ( bday ` m ) e. ( bday ` Y ) <-> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
22 16 21 sylib 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
23 elun1 
 |-  ( ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
24 22 23 syl 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
25 15 24 eqeltrid 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` m ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
26 12 13 14 14 25 addsproplem1 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( ( X +s m ) e. No /\ ( m  ( m +s X )
27 26 simpld 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( X +s m ) e. No )
28 uncom 
 |-  ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) = ( ( ( bday ` X ) +no ( bday ` Z ) ) u. ( ( bday ` X ) +no ( bday ` Y ) ) )
29 28 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 ) ) ) )
30 29 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 )
31 30 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 )
32 31 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 )
33 1 32 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 )
34 33 2 4 addsproplem3 
 |-  ( ph -> ( ( X +s Z ) e. No /\ ( { a | E. b e. ( _Left ` X ) a = ( b +s Z ) } u. { c | E. d e. ( _Left ` Z ) c = ( X +s d ) } ) <
35 34 simp1d 
 |-  ( ph -> ( X +s Z ) e. No )
36 35 adantr 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( X +s Z ) e. No )
37 9 simp3d 
 |-  ( ph -> { ( X +s Y ) } <
38 37 adantr 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  { ( X +s Y ) } <
39 ovex 
 |-  ( X +s Y ) e. _V
40 39 snid 
 |-  ( X +s Y ) e. { ( X +s Y ) }
41 40 a1i 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( X +s Y ) e. { ( X +s Y ) } )
42 oldbday 
 |-  ( ( ( bday ` Y ) e. On /\ m e. No ) -> ( m e. ( _Old ` ( bday ` Y ) ) <-> ( bday ` m ) e. ( bday ` Y ) ) )
43 18 14 42 sylancr 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( m e. ( _Old ` ( bday ` Y ) ) <-> ( bday ` m ) e. ( bday ` Y ) ) )
44 16 43 mpbird 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  m e. ( _Old ` ( bday ` Y ) ) )
45 simprr2 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  Y
46 elright 
 |-  ( m e. ( _Right ` Y ) <-> ( m e. ( _Old ` ( bday ` Y ) ) /\ Y
47 44 45 46 sylanbrc 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  m e. ( _Right ` Y ) )
48 eqid 
 |-  ( X +s m ) = ( X +s m )
49 oveq2 
 |-  ( h = m -> ( X +s h ) = ( X +s m ) )
50 49 rspceeqv 
 |-  ( ( m e. ( _Right ` Y ) /\ ( X +s m ) = ( X +s m ) ) -> E. h e. ( _Right ` Y ) ( X +s m ) = ( X +s h ) )
51 47 48 50 sylancl 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  E. h e. ( _Right ` Y ) ( X +s m ) = ( X +s h ) )
52 ovex 
 |-  ( X +s m ) e. _V
53 eqeq1 
 |-  ( g = ( X +s m ) -> ( g = ( X +s h ) <-> ( X +s m ) = ( X +s h ) ) )
54 53 rexbidv 
 |-  ( g = ( X +s m ) -> ( E. h e. ( _Right ` Y ) g = ( X +s h ) <-> E. h e. ( _Right ` Y ) ( X +s m ) = ( X +s h ) ) )
55 52 54 elab 
 |-  ( ( X +s m ) e. { g | E. h e. ( _Right ` Y ) g = ( X +s h ) } <-> E. h e. ( _Right ` Y ) ( X +s m ) = ( X +s h ) )
56 51 55 sylibr 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( X +s m ) e. { g | E. h e. ( _Right ` Y ) g = ( X +s h ) } )
57 elun2 
 |-  ( ( X +s m ) e. { g | E. h e. ( _Right ` Y ) g = ( X +s h ) } -> ( X +s m ) e. ( { e | E. f e. ( _Right ` X ) e = ( f +s Y ) } u. { g | E. h e. ( _Right ` Y ) g = ( X +s h ) } ) )
58 56 57 syl 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( X +s m ) e. ( { e | E. f e. ( _Right ` X ) e = ( f +s Y ) } u. { g | E. h e. ( _Right ` Y ) g = ( X +s h ) } ) )
59 38 41 58 ssltsepcd 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( X +s Y )
60 33 adantr 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  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 )
61 4 adantr 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  Z e. No )
62 60 13 61 addsproplem3 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( ( X +s Z ) e. No /\ ( { a | E. b e. ( _Left ` X ) a = ( b +s Z ) } u. { c | E. d e. ( _Left ` Z ) c = ( X +s d ) } ) <
63 62 simp2d 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( { a | E. b e. ( _Left ` X ) a = ( b +s Z ) } u. { c | E. d e. ( _Left ` Z ) c = ( X +s d ) } ) <
64 6 adantr 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( bday ` Y ) = ( bday ` Z ) )
65 16 64 eleqtrd 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( bday ` m ) e. ( bday ` Z ) )
66 bdayelon 
 |-  ( bday ` Z ) e. On
67 oldbday 
 |-  ( ( ( bday ` Z ) e. On /\ m e. No ) -> ( m e. ( _Old ` ( bday ` Z ) ) <-> ( bday ` m ) e. ( bday ` Z ) ) )
68 66 14 67 sylancr 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( m e. ( _Old ` ( bday ` Z ) ) <-> ( bday ` m ) e. ( bday ` Z ) ) )
69 65 68 mpbird 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  m e. ( _Old ` ( bday ` Z ) ) )
70 simprr3 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  m
71 elleft 
 |-  ( m e. ( _Left ` Z ) <-> ( m e. ( _Old ` ( bday ` Z ) ) /\ m
72 69 70 71 sylanbrc 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  m e. ( _Left ` Z ) )
73 oveq2 
 |-  ( d = m -> ( X +s d ) = ( X +s m ) )
74 73 rspceeqv 
 |-  ( ( m e. ( _Left ` Z ) /\ ( X +s m ) = ( X +s m ) ) -> E. d e. ( _Left ` Z ) ( X +s m ) = ( X +s d ) )
75 72 48 74 sylancl 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  E. d e. ( _Left ` Z ) ( X +s m ) = ( X +s d ) )
76 eqeq1 
 |-  ( c = ( X +s m ) -> ( c = ( X +s d ) <-> ( X +s m ) = ( X +s d ) ) )
77 76 rexbidv 
 |-  ( c = ( X +s m ) -> ( E. d e. ( _Left ` Z ) c = ( X +s d ) <-> E. d e. ( _Left ` Z ) ( X +s m ) = ( X +s d ) ) )
78 52 77 elab 
 |-  ( ( X +s m ) e. { c | E. d e. ( _Left ` Z ) c = ( X +s d ) } <-> E. d e. ( _Left ` Z ) ( X +s m ) = ( X +s d ) )
79 75 78 sylibr 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( X +s m ) e. { c | E. d e. ( _Left ` Z ) c = ( X +s d ) } )
80 elun2 
 |-  ( ( X +s m ) e. { c | E. d e. ( _Left ` Z ) c = ( X +s d ) } -> ( X +s m ) e. ( { a | E. b e. ( _Left ` X ) a = ( b +s Z ) } u. { c | E. d e. ( _Left ` Z ) c = ( X +s d ) } ) )
81 79 80 syl 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( X +s m ) e. ( { a | E. b e. ( _Left ` X ) a = ( b +s Z ) } u. { c | E. d e. ( _Left ` Z ) c = ( X +s d ) } ) )
82 ovex 
 |-  ( X +s Z ) e. _V
83 82 snid 
 |-  ( X +s Z ) e. { ( X +s Z ) }
84 83 a1i 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( X +s Z ) e. { ( X +s Z ) } )
85 63 81 84 ssltsepcd 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( X +s m )
86 11 27 36 59 85 slttrd 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( X +s Y )
87 8 86 rexlimddv 
 |-  ( ph -> ( X +s Y )
88 3 2 addscomd 
 |-  ( ph -> ( Y +s X ) = ( X +s Y ) )
89 4 2 addscomd 
 |-  ( ph -> ( Z +s X ) = ( X +s Z ) )
90 87 88 89 3brtr4d 
 |-  ( ph -> ( Y +s X )