Metamath Proof Explorer

Theorem addsproplem2

Description: Lemma for surreal addition properties. When proving closure for operations defined using norec and norec2 , it is a strictly stronger statement to say that the cut defined is actually a cut than it is to say that the operation is closed. We will often prove this stronger statement. Here, we do so for the cut involved in surreal addition. (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 )
addsproplem2.2 
|- ( ph -> X e. No )
addsproplem2.3 
|- ( ph -> Y e. No )
Assertion addsproplem2 
|- ( ph -> ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <

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 addsproplem2.2 
 |-  ( ph -> X e. No )
3 addsproplem2.3 
 |-  ( ph -> Y e. No )
4 fvex 
 |-  ( _Left ` X ) e. _V
5 4 abrexex 
 |-  { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } e. _V
6 5 a1i 
 |-  ( ph -> { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } e. _V )
7 fvex 
 |-  ( _Left ` Y ) e. _V
8 7 abrexex 
 |-  { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } e. _V
9 8 a1i 
 |-  ( ph -> { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } e. _V )
10 6 9 unexd 
 |-  ( ph -> ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) e. _V )
11 fvex 
 |-  ( _Right ` X ) e. _V
12 11 abrexex 
 |-  { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } e. _V
13 12 a1i 
 |-  ( ph -> { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } e. _V )
14 fvex 
 |-  ( _Right ` Y ) e. _V
15 14 abrexex 
 |-  { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } e. _V
16 15 a1i 
 |-  ( ph -> { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } e. _V )
17 13 16 unexd 
 |-  ( ph -> ( { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) e. _V )
18 1 adantr 
 |-  ( ( ph /\ l e. ( _Left ` 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 ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )
19 leftno 
 |-  ( l e. ( _Left ` X ) -> l e. No )
20 19 adantl 
 |-  ( ( ph /\ l e. ( _Left ` X ) ) -> l e. No )
21 3 adantr 
 |-  ( ( ph /\ l e. ( _Left ` X ) ) -> Y e. No )
22 0no 
 |-  0s e. No
23 22 a1i 
 |-  ( ( ph /\ l e. ( _Left ` X ) ) -> 0s e. No )
24 bday0 
 |-  ( bday ` 0s ) = (/)
25 24 oveq2i 
 |-  ( ( bday ` l ) +no ( bday ` 0s ) ) = ( ( bday ` l ) +no (/) )
26 bdayon 
 |-  ( bday ` l ) e. On
27 naddrid 
 |-  ( ( bday ` l ) e. On -> ( ( bday ` l ) +no (/) ) = ( bday ` l ) )
28 26 27 ax-mp 
 |-  ( ( bday ` l ) +no (/) ) = ( bday ` l )
29 25 28 eqtri 
 |-  ( ( bday ` l ) +no ( bday ` 0s ) ) = ( bday ` l )
30 29 uneq2i 
 |-  ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( ( bday ` l ) +no ( bday ` 0s ) ) ) = ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( bday ` l ) )
31 bdayon 
 |-  ( bday ` Y ) e. On
32 naddword1 
 |-  ( ( ( bday ` l ) e. On /\ ( bday ` Y ) e. On ) -> ( bday ` l ) C_ ( ( bday ` l ) +no ( bday ` Y ) ) )
33 26 31 32 mp2an 
 |-  ( bday ` l ) C_ ( ( bday ` l ) +no ( bday ` Y ) )
34 ssequn2 
 |-  ( ( bday ` l ) C_ ( ( bday ` l ) +no ( bday ` Y ) ) <-> ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( bday ` l ) ) = ( ( bday ` l ) +no ( bday ` Y ) ) )
35 33 34 mpbi 
 |-  ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( bday ` l ) ) = ( ( bday ` l ) +no ( bday ` Y ) )
36 30 35 eqtri 
 |-  ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( ( bday ` l ) +no ( bday ` 0s ) ) ) = ( ( bday ` l ) +no ( bday ` Y ) )
37 leftold 
 |-  ( l e. ( _Left ` X ) -> l e. ( _Old ` ( bday ` X ) ) )
38 bdayon 
 |-  ( bday ` X ) e. On
39 oldbday 
 |-  ( ( ( bday ` X ) e. On /\ l e. No ) -> ( l e. ( _Old ` ( bday ` X ) ) <-> ( bday ` l ) e. ( bday ` X ) ) )
40 38 19 39 sylancr 
 |-  ( l e. ( _Left ` X ) -> ( l e. ( _Old ` ( bday ` X ) ) <-> ( bday ` l ) e. ( bday ` X ) ) )
41 37 40 mpbid 
 |-  ( l e. ( _Left ` X ) -> ( bday ` l ) e. ( bday ` X ) )
42 naddel1 
 |-  ( ( ( bday ` l ) e. On /\ ( bday ` X ) e. On /\ ( bday ` Y ) e. On ) -> ( ( bday ` l ) e. ( bday ` X ) <-> ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) )
43 26 38 31 42 mp3an 
 |-  ( ( bday ` l ) e. ( bday ` X ) <-> ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
44 41 43 sylib 
 |-  ( l e. ( _Left ` X ) -> ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
45 44 adantl 
 |-  ( ( ph /\ l e. ( _Left ` X ) ) -> ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
46 elun1 
 |-  ( ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
47 45 46 syl 
 |-  ( ( ph /\ l e. ( _Left ` X ) ) -> ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
48 36 47 eqeltrid 
 |-  ( ( ph /\ l e. ( _Left ` X ) ) -> ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( ( bday ` l ) +no ( bday ` 0s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
49 18 20 21 23 48 addsproplem1 
 |-  ( ( ph /\ l e. ( _Left ` X ) ) -> ( ( l +s Y ) e. No /\ ( Y  ( Y +s l )
50 49 simpld 
 |-  ( ( ph /\ l e. ( _Left ` X ) ) -> ( l +s Y ) e. No )
51 eleq1a 
 |-  ( ( l +s Y ) e. No -> ( p = ( l +s Y ) -> p e. No ) )
52 50 51 syl 
 |-  ( ( ph /\ l e. ( _Left ` X ) ) -> ( p = ( l +s Y ) -> p e. No ) )
53 52 rexlimdva 
 |-  ( ph -> ( E. l e. ( _Left ` X ) p = ( l +s Y ) -> p e. No ) )
54 53 abssdv 
 |-  ( ph -> { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } C_ No )
55 1 adantr 
 |-  ( ( ph /\ m e. ( _Left ` 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 )
56 2 adantr 
 |-  ( ( ph /\ m e. ( _Left ` Y ) ) -> X e. No )
57 leftno 
 |-  ( m e. ( _Left ` Y ) -> m e. No )
58 57 adantl 
 |-  ( ( ph /\ m e. ( _Left ` Y ) ) -> m e. No )
59 22 a1i 
 |-  ( ( ph /\ m e. ( _Left ` Y ) ) -> 0s e. No )
60 24 oveq2i 
 |-  ( ( bday ` X ) +no ( bday ` 0s ) ) = ( ( bday ` X ) +no (/) )
61 naddrid 
 |-  ( ( bday ` X ) e. On -> ( ( bday ` X ) +no (/) ) = ( bday ` X ) )
62 38 61 ax-mp 
 |-  ( ( bday ` X ) +no (/) ) = ( bday ` X )
63 60 62 eqtri 
 |-  ( ( bday ` X ) +no ( bday ` 0s ) ) = ( bday ` X )
64 63 uneq2i 
 |-  ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` 0s ) ) ) = ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( bday ` X ) )
65 bdayon 
 |-  ( bday ` m ) e. On
66 naddword1 
 |-  ( ( ( bday ` X ) e. On /\ ( bday ` m ) e. On ) -> ( bday ` X ) C_ ( ( bday ` X ) +no ( bday ` m ) ) )
67 38 65 66 mp2an 
 |-  ( bday ` X ) C_ ( ( bday ` X ) +no ( bday ` m ) )
68 ssequn2 
 |-  ( ( bday ` X ) C_ ( ( bday ` X ) +no ( bday ` m ) ) <-> ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( bday ` X ) ) = ( ( bday ` X ) +no ( bday ` m ) ) )
69 67 68 mpbi 
 |-  ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( bday ` X ) ) = ( ( bday ` X ) +no ( bday ` m ) )
70 64 69 eqtri 
 |-  ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` 0s ) ) ) = ( ( bday ` X ) +no ( bday ` m ) )
71 leftold 
 |-  ( m e. ( _Left ` Y ) -> m e. ( _Old ` ( bday ` Y ) ) )
72 oldbday 
 |-  ( ( ( bday ` Y ) e. On /\ m e. No ) -> ( m e. ( _Old ` ( bday ` Y ) ) <-> ( bday ` m ) e. ( bday ` Y ) ) )
73 31 57 72 sylancr 
 |-  ( m e. ( _Left ` Y ) -> ( m e. ( _Old ` ( bday ` Y ) ) <-> ( bday ` m ) e. ( bday ` Y ) ) )
74 71 73 mpbid 
 |-  ( m e. ( _Left ` Y ) -> ( bday ` m ) e. ( bday ` Y ) )
75 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 ) ) ) )
76 65 31 38 75 mp3an 
 |-  ( ( bday ` m ) e. ( bday ` Y ) <-> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
77 74 76 sylib 
 |-  ( m e. ( _Left ` Y ) -> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
78 77 adantl 
 |-  ( ( ph /\ m e. ( _Left ` Y ) ) -> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
79 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 ) ) ) )
80 78 79 syl 
 |-  ( ( ph /\ m e. ( _Left ` Y ) ) -> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
81 70 80 eqeltrid 
 |-  ( ( ph /\ m e. ( _Left ` Y ) ) -> ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` 0s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
82 55 56 58 59 81 addsproplem1 
 |-  ( ( ph /\ m e. ( _Left ` Y ) ) -> ( ( X +s m ) e. No /\ ( m  ( m +s X )
83 82 simpld 
 |-  ( ( ph /\ m e. ( _Left ` Y ) ) -> ( X +s m ) e. No )
84 eleq1a 
 |-  ( ( X +s m ) e. No -> ( q = ( X +s m ) -> q e. No ) )
85 83 84 syl 
 |-  ( ( ph /\ m e. ( _Left ` Y ) ) -> ( q = ( X +s m ) -> q e. No ) )
86 85 rexlimdva 
 |-  ( ph -> ( E. m e. ( _Left ` Y ) q = ( X +s m ) -> q e. No ) )
87 86 abssdv 
 |-  ( ph -> { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } C_ No )
88 54 87 unssd 
 |-  ( ph -> ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) C_ No )
89 1 adantr 
 |-  ( ( ph /\ r e. ( _Right ` 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 ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )
90 rightno 
 |-  ( r e. ( _Right ` X ) -> r e. No )
91 90 adantl 
 |-  ( ( ph /\ r e. ( _Right ` X ) ) -> r e. No )
92 3 adantr 
 |-  ( ( ph /\ r e. ( _Right ` X ) ) -> Y e. No )
93 22 a1i 
 |-  ( ( ph /\ r e. ( _Right ` X ) ) -> 0s e. No )
94 24 oveq2i 
 |-  ( ( bday ` r ) +no ( bday ` 0s ) ) = ( ( bday ` r ) +no (/) )
95 bdayon 
 |-  ( bday ` r ) e. On
96 naddrid 
 |-  ( ( bday ` r ) e. On -> ( ( bday ` r ) +no (/) ) = ( bday ` r ) )
97 95 96 ax-mp 
 |-  ( ( bday ` r ) +no (/) ) = ( bday ` r )
98 94 97 eqtri 
 |-  ( ( bday ` r ) +no ( bday ` 0s ) ) = ( bday ` r )
99 98 uneq2i 
 |-  ( ( ( bday ` r ) +no ( bday ` Y ) ) u. ( ( bday ` r ) +no ( bday ` 0s ) ) ) = ( ( ( bday ` r ) +no ( bday ` Y ) ) u. ( bday ` r ) )
100 naddword1 
 |-  ( ( ( bday ` r ) e. On /\ ( bday ` Y ) e. On ) -> ( bday ` r ) C_ ( ( bday ` r ) +no ( bday ` Y ) ) )
101 95 31 100 mp2an 
 |-  ( bday ` r ) C_ ( ( bday ` r ) +no ( bday ` Y ) )
102 ssequn2 
 |-  ( ( bday ` r ) C_ ( ( bday ` r ) +no ( bday ` Y ) ) <-> ( ( ( bday ` r ) +no ( bday ` Y ) ) u. ( bday ` r ) ) = ( ( bday ` r ) +no ( bday ` Y ) ) )
103 101 102 mpbi 
 |-  ( ( ( bday ` r ) +no ( bday ` Y ) ) u. ( bday ` r ) ) = ( ( bday ` r ) +no ( bday ` Y ) )
104 99 103 eqtri 
 |-  ( ( ( bday ` r ) +no ( bday ` Y ) ) u. ( ( bday ` r ) +no ( bday ` 0s ) ) ) = ( ( bday ` r ) +no ( bday ` Y ) )
105 rightold 
 |-  ( r e. ( _Right ` X ) -> r e. ( _Old ` ( bday ` X ) ) )
106 oldbday 
 |-  ( ( ( bday ` X ) e. On /\ r e. No ) -> ( r e. ( _Old ` ( bday ` X ) ) <-> ( bday ` r ) e. ( bday ` X ) ) )
107 38 90 106 sylancr 
 |-  ( r e. ( _Right ` X ) -> ( r e. ( _Old ` ( bday ` X ) ) <-> ( bday ` r ) e. ( bday ` X ) ) )
108 105 107 mpbid 
 |-  ( r e. ( _Right ` X ) -> ( bday ` r ) e. ( bday ` X ) )
109 naddel1 
 |-  ( ( ( bday ` r ) e. On /\ ( bday ` X ) e. On /\ ( bday ` Y ) e. On ) -> ( ( bday ` r ) e. ( bday ` X ) <-> ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) )
110 95 38 31 109 mp3an 
 |-  ( ( bday ` r ) e. ( bday ` X ) <-> ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
111 108 110 sylib 
 |-  ( r e. ( _Right ` X ) -> ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
112 111 adantl 
 |-  ( ( ph /\ r e. ( _Right ` X ) ) -> ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
113 elun1 
 |-  ( ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
114 112 113 syl 
 |-  ( ( ph /\ r e. ( _Right ` X ) ) -> ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
115 104 114 eqeltrid 
 |-  ( ( ph /\ r e. ( _Right ` X ) ) -> ( ( ( bday ` r ) +no ( bday ` Y ) ) u. ( ( bday ` r ) +no ( bday ` 0s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
116 89 91 92 93 115 addsproplem1 
 |-  ( ( ph /\ r e. ( _Right ` X ) ) -> ( ( r +s Y ) e. No /\ ( Y  ( Y +s r )
117 116 simpld 
 |-  ( ( ph /\ r e. ( _Right ` X ) ) -> ( r +s Y ) e. No )
118 eleq1a 
 |-  ( ( r +s Y ) e. No -> ( w = ( r +s Y ) -> w e. No ) )
119 117 118 syl 
 |-  ( ( ph /\ r e. ( _Right ` X ) ) -> ( w = ( r +s Y ) -> w e. No ) )
120 119 rexlimdva 
 |-  ( ph -> ( E. r e. ( _Right ` X ) w = ( r +s Y ) -> w e. No ) )
121 120 abssdv 
 |-  ( ph -> { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } C_ No )
122 1 adantr 
 |-  ( ( ph /\ s e. ( _Right ` 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 )
123 2 adantr 
 |-  ( ( ph /\ s e. ( _Right ` Y ) ) -> X e. No )
124 rightno 
 |-  ( s e. ( _Right ` Y ) -> s e. No )
125 124 adantl 
 |-  ( ( ph /\ s e. ( _Right ` Y ) ) -> s e. No )
126 22 a1i 
 |-  ( ( ph /\ s e. ( _Right ` Y ) ) -> 0s e. No )
127 63 uneq2i 
 |-  ( ( ( bday ` X ) +no ( bday ` s ) ) u. ( ( bday ` X ) +no ( bday ` 0s ) ) ) = ( ( ( bday ` X ) +no ( bday ` s ) ) u. ( bday ` X ) )
128 bdayon 
 |-  ( bday ` s ) e. On
129 naddword1 
 |-  ( ( ( bday ` X ) e. On /\ ( bday ` s ) e. On ) -> ( bday ` X ) C_ ( ( bday ` X ) +no ( bday ` s ) ) )
130 38 128 129 mp2an 
 |-  ( bday ` X ) C_ ( ( bday ` X ) +no ( bday ` s ) )
131 ssequn2 
 |-  ( ( bday ` X ) C_ ( ( bday ` X ) +no ( bday ` s ) ) <-> ( ( ( bday ` X ) +no ( bday ` s ) ) u. ( bday ` X ) ) = ( ( bday ` X ) +no ( bday ` s ) ) )
132 130 131 mpbi 
 |-  ( ( ( bday ` X ) +no ( bday ` s ) ) u. ( bday ` X ) ) = ( ( bday ` X ) +no ( bday ` s ) )
133 127 132 eqtri 
 |-  ( ( ( bday ` X ) +no ( bday ` s ) ) u. ( ( bday ` X ) +no ( bday ` 0s ) ) ) = ( ( bday ` X ) +no ( bday ` s ) )
134 rightold 
 |-  ( s e. ( _Right ` Y ) -> s e. ( _Old ` ( bday ` Y ) ) )
135 oldbday 
 |-  ( ( ( bday ` Y ) e. On /\ s e. No ) -> ( s e. ( _Old ` ( bday ` Y ) ) <-> ( bday ` s ) e. ( bday ` Y ) ) )
136 31 124 135 sylancr 
 |-  ( s e. ( _Right ` Y ) -> ( s e. ( _Old ` ( bday ` Y ) ) <-> ( bday ` s ) e. ( bday ` Y ) ) )
137 134 136 mpbid 
 |-  ( s e. ( _Right ` Y ) -> ( bday ` s ) e. ( bday ` Y ) )
138 naddel2 
 |-  ( ( ( bday ` s ) e. On /\ ( bday ` Y ) e. On /\ ( bday ` X ) e. On ) -> ( ( bday ` s ) e. ( bday ` Y ) <-> ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) )
139 128 31 38 138 mp3an 
 |-  ( ( bday ` s ) e. ( bday ` Y ) <-> ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
140 137 139 sylib 
 |-  ( s e. ( _Right ` Y ) -> ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
141 140 adantl 
 |-  ( ( ph /\ s e. ( _Right ` Y ) ) -> ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
142 elun1 
 |-  ( ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
143 141 142 syl 
 |-  ( ( ph /\ s e. ( _Right ` Y ) ) -> ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
144 133 143 eqeltrid 
 |-  ( ( ph /\ s e. ( _Right ` Y ) ) -> ( ( ( bday ` X ) +no ( bday ` s ) ) u. ( ( bday ` X ) +no ( bday ` 0s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
145 122 123 125 126 144 addsproplem1 
 |-  ( ( ph /\ s e. ( _Right ` Y ) ) -> ( ( X +s s ) e. No /\ ( s  ( s +s X )
146 145 simpld 
 |-  ( ( ph /\ s e. ( _Right ` Y ) ) -> ( X +s s ) e. No )
147 eleq1a 
 |-  ( ( X +s s ) e. No -> ( t = ( X +s s ) -> t e. No ) )
148 146 147 syl 
 |-  ( ( ph /\ s e. ( _Right ` Y ) ) -> ( t = ( X +s s ) -> t e. No ) )
149 148 rexlimdva 
 |-  ( ph -> ( E. s e. ( _Right ` Y ) t = ( X +s s ) -> t e. No ) )
150 149 abssdv 
 |-  ( ph -> { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } C_ No )
151 121 150 unssd 
 |-  ( ph -> ( { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) C_ No )
152 elun 
 |-  ( a e. ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <-> ( a e. { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } \/ a e. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) )
153 vex 
 |-  a e. _V
154 eqeq1 
 |-  ( p = a -> ( p = ( l +s Y ) <-> a = ( l +s Y ) ) )
155 154 rexbidv 
 |-  ( p = a -> ( E. l e. ( _Left ` X ) p = ( l +s Y ) <-> E. l e. ( _Left ` X ) a = ( l +s Y ) ) )
156 153 155 elab 
 |-  ( a e. { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } <-> E. l e. ( _Left ` X ) a = ( l +s Y ) )
157 eqeq1 
 |-  ( q = a -> ( q = ( X +s m ) <-> a = ( X +s m ) ) )
158 157 rexbidv 
 |-  ( q = a -> ( E. m e. ( _Left ` Y ) q = ( X +s m ) <-> E. m e. ( _Left ` Y ) a = ( X +s m ) ) )
159 153 158 elab 
 |-  ( a e. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } <-> E. m e. ( _Left ` Y ) a = ( X +s m ) )
160 156 159 orbi12i 
 |-  ( ( a e. { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } \/ a e. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <-> ( E. l e. ( _Left ` X ) a = ( l +s Y ) \/ E. m e. ( _Left ` Y ) a = ( X +s m ) ) )
161 152 160 bitri 
 |-  ( a e. ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <-> ( E. l e. ( _Left ` X ) a = ( l +s Y ) \/ E. m e. ( _Left ` Y ) a = ( X +s m ) ) )
162 elun 
 |-  ( b e. ( { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) <-> ( b e. { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } \/ b e. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) )
163 vex 
 |-  b e. _V
164 eqeq1 
 |-  ( w = b -> ( w = ( r +s Y ) <-> b = ( r +s Y ) ) )
165 164 rexbidv 
 |-  ( w = b -> ( E. r e. ( _Right ` X ) w = ( r +s Y ) <-> E. r e. ( _Right ` X ) b = ( r +s Y ) ) )
166 163 165 elab 
 |-  ( b e. { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } <-> E. r e. ( _Right ` X ) b = ( r +s Y ) )
167 eqeq1 
 |-  ( t = b -> ( t = ( X +s s ) <-> b = ( X +s s ) ) )
168 167 rexbidv 
 |-  ( t = b -> ( E. s e. ( _Right ` Y ) t = ( X +s s ) <-> E. s e. ( _Right ` Y ) b = ( X +s s ) ) )
169 163 168 elab 
 |-  ( b e. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } <-> E. s e. ( _Right ` Y ) b = ( X +s s ) )
170 166 169 orbi12i 
 |-  ( ( b e. { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } \/ b e. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) <-> ( E. r e. ( _Right ` X ) b = ( r +s Y ) \/ E. s e. ( _Right ` Y ) b = ( X +s s ) ) )
171 162 170 bitri 
 |-  ( b e. ( { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) <-> ( E. r e. ( _Right ` X ) b = ( r +s Y ) \/ E. s e. ( _Right ` Y ) b = ( X +s s ) ) )
172 161 171 anbi12i 
 |-  ( ( a e. ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) /\ b e. ( { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) ) <-> ( ( E. l e. ( _Left ` X ) a = ( l +s Y ) \/ E. m e. ( _Left ` Y ) a = ( X +s m ) ) /\ ( E. r e. ( _Right ` X ) b = ( r +s Y ) \/ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) )
173 anddi 
 |-  ( ( ( E. l e. ( _Left ` X ) a = ( l +s Y ) \/ E. m e. ( _Left ` Y ) a = ( X +s m ) ) /\ ( E. r e. ( _Right ` X ) b = ( r +s Y ) \/ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) <-> ( ( ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) \/ ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) \/ ( ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) \/ ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) ) )
174 172 173 bitri 
 |-  ( ( a e. ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) /\ b e. ( { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) ) <-> ( ( ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) \/ ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) \/ ( ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) \/ ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) ) )
175 reeanv 
 |-  ( E. l e. ( _Left ` X ) E. r e. ( _Right ` X ) ( a = ( l +s Y ) /\ b = ( r +s Y ) ) <-> ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) )
176 lltr 
 |-  ( _Left ` X ) <
177 176 a1i 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> ( _Left ` X ) <
178 simprl 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> l e. ( _Left ` X ) )
179 simprr 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> r e. ( _Right ` X ) )
180 177 178 179 sltssepcd 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> l
181 1 adantr 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` 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 ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )
182 3 adantr 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> Y e. No )
183 19 ad2antrl 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> l e. No )
184 90 ad2antll 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> r e. No )
185 naddcom 
 |-  ( ( ( bday ` Y ) e. On /\ ( bday ` l ) e. On ) -> ( ( bday ` Y ) +no ( bday ` l ) ) = ( ( bday ` l ) +no ( bday ` Y ) ) )
186 31 26 185 mp2an 
 |-  ( ( bday ` Y ) +no ( bday ` l ) ) = ( ( bday ` l ) +no ( bday ` Y ) )
187 44 ad2antrl 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
188 186 187 eqeltrid 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` Y ) +no ( bday ` l ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
189 naddcom 
 |-  ( ( ( bday ` Y ) e. On /\ ( bday ` r ) e. On ) -> ( ( bday ` Y ) +no ( bday ` r ) ) = ( ( bday ` r ) +no ( bday ` Y ) ) )
190 31 95 189 mp2an 
 |-  ( ( bday ` Y ) +no ( bday ` r ) ) = ( ( bday ` r ) +no ( bday ` Y ) )
191 111 ad2antll 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
192 190 191 eqeltrid 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` Y ) +no ( bday ` r ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
193 naddcl 
 |-  ( ( ( bday ` Y ) e. On /\ ( bday ` l ) e. On ) -> ( ( bday ` Y ) +no ( bday ` l ) ) e. On )
194 31 26 193 mp2an 
 |-  ( ( bday ` Y ) +no ( bday ` l ) ) e. On
195 naddcl 
 |-  ( ( ( bday ` Y ) e. On /\ ( bday ` r ) e. On ) -> ( ( bday ` Y ) +no ( bday ` r ) ) e. On )
196 31 95 195 mp2an 
 |-  ( ( bday ` Y ) +no ( bday ` r ) ) e. On
197 naddcl 
 |-  ( ( ( bday ` X ) e. On /\ ( bday ` Y ) e. On ) -> ( ( bday ` X ) +no ( bday ` Y ) ) e. On )
198 38 31 197 mp2an 
 |-  ( ( bday ` X ) +no ( bday ` Y ) ) e. On
199 onunel 
 |-  ( ( ( ( bday ` Y ) +no ( bday ` l ) ) e. On /\ ( ( bday ` Y ) +no ( bday ` r ) ) e. On /\ ( ( bday ` X ) +no ( bday ` Y ) ) e. On ) -> ( ( ( ( bday ` Y ) +no ( bday ` l ) ) u. ( ( bday ` Y ) +no ( bday ` r ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` Y ) +no ( bday ` l ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` Y ) +no ( bday ` r ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) )
200 194 196 198 199 mp3an 
 |-  ( ( ( ( bday ` Y ) +no ( bday ` l ) ) u. ( ( bday ` Y ) +no ( bday ` r ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` Y ) +no ( bday ` l ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` Y ) +no ( bday ` r ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) )
201 188 192 200 sylanbrc 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> ( ( ( bday ` Y ) +no ( bday ` l ) ) u. ( ( bday ` Y ) +no ( bday ` r ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
202 elun1 
 |-  ( ( ( ( bday ` Y ) +no ( bday ` l ) ) u. ( ( bday ` Y ) +no ( bday ` r ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( ( bday ` Y ) +no ( bday ` l ) ) u. ( ( bday ` Y ) +no ( bday ` r ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
203 201 202 syl 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> ( ( ( bday ` Y ) +no ( bday ` l ) ) u. ( ( bday ` Y ) +no ( bday ` r ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
204 181 182 183 184 203 addsproplem1 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> ( ( Y +s l ) e. No /\ ( l  ( l +s Y )
205 204 simprd 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> ( l  ( l +s Y )
206 180 205 mpd 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> ( l +s Y )
207 breq12 
 |-  ( ( a = ( l +s Y ) /\ b = ( r +s Y ) ) -> ( a  ( l +s Y )
208 206 207 syl5ibrcom 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ r e. ( _Right ` X ) ) ) -> ( ( a = ( l +s Y ) /\ b = ( r +s Y ) ) -> a
209 208 rexlimdvva 
 |-  ( ph -> ( E. l e. ( _Left ` X ) E. r e. ( _Right ` X ) ( a = ( l +s Y ) /\ b = ( r +s Y ) ) -> a
210 175 209 biimtrrid 
 |-  ( ph -> ( ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) -> a
211 reeanv 
 |-  ( E. l e. ( _Left ` X ) E. s e. ( _Right ` Y ) ( a = ( l +s Y ) /\ b = ( X +s s ) ) <-> ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) )
212 50 adantrr 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( l +s Y ) e. No )
213 1 adantr 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` 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 )
214 19 ad2antrl 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> l e. No )
215 124 ad2antll 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> s e. No )
216 22 a1i 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> 0s e. No )
217 29 uneq2i 
 |-  ( ( ( bday ` l ) +no ( bday ` s ) ) u. ( ( bday ` l ) +no ( bday ` 0s ) ) ) = ( ( ( bday ` l ) +no ( bday ` s ) ) u. ( bday ` l ) )
218 naddword1 
 |-  ( ( ( bday ` l ) e. On /\ ( bday ` s ) e. On ) -> ( bday ` l ) C_ ( ( bday ` l ) +no ( bday ` s ) ) )
219 26 128 218 mp2an 
 |-  ( bday ` l ) C_ ( ( bday ` l ) +no ( bday ` s ) )
220 ssequn2 
 |-  ( ( bday ` l ) C_ ( ( bday ` l ) +no ( bday ` s ) ) <-> ( ( ( bday ` l ) +no ( bday ` s ) ) u. ( bday ` l ) ) = ( ( bday ` l ) +no ( bday ` s ) ) )
221 219 220 mpbi 
 |-  ( ( ( bday ` l ) +no ( bday ` s ) ) u. ( bday ` l ) ) = ( ( bday ` l ) +no ( bday ` s ) )
222 217 221 eqtri 
 |-  ( ( ( bday ` l ) +no ( bday ` s ) ) u. ( ( bday ` l ) +no ( bday ` 0s ) ) ) = ( ( bday ` l ) +no ( bday ` s ) )
223 naddel1 
 |-  ( ( ( bday ` l ) e. On /\ ( bday ` X ) e. On /\ ( bday ` s ) e. On ) -> ( ( bday ` l ) e. ( bday ` X ) <-> ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` s ) ) ) )
224 26 38 128 223 mp3an 
 |-  ( ( bday ` l ) e. ( bday ` X ) <-> ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` s ) ) )
225 41 224 sylib 
 |-  ( l e. ( _Left ` X ) -> ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` s ) ) )
226 225 ad2antrl 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` s ) ) )
227 140 ad2antll 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
228 ontr1 
 |-  ( ( ( bday ` X ) +no ( bday ` Y ) ) e. On -> ( ( ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` s ) ) /\ ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) -> ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) )
229 198 228 ax-mp 
 |-  ( ( ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` s ) ) /\ ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) -> ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
230 226 227 229 syl2anc 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
231 elun1 
 |-  ( ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
232 230 231 syl 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
233 222 232 eqeltrid 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( ( bday ` l ) +no ( bday ` s ) ) u. ( ( bday ` l ) +no ( bday ` 0s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
234 213 214 215 216 233 addsproplem1 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( l +s s ) e. No /\ ( s  ( s +s l )
235 234 simpld 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( l +s s ) e. No )
236 146 adantrl 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( X +s s ) e. No )
237 rightgt 
 |-  ( s e. ( _Right ` Y ) -> Y
238 237 ad2antll 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> Y
239 3 adantr 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> Y e. No )
240 44 ad2antrl 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
241 naddcl 
 |-  ( ( ( bday ` l ) e. On /\ ( bday ` Y ) e. On ) -> ( ( bday ` l ) +no ( bday ` Y ) ) e. On )
242 26 31 241 mp2an 
 |-  ( ( bday ` l ) +no ( bday ` Y ) ) e. On
243 naddcl 
 |-  ( ( ( bday ` l ) e. On /\ ( bday ` s ) e. On ) -> ( ( bday ` l ) +no ( bday ` s ) ) e. On )
244 26 128 243 mp2an 
 |-  ( ( bday ` l ) +no ( bday ` s ) ) e. On
245 onunel 
 |-  ( ( ( ( bday ` l ) +no ( bday ` Y ) ) e. On /\ ( ( bday ` l ) +no ( bday ` s ) ) e. On /\ ( ( bday ` X ) +no ( bday ` Y ) ) e. On ) -> ( ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( ( bday ` l ) +no ( bday ` s ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) )
246 242 244 198 245 mp3an 
 |-  ( ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( ( bday ` l ) +no ( bday ` s ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` l ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` l ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) )
247 240 230 246 sylanbrc 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( ( bday ` l ) +no ( bday ` s ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
248 elun1 
 |-  ( ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( ( bday ` l ) +no ( bday ` s ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( ( bday ` l ) +no ( bday ` s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
249 247 248 syl 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( ( bday ` l ) +no ( bday ` Y ) ) u. ( ( bday ` l ) +no ( bday ` s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
250 213 214 239 215 249 addsproplem1 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( l +s Y ) e. No /\ ( Y  ( Y +s l )
251 250 simprd 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( Y  ( Y +s l )
252 238 251 mpd 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( Y +s l )
253 214 239 addscomd 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( l +s Y ) = ( Y +s l ) )
254 214 215 addscomd 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( l +s s ) = ( s +s l ) )
255 252 253 254 3brtr4d 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( l +s Y )
256 leftlt 
 |-  ( l e. ( _Left ` X ) -> l
257 256 ad2antrl 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> l
258 2 adantr 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> X e. No )
259 naddcom 
 |-  ( ( ( bday ` s ) e. On /\ ( bday ` l ) e. On ) -> ( ( bday ` s ) +no ( bday ` l ) ) = ( ( bday ` l ) +no ( bday ` s ) ) )
260 128 26 259 mp2an 
 |-  ( ( bday ` s ) +no ( bday ` l ) ) = ( ( bday ` l ) +no ( bday ` s ) )
261 260 230 eqeltrid 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( bday ` s ) +no ( bday ` l ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
262 naddcom 
 |-  ( ( ( bday ` s ) e. On /\ ( bday ` X ) e. On ) -> ( ( bday ` s ) +no ( bday ` X ) ) = ( ( bday ` X ) +no ( bday ` s ) ) )
263 128 38 262 mp2an 
 |-  ( ( bday ` s ) +no ( bday ` X ) ) = ( ( bday ` X ) +no ( bday ` s ) )
264 263 227 eqeltrid 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( bday ` s ) +no ( bday ` X ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
265 naddcl 
 |-  ( ( ( bday ` s ) e. On /\ ( bday ` l ) e. On ) -> ( ( bday ` s ) +no ( bday ` l ) ) e. On )
266 128 26 265 mp2an 
 |-  ( ( bday ` s ) +no ( bday ` l ) ) e. On
267 naddcl 
 |-  ( ( ( bday ` s ) e. On /\ ( bday ` X ) e. On ) -> ( ( bday ` s ) +no ( bday ` X ) ) e. On )
268 128 38 267 mp2an 
 |-  ( ( bday ` s ) +no ( bday ` X ) ) e. On
269 onunel 
 |-  ( ( ( ( bday ` s ) +no ( bday ` l ) ) e. On /\ ( ( bday ` s ) +no ( bday ` X ) ) e. On /\ ( ( bday ` X ) +no ( bday ` Y ) ) e. On ) -> ( ( ( ( bday ` s ) +no ( bday ` l ) ) u. ( ( bday ` s ) +no ( bday ` X ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` s ) +no ( bday ` l ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` s ) +no ( bday ` X ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) )
270 266 268 198 269 mp3an 
 |-  ( ( ( ( bday ` s ) +no ( bday ` l ) ) u. ( ( bday ` s ) +no ( bday ` X ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` s ) +no ( bday ` l ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` s ) +no ( bday ` X ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) )
271 261 264 270 sylanbrc 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( ( bday ` s ) +no ( bday ` l ) ) u. ( ( bday ` s ) +no ( bday ` X ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
272 elun1 
 |-  ( ( ( ( bday ` s ) +no ( bday ` l ) ) u. ( ( bday ` s ) +no ( bday ` X ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( ( bday ` s ) +no ( bday ` l ) ) u. ( ( bday ` s ) +no ( bday ` X ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
273 271 272 syl 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( ( bday ` s ) +no ( bday ` l ) ) u. ( ( bday ` s ) +no ( bday ` X ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
274 213 215 214 258 273 addsproplem1 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( s +s l ) e. No /\ ( l  ( l +s s )
275 274 simprd 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( l  ( l +s s )
276 257 275 mpd 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( l +s s )
277 212 235 236 255 276 ltstrd 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( l +s Y )
278 breq12 
 |-  ( ( a = ( l +s Y ) /\ b = ( X +s s ) ) -> ( a  ( l +s Y )
279 277 278 syl5ibrcom 
 |-  ( ( ph /\ ( l e. ( _Left ` X ) /\ s e. ( _Right ` Y ) ) ) -> ( ( a = ( l +s Y ) /\ b = ( X +s s ) ) -> a
280 279 rexlimdvva 
 |-  ( ph -> ( E. l e. ( _Left ` X ) E. s e. ( _Right ` Y ) ( a = ( l +s Y ) /\ b = ( X +s s ) ) -> a
281 211 280 biimtrrid 
 |-  ( ph -> ( ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) -> a
282 210 281 jaod 
 |-  ( ph -> ( ( ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) \/ ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) -> a
283 reeanv 
 |-  ( E. m e. ( _Left ` Y ) E. r e. ( _Right ` X ) ( a = ( X +s m ) /\ b = ( r +s Y ) ) <-> ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) )
284 1 adantr 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` 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 ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )
285 2 adantr 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> X e. No )
286 57 ad2antrl 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> m e. No )
287 22 a1i 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> 0s e. No )
288 77 ad2antrl 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
289 288 79 syl 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
290 70 289 eqeltrid 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` 0s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
291 284 285 286 287 290 addsproplem1 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( X +s m ) e. No /\ ( m  ( m +s X )
292 291 simpld 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( X +s m ) e. No )
293 90 ad2antll 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> r e. No )
294 98 uneq2i 
 |-  ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( ( bday ` r ) +no ( bday ` 0s ) ) ) = ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( bday ` r ) )
295 naddword1 
 |-  ( ( ( bday ` r ) e. On /\ ( bday ` m ) e. On ) -> ( bday ` r ) C_ ( ( bday ` r ) +no ( bday ` m ) ) )
296 95 65 295 mp2an 
 |-  ( bday ` r ) C_ ( ( bday ` r ) +no ( bday ` m ) )
297 ssequn2 
 |-  ( ( bday ` r ) C_ ( ( bday ` r ) +no ( bday ` m ) ) <-> ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( bday ` r ) ) = ( ( bday ` r ) +no ( bday ` m ) ) )
298 296 297 mpbi 
 |-  ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( bday ` r ) ) = ( ( bday ` r ) +no ( bday ` m ) )
299 294 298 eqtri 
 |-  ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( ( bday ` r ) +no ( bday ` 0s ) ) ) = ( ( bday ` r ) +no ( bday ` m ) )
300 naddel1 
 |-  ( ( ( bday ` r ) e. On /\ ( bday ` X ) e. On /\ ( bday ` m ) e. On ) -> ( ( bday ` r ) e. ( bday ` X ) <-> ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` m ) ) ) )
301 95 38 65 300 mp3an 
 |-  ( ( bday ` r ) e. ( bday ` X ) <-> ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` m ) ) )
302 108 301 sylib 
 |-  ( r e. ( _Right ` X ) -> ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` m ) ) )
303 302 ad2antll 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` m ) ) )
304 ontr1 
 |-  ( ( ( bday ` X ) +no ( bday ` Y ) ) e. On -> ( ( ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` m ) ) /\ ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) -> ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) )
305 198 304 ax-mp 
 |-  ( ( ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` m ) ) /\ ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) -> ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
306 303 288 305 syl2anc 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
307 elun1 
 |-  ( ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
308 306 307 syl 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
309 299 308 eqeltrid 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( ( bday ` r ) +no ( bday ` 0s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
310 284 293 286 287 309 addsproplem1 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( r +s m ) e. No /\ ( m  ( m +s r )
311 310 simpld 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( r +s m ) e. No )
312 3 adantr 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> Y e. No )
313 111 ad2antll 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
314 313 113 syl 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
315 104 314 eqeltrid 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( ( bday ` r ) +no ( bday ` Y ) ) u. ( ( bday ` r ) +no ( bday ` 0s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
316 284 293 312 287 315 addsproplem1 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( r +s Y ) e. No /\ ( Y  ( Y +s r )
317 316 simpld 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( r +s Y ) e. No )
318 rightval 
 |-  ( _Right ` X ) = { r e. ( _Old ` ( bday ` X ) ) | X
319 318 eleq2i 
 |-  ( r e. ( _Right ` X ) <-> r e. { r e. ( _Old ` ( bday ` X ) ) | X
320 319 biimpi 
 |-  ( r e. ( _Right ` X ) -> r e. { r e. ( _Old ` ( bday ` X ) ) | X
321 320 ad2antll 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> r e. { r e. ( _Old ` ( bday ` X ) ) | X
322 rabid 
 |-  ( r e. { r e. ( _Old ` ( bday ` X ) ) | X  ( r e. ( _Old ` ( bday ` X ) ) /\ X
323 321 322 sylib 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( r e. ( _Old ` ( bday ` X ) ) /\ X
324 323 simprd 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> X
325 naddcom 
 |-  ( ( ( bday ` m ) e. On /\ ( bday ` X ) e. On ) -> ( ( bday ` m ) +no ( bday ` X ) ) = ( ( bday ` X ) +no ( bday ` m ) ) )
326 65 38 325 mp2an 
 |-  ( ( bday ` m ) +no ( bday ` X ) ) = ( ( bday ` X ) +no ( bday ` m ) )
327 326 288 eqeltrid 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` m ) +no ( bday ` X ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
328 naddcom 
 |-  ( ( ( bday ` m ) e. On /\ ( bday ` r ) e. On ) -> ( ( bday ` m ) +no ( bday ` r ) ) = ( ( bday ` r ) +no ( bday ` m ) ) )
329 65 95 328 mp2an 
 |-  ( ( bday ` m ) +no ( bday ` r ) ) = ( ( bday ` r ) +no ( bday ` m ) )
330 329 306 eqeltrid 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( bday ` m ) +no ( bday ` r ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
331 naddcl 
 |-  ( ( ( bday ` m ) e. On /\ ( bday ` X ) e. On ) -> ( ( bday ` m ) +no ( bday ` X ) ) e. On )
332 65 38 331 mp2an 
 |-  ( ( bday ` m ) +no ( bday ` X ) ) e. On
333 naddcl 
 |-  ( ( ( bday ` m ) e. On /\ ( bday ` r ) e. On ) -> ( ( bday ` m ) +no ( bday ` r ) ) e. On )
334 65 95 333 mp2an 
 |-  ( ( bday ` m ) +no ( bday ` r ) ) e. On
335 onunel 
 |-  ( ( ( ( bday ` m ) +no ( bday ` X ) ) e. On /\ ( ( bday ` m ) +no ( bday ` r ) ) e. On /\ ( ( bday ` X ) +no ( bday ` Y ) ) e. On ) -> ( ( ( ( bday ` m ) +no ( bday ` X ) ) u. ( ( bday ` m ) +no ( bday ` r ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` m ) +no ( bday ` X ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` m ) +no ( bday ` r ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) )
336 332 334 198 335 mp3an 
 |-  ( ( ( ( bday ` m ) +no ( bday ` X ) ) u. ( ( bday ` m ) +no ( bday ` r ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` m ) +no ( bday ` X ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` m ) +no ( bday ` r ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) )
337 327 330 336 sylanbrc 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( ( bday ` m ) +no ( bday ` X ) ) u. ( ( bday ` m ) +no ( bday ` r ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
338 elun1 
 |-  ( ( ( ( bday ` m ) +no ( bday ` X ) ) u. ( ( bday ` m ) +no ( bday ` r ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( ( bday ` m ) +no ( bday ` X ) ) u. ( ( bday ` m ) +no ( bday ` r ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
339 337 338 syl 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( ( bday ` m ) +no ( bday ` X ) ) u. ( ( bday ` m ) +no ( bday ` r ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
340 284 286 285 293 339 addsproplem1 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( m +s X ) e. No /\ ( X  ( X +s m )
341 340 simprd 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( X  ( X +s m )
342 324 341 mpd 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( X +s m )
343 leftval 
 |-  ( _Left ` Y ) = { m e. ( _Old ` ( bday ` Y ) ) | m
344 343 eleq2i 
 |-  ( m e. ( _Left ` Y ) <-> m e. { m e. ( _Old ` ( bday ` Y ) ) | m
345 344 biimpi 
 |-  ( m e. ( _Left ` Y ) -> m e. { m e. ( _Old ` ( bday ` Y ) ) | m
346 345 ad2antrl 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> m e. { m e. ( _Old ` ( bday ` Y ) ) | m
347 rabid 
 |-  ( m e. { m e. ( _Old ` ( bday ` Y ) ) | m  ( m e. ( _Old ` ( bday ` Y ) ) /\ m
348 346 347 sylib 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( m e. ( _Old ` ( bday ` Y ) ) /\ m
349 348 simprd 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> m
350 naddcl 
 |-  ( ( ( bday ` r ) e. On /\ ( bday ` m ) e. On ) -> ( ( bday ` r ) +no ( bday ` m ) ) e. On )
351 95 65 350 mp2an 
 |-  ( ( bday ` r ) +no ( bday ` m ) ) e. On
352 naddcl 
 |-  ( ( ( bday ` r ) e. On /\ ( bday ` Y ) e. On ) -> ( ( bday ` r ) +no ( bday ` Y ) ) e. On )
353 95 31 352 mp2an 
 |-  ( ( bday ` r ) +no ( bday ` Y ) ) e. On
354 onunel 
 |-  ( ( ( ( bday ` r ) +no ( bday ` m ) ) e. On /\ ( ( bday ` r ) +no ( bday ` Y ) ) e. On /\ ( ( bday ` X ) +no ( bday ` Y ) ) e. On ) -> ( ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( ( bday ` r ) +no ( bday ` Y ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) )
355 351 353 198 354 mp3an 
 |-  ( ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( ( bday ` r ) +no ( bday ` Y ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` r ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` r ) +no ( bday ` Y ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) )
356 306 313 355 sylanbrc 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( ( bday ` r ) +no ( bday ` Y ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
357 elun1 
 |-  ( ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( ( bday ` r ) +no ( bday ` Y ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( ( bday ` r ) +no ( bday ` Y ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
358 356 357 syl 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( ( bday ` r ) +no ( bday ` m ) ) u. ( ( bday ` r ) +no ( bday ` Y ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
359 284 293 286 312 358 addsproplem1 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( r +s m ) e. No /\ ( m  ( m +s r )
360 359 simprd 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( m  ( m +s r )
361 349 360 mpd 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( m +s r )
362 293 286 addscomd 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( r +s m ) = ( m +s r ) )
363 293 312 addscomd 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( r +s Y ) = ( Y +s r ) )
364 361 362 363 3brtr4d 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( r +s m )
365 292 311 317 342 364 ltstrd 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( X +s m )
366 breq12 
 |-  ( ( a = ( X +s m ) /\ b = ( r +s Y ) ) -> ( a  ( X +s m )
367 365 366 syl5ibrcom 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ r e. ( _Right ` X ) ) ) -> ( ( a = ( X +s m ) /\ b = ( r +s Y ) ) -> a
368 367 rexlimdvva 
 |-  ( ph -> ( E. m e. ( _Left ` Y ) E. r e. ( _Right ` X ) ( a = ( X +s m ) /\ b = ( r +s Y ) ) -> a
369 283 368 biimtrrid 
 |-  ( ph -> ( ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) -> a
370 reeanv 
 |-  ( E. m e. ( _Left ` Y ) E. s e. ( _Right ` Y ) ( a = ( X +s m ) /\ b = ( X +s s ) ) <-> ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) )
371 lltr 
 |-  ( _Left ` Y ) <
372 371 a1i 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( _Left ` Y ) <
373 simprl 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> m e. ( _Left ` Y ) )
374 simprr 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> s e. ( _Right ` Y ) )
375 372 373 374 sltssepcd 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> m
376 1 adantr 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` 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 )
377 2 adantr 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> X e. No )
378 57 ad2antrl 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> m e. No )
379 124 ad2antll 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> s e. No )
380 77 ad2antrl 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
381 140 ad2antll 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
382 naddcl 
 |-  ( ( ( bday ` X ) e. On /\ ( bday ` m ) e. On ) -> ( ( bday ` X ) +no ( bday ` m ) ) e. On )
383 38 65 382 mp2an 
 |-  ( ( bday ` X ) +no ( bday ` m ) ) e. On
384 naddcl 
 |-  ( ( ( bday ` X ) e. On /\ ( bday ` s ) e. On ) -> ( ( bday ` X ) +no ( bday ` s ) ) e. On )
385 38 128 384 mp2an 
 |-  ( ( bday ` X ) +no ( bday ` s ) ) e. On
386 onunel 
 |-  ( ( ( ( bday ` X ) +no ( bday ` m ) ) e. On /\ ( ( bday ` X ) +no ( bday ` s ) ) e. On /\ ( ( bday ` X ) +no ( bday ` Y ) ) e. On ) -> ( ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` s ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) ) )
387 383 385 198 386 mp3an 
 |-  ( ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` s ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) <-> ( ( ( bday ` X ) +no ( bday ` m ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) /\ ( ( bday ` X ) +no ( bday ` s ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) ) )
388 380 381 387 sylanbrc 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` s ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) )
389 elun1 
 |-  ( ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` s ) ) ) e. ( ( bday ` X ) +no ( bday ` Y ) ) -> ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
390 388 389 syl 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( ( ( bday ` X ) +no ( bday ` m ) ) u. ( ( bday ` X ) +no ( bday ` s ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
391 376 377 378 379 390 addsproplem1 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( ( X +s m ) e. No /\ ( m  ( m +s X )
392 391 simprd 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( m  ( m +s X )
393 375 392 mpd 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( m +s X )
394 377 378 addscomd 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( X +s m ) = ( m +s X ) )
395 377 379 addscomd 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( X +s s ) = ( s +s X ) )
396 393 394 395 3brtr4d 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( X +s m )
397 breq12 
 |-  ( ( a = ( X +s m ) /\ b = ( X +s s ) ) -> ( a  ( X +s m )
398 396 397 syl5ibrcom 
 |-  ( ( ph /\ ( m e. ( _Left ` Y ) /\ s e. ( _Right ` Y ) ) ) -> ( ( a = ( X +s m ) /\ b = ( X +s s ) ) -> a
399 398 rexlimdvva 
 |-  ( ph -> ( E. m e. ( _Left ` Y ) E. s e. ( _Right ` Y ) ( a = ( X +s m ) /\ b = ( X +s s ) ) -> a
400 370 399 biimtrrid 
 |-  ( ph -> ( ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) -> a
401 369 400 jaod 
 |-  ( ph -> ( ( ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) \/ ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) -> a
402 282 401 jaod 
 |-  ( ph -> ( ( ( ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) \/ ( E. l e. ( _Left ` X ) a = ( l +s Y ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) \/ ( ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. r e. ( _Right ` X ) b = ( r +s Y ) ) \/ ( E. m e. ( _Left ` Y ) a = ( X +s m ) /\ E. s e. ( _Right ` Y ) b = ( X +s s ) ) ) ) -> a
403 174 402 biimtrid 
 |-  ( ph -> ( ( a e. ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) /\ b e. ( { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) ) -> a
404 403 3impib 
 |-  ( ( ph /\ a e. ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) /\ b e. ( { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) ) -> a
405 10 17 88 151 404 sltsd 
 |-  ( ph -> ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <