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 breq2 
 |-  ( a = m -> ( Y  Y
47 rightval 
 |-  ( _Right ` Y ) = { a e. ( _Old ` ( bday ` Y ) ) | Y
48 46 47 elrab2 
 |-  ( m e. ( _Right ` Y ) <-> ( m e. ( _Old ` ( bday ` Y ) ) /\ Y
49 44 45 48 sylanbrc 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  m e. ( _Right ` Y ) )
50 eqid 
 |-  ( X +s m ) = ( X +s m )
51 oveq2 
 |-  ( h = m -> ( X +s h ) = ( X +s m ) )
52 51 rspceeqv 
 |-  ( ( m e. ( _Right ` Y ) /\ ( X +s m ) = ( X +s m ) ) -> E. h e. ( _Right ` Y ) ( X +s m ) = ( X +s h ) )
53 49 50 52 sylancl 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  E. h e. ( _Right ` Y ) ( X +s m ) = ( X +s h ) )
54 ovex 
 |-  ( X +s m ) e. _V
55 eqeq1 
 |-  ( g = ( X +s m ) -> ( g = ( X +s h ) <-> ( X +s m ) = ( X +s h ) ) )
56 55 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 ) ) )
57 54 56 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 ) )
58 53 57 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 ) } )
59 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 ) } ) )
60 58 59 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 ) } ) )
61 38 41 60 ssltsepcd 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( X +s Y )
62 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 )
63 4 adantr 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  Z e. No )
64 62 13 63 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 ) } ) <
65 64 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 ) } ) <
66 6 adantr 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( bday ` Y ) = ( bday ` Z ) )
67 16 66 eleqtrd 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( bday ` m ) e. ( bday ` Z ) )
68 bdayelon 
 |-  ( bday ` Z ) e. On
69 oldbday 
 |-  ( ( ( bday ` Z ) e. On /\ m e. No ) -> ( m e. ( _Old ` ( bday ` Z ) ) <-> ( bday ` m ) e. ( bday ` Z ) ) )
70 68 14 69 sylancr 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( m e. ( _Old ` ( bday ` Z ) ) <-> ( bday ` m ) e. ( bday ` Z ) ) )
71 67 70 mpbird 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  m e. ( _Old ` ( bday ` Z ) ) )
72 simprr3 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  m
73 breq1 
 |-  ( a = m -> ( a  m
74 leftval 
 |-  ( _Left ` Z ) = { a e. ( _Old ` ( bday ` Z ) ) | a
75 73 74 elrab2 
 |-  ( m e. ( _Left ` Z ) <-> ( m e. ( _Old ` ( bday ` Z ) ) /\ m
76 71 72 75 sylanbrc 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  m e. ( _Left ` Z ) )
77 oveq2 
 |-  ( d = m -> ( X +s d ) = ( X +s m ) )
78 77 rspceeqv 
 |-  ( ( m e. ( _Left ` Z ) /\ ( X +s m ) = ( X +s m ) ) -> E. d e. ( _Left ` Z ) ( X +s m ) = ( X +s d ) )
79 76 50 78 sylancl 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  E. d e. ( _Left ` Z ) ( X +s m ) = ( X +s d ) )
80 eqeq1 
 |-  ( c = ( X +s m ) -> ( c = ( X +s d ) <-> ( X +s m ) = ( X +s d ) ) )
81 80 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 ) ) )
82 54 81 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 ) )
83 79 82 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 ) } )
84 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 ) } ) )
85 83 84 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 ) } ) )
86 ovex 
 |-  ( X +s Z ) e. _V
87 86 snid 
 |-  ( X +s Z ) e. { ( X +s Z ) }
88 87 a1i 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( X +s Z ) e. { ( X +s Z ) } )
89 65 85 88 ssltsepcd 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( X +s m )
90 11 27 36 61 89 slttrd 
 |-  ( ( ph /\ ( m e. No /\ ( ( bday ` m ) e. ( bday ` Y ) /\ Y  ( X +s Y )
91 8 90 rexlimddv 
 |-  ( ph -> ( X +s Y )
92 3 2 addscomd 
 |-  ( ph -> ( Y +s X ) = ( X +s Y ) )
93 4 2 addscomd 
 |-  ( ph -> ( Z +s X ) = ( X +s Z ) )
94 91 92 93 3brtr4d 
 |-  ( ph -> ( Y +s X )