Metamath Proof Explorer

Theorem sleadd1

Description: Addition to both sides of surreal less-than or equal. Theorem 5 of Conway p. 18. (Contributed by Scott Fenton, 21-Jan-2025)

Ref Expression
Assertion sleadd1 
|- ( ( A e. No /\ B e. No /\ C e. No ) -> ( A <_s B <-> ( A +s C ) <_s ( B +s C ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( x = xO -> ( x +s z ) = ( xO +s z ) )
2 1 breq2d 
 |-  ( x = xO -> ( ( y +s z )  ( y +s z )
3 breq2 
 |-  ( x = xO -> ( y  y
4 2 3 imbi12d 
 |-  ( x = xO -> ( ( ( y +s z )  y  ( ( y +s z )  y
5 oveq1 
 |-  ( y = yO -> ( y +s z ) = ( yO +s z ) )
6 5 breq1d 
 |-  ( y = yO -> ( ( y +s z )  ( yO +s z )
7 breq1 
 |-  ( y = yO -> ( y  yO
8 6 7 imbi12d 
 |-  ( y = yO -> ( ( ( y +s z )  y  ( ( yO +s z )  yO
9 oveq2 
 |-  ( z = zO -> ( yO +s z ) = ( yO +s zO ) )
10 oveq2 
 |-  ( z = zO -> ( xO +s z ) = ( xO +s zO ) )
11 9 10 breq12d 
 |-  ( z = zO -> ( ( yO +s z )  ( yO +s zO )
12 11 imbi1d 
 |-  ( z = zO -> ( ( ( yO +s z )  yO  ( ( yO +s zO )  yO
13 oveq1 
 |-  ( x = xO -> ( x +s zO ) = ( xO +s zO ) )
14 13 breq2d 
 |-  ( x = xO -> ( ( yO +s zO )  ( yO +s zO )
15 breq2 
 |-  ( x = xO -> ( yO  yO
16 14 15 imbi12d 
 |-  ( x = xO -> ( ( ( yO +s zO )  yO  ( ( yO +s zO )  yO
17 oveq1 
 |-  ( y = yO -> ( y +s zO ) = ( yO +s zO ) )
18 17 breq1d 
 |-  ( y = yO -> ( ( y +s zO )  ( yO +s zO )
19 breq1 
 |-  ( y = yO -> ( y  yO
20 18 19 imbi12d 
 |-  ( y = yO -> ( ( ( y +s zO )  y  ( ( yO +s zO )  yO
21 17 breq1d 
 |-  ( y = yO -> ( ( y +s zO )  ( yO +s zO )
22 21 7 imbi12d 
 |-  ( y = yO -> ( ( ( y +s zO )  y  ( ( yO +s zO )  yO
23 oveq2 
 |-  ( z = zO -> ( x +s z ) = ( x +s zO ) )
24 9 23 breq12d 
 |-  ( z = zO -> ( ( yO +s z )  ( yO +s zO )
25 24 imbi1d 
 |-  ( z = zO -> ( ( ( yO +s z )  yO  ( ( yO +s zO )  yO
26 oveq1 
 |-  ( x = A -> ( x +s z ) = ( A +s z ) )
27 26 breq2d 
 |-  ( x = A -> ( ( y +s z )  ( y +s z )
28 breq2 
 |-  ( x = A -> ( y  y
29 27 28 imbi12d 
 |-  ( x = A -> ( ( ( y +s z )  y  ( ( y +s z )  y
30 oveq1 
 |-  ( y = B -> ( y +s z ) = ( B +s z ) )
31 30 breq1d 
 |-  ( y = B -> ( ( y +s z )  ( B +s z )
32 breq1 
 |-  ( y = B -> ( y  B
33 31 32 imbi12d 
 |-  ( y = B -> ( ( ( y +s z )  y  ( ( B +s z )  B
34 oveq2 
 |-  ( z = C -> ( B +s z ) = ( B +s C ) )
35 oveq2 
 |-  ( z = C -> ( A +s z ) = ( A +s C ) )
36 34 35 breq12d 
 |-  ( z = C -> ( ( B +s z )  ( B +s C )
37 36 imbi1d 
 |-  ( z = C -> ( ( ( B +s z )  B  ( ( B +s C )  B
38 simp2 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> y e. No )
39 simp3 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> z e. No )
40 38 39 addscut 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> ( ( y +s z ) e. No /\ ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) <
41 simp2 
 |-  ( ( ( y +s z ) e. No /\ ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) < ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) <
42 40 41 syl 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) <
43 40 simp3d 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> { ( y +s z ) } <
44 ovex 
 |-  ( y +s z ) e. _V
45 44 snnz 
 |-  { ( y +s z ) } =/= (/)
46 sslttr 
 |-  ( ( ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) < ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) <
47 45 46 mp3an3 
 |-  ( ( ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) < ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) <
48 42 43 47 syl2anc 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) <
49 simp1 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> x e. No )
50 49 39 addscut 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> ( ( x +s z ) e. No /\ ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) <
51 simp2 
 |-  ( ( ( x +s z ) e. No /\ ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) < ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) <
52 50 51 syl 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) <
53 50 simp3d 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> { ( x +s z ) } <
54 ovex 
 |-  ( x +s z ) e. _V
55 54 snnz 
 |-  { ( x +s z ) } =/= (/)
56 sslttr 
 |-  ( ( ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) < ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) <
57 55 56 mp3an3 
 |-  ( ( ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) < ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) <
58 52 53 57 syl2anc 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) <
59 addsval2 
 |-  ( ( y e. No /\ z e. No ) -> ( y +s z ) = ( ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) |s ( { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } ) ) )
60 59 3adant1 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> ( y +s z ) = ( ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) |s ( { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } ) ) )
61 addsval2 
 |-  ( ( x e. No /\ z e. No ) -> ( x +s z ) = ( ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) |s ( { c | E. xR e. ( _Right ` x ) c = ( xR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( x +s zR ) } ) ) )
62 61 3adant2 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> ( x +s z ) = ( ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) |s ( { c | E. xR e. ( _Right ` x ) c = ( xR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( x +s zR ) } ) ) )
63 sltrec 
 |-  ( ( ( ( { a | E. yL e. ( _Left ` y ) a = ( yL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( y +s zL ) } ) < ( ( y +s z )  ( E. p e. ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) ( y +s z ) <_s p \/ E. q e. ( { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } ) q <_s ( x +s z ) ) ) )
64 48 58 60 62 63 syl22anc 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> ( ( y +s z )  ( E. p e. ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) ( y +s z ) <_s p \/ E. q e. ( { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } ) q <_s ( x +s z ) ) ) )
65 64 adantr 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( ( y +s z )  ( E. p e. ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) ( y +s z ) <_s p \/ E. q e. ( { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } ) q <_s ( x +s z ) ) ) )
66 rexun 
 |-  ( E. p e. ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) ( y +s z ) <_s p <-> ( E. p e. { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } ( y +s z ) <_s p \/ E. p e. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ( y +s z ) <_s p ) )
67 eqeq1 
 |-  ( a = p -> ( a = ( xL +s z ) <-> p = ( xL +s z ) ) )
68 67 rexbidv 
 |-  ( a = p -> ( E. xL e. ( _Left ` x ) a = ( xL +s z ) <-> E. xL e. ( _Left ` x ) p = ( xL +s z ) ) )
69 68 rexab 
 |-  ( E. p e. { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } ( y +s z ) <_s p <-> E. p ( E. xL e. ( _Left ` x ) p = ( xL +s z ) /\ ( y +s z ) <_s p ) )
70 rexcom4 
 |-  ( E. xL e. ( _Left ` x ) E. p ( p = ( xL +s z ) /\ ( y +s z ) <_s p ) <-> E. p E. xL e. ( _Left ` x ) ( p = ( xL +s z ) /\ ( y +s z ) <_s p ) )
71 r19.41v 
 |-  ( E. xL e. ( _Left ` x ) ( p = ( xL +s z ) /\ ( y +s z ) <_s p ) <-> ( E. xL e. ( _Left ` x ) p = ( xL +s z ) /\ ( y +s z ) <_s p ) )
72 71 exbii 
 |-  ( E. p E. xL e. ( _Left ` x ) ( p = ( xL +s z ) /\ ( y +s z ) <_s p ) <-> E. p ( E. xL e. ( _Left ` x ) p = ( xL +s z ) /\ ( y +s z ) <_s p ) )
73 70 72 bitri 
 |-  ( E. xL e. ( _Left ` x ) E. p ( p = ( xL +s z ) /\ ( y +s z ) <_s p ) <-> E. p ( E. xL e. ( _Left ` x ) p = ( xL +s z ) /\ ( y +s z ) <_s p ) )
74 ovex 
 |-  ( xL +s z ) e. _V
75 breq2 
 |-  ( p = ( xL +s z ) -> ( ( y +s z ) <_s p <-> ( y +s z ) <_s ( xL +s z ) ) )
76 74 75 ceqsexv 
 |-  ( E. p ( p = ( xL +s z ) /\ ( y +s z ) <_s p ) <-> ( y +s z ) <_s ( xL +s z ) )
77 76 rexbii 
 |-  ( E. xL e. ( _Left ` x ) E. p ( p = ( xL +s z ) /\ ( y +s z ) <_s p ) <-> E. xL e. ( _Left ` x ) ( y +s z ) <_s ( xL +s z ) )
78 73 77 bitr3i 
 |-  ( E. p ( E. xL e. ( _Left ` x ) p = ( xL +s z ) /\ ( y +s z ) <_s p ) <-> E. xL e. ( _Left ` x ) ( y +s z ) <_s ( xL +s z ) )
79 69 78 bitri 
 |-  ( E. p e. { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } ( y +s z ) <_s p <-> E. xL e. ( _Left ` x ) ( y +s z ) <_s ( xL +s z ) )
80 eqeq1 
 |-  ( b = p -> ( b = ( x +s zL ) <-> p = ( x +s zL ) ) )
81 80 rexbidv 
 |-  ( b = p -> ( E. zL e. ( _Left ` z ) b = ( x +s zL ) <-> E. zL e. ( _Left ` z ) p = ( x +s zL ) ) )
82 81 rexab 
 |-  ( E. p e. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ( y +s z ) <_s p <-> E. p ( E. zL e. ( _Left ` z ) p = ( x +s zL ) /\ ( y +s z ) <_s p ) )
83 rexcom4 
 |-  ( E. zL e. ( _Left ` z ) E. p ( p = ( x +s zL ) /\ ( y +s z ) <_s p ) <-> E. p E. zL e. ( _Left ` z ) ( p = ( x +s zL ) /\ ( y +s z ) <_s p ) )
84 r19.41v 
 |-  ( E. zL e. ( _Left ` z ) ( p = ( x +s zL ) /\ ( y +s z ) <_s p ) <-> ( E. zL e. ( _Left ` z ) p = ( x +s zL ) /\ ( y +s z ) <_s p ) )
85 84 exbii 
 |-  ( E. p E. zL e. ( _Left ` z ) ( p = ( x +s zL ) /\ ( y +s z ) <_s p ) <-> E. p ( E. zL e. ( _Left ` z ) p = ( x +s zL ) /\ ( y +s z ) <_s p ) )
86 83 85 bitri 
 |-  ( E. zL e. ( _Left ` z ) E. p ( p = ( x +s zL ) /\ ( y +s z ) <_s p ) <-> E. p ( E. zL e. ( _Left ` z ) p = ( x +s zL ) /\ ( y +s z ) <_s p ) )
87 ovex 
 |-  ( x +s zL ) e. _V
88 breq2 
 |-  ( p = ( x +s zL ) -> ( ( y +s z ) <_s p <-> ( y +s z ) <_s ( x +s zL ) ) )
89 87 88 ceqsexv 
 |-  ( E. p ( p = ( x +s zL ) /\ ( y +s z ) <_s p ) <-> ( y +s z ) <_s ( x +s zL ) )
90 89 rexbii 
 |-  ( E. zL e. ( _Left ` z ) E. p ( p = ( x +s zL ) /\ ( y +s z ) <_s p ) <-> E. zL e. ( _Left ` z ) ( y +s z ) <_s ( x +s zL ) )
91 86 90 bitr3i 
 |-  ( E. p ( E. zL e. ( _Left ` z ) p = ( x +s zL ) /\ ( y +s z ) <_s p ) <-> E. zL e. ( _Left ` z ) ( y +s z ) <_s ( x +s zL ) )
92 82 91 bitri 
 |-  ( E. p e. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ( y +s z ) <_s p <-> E. zL e. ( _Left ` z ) ( y +s z ) <_s ( x +s zL ) )
93 79 92 orbi12i 
 |-  ( ( E. p e. { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } ( y +s z ) <_s p \/ E. p e. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ( y +s z ) <_s p ) <-> ( E. xL e. ( _Left ` x ) ( y +s z ) <_s ( xL +s z ) \/ E. zL e. ( _Left ` z ) ( y +s z ) <_s ( x +s zL ) ) )
94 66 93 bitri 
 |-  ( E. p e. ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) ( y +s z ) <_s p <-> ( E. xL e. ( _Left ` x ) ( y +s z ) <_s ( xL +s z ) \/ E. zL e. ( _Left ` z ) ( y +s z ) <_s ( x +s zL ) ) )
95 simpll2 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  y e. No )
96 leftssno 
 |-  ( _Left ` x ) C_ No
97 96 sseli 
 |-  ( xL e. ( _Left ` x ) -> xL e. No )
98 97 adantr 
 |-  ( ( xL e. ( _Left ` x ) /\ ( y +s z ) <_s ( xL +s z ) ) -> xL e. No )
99 98 adantl 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  xL e. No )
100 simpll1 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  x e. No )
101 simprr 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( y +s z ) <_s ( xL +s z ) )
102 simpll3 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  z e. No )
103 sleadd1im 
 |-  ( ( y e. No /\ xL e. No /\ z e. No ) -> ( ( y +s z ) <_s ( xL +s z ) -> y <_s xL ) )
104 95 99 102 103 syl3anc 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( ( y +s z ) <_s ( xL +s z ) -> y <_s xL ) )
105 101 104 mpd 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  y <_s xL )
106 leftval 
 |-  ( _Left ` x ) = { xL e. ( _Old ` ( bday ` x ) ) | xL
107 106 reqabi 
 |-  ( xL e. ( _Left ` x ) <-> ( xL e. ( _Old ` ( bday ` x ) ) /\ xL
108 107 simprbi 
 |-  ( xL e. ( _Left ` x ) -> xL
109 108 adantr 
 |-  ( ( xL e. ( _Left ` x ) /\ ( y +s z ) <_s ( xL +s z ) ) -> xL
110 109 adantl 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  xL
111 95 99 100 105 110 slelttrd 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  y
112 111 rexlimdvaa 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( E. xL e. ( _Left ` x ) ( y +s z ) <_s ( xL +s z ) -> y
113 simpll2 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  y e. No )
114 leftssno 
 |-  ( _Left ` z ) C_ No
115 114 sseli 
 |-  ( zL e. ( _Left ` z ) -> zL e. No )
116 115 adantr 
 |-  ( ( zL e. ( _Left ` z ) /\ ( y +s z ) <_s ( x +s zL ) ) -> zL e. No )
117 116 adantl 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  zL e. No )
118 113 117 addscld 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( y +s zL ) e. No )
119 simpll3 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  z e. No )
120 113 119 addscld 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( y +s z ) e. No )
121 simpll1 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  x e. No )
122 121 117 addscld 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( x +s zL ) e. No )
123 leftval 
 |-  ( _Left ` z ) = { zL e. ( _Old ` ( bday ` z ) ) | zL
124 123 reqabi 
 |-  ( zL e. ( _Left ` z ) <-> ( zL e. ( _Old ` ( bday ` z ) ) /\ zL
125 124 simprbi 
 |-  ( zL e. ( _Left ` z ) -> zL
126 125 adantr 
 |-  ( ( zL e. ( _Left ` z ) /\ ( y +s z ) <_s ( x +s zL ) ) -> zL
127 126 adantl 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  zL
128 sltadd2im 
 |-  ( ( zL e. No /\ z e. No /\ y e. No ) -> ( zL  ( y +s zL )
129 117 119 113 128 syl3anc 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( zL  ( y +s zL )
130 127 129 mpd 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( y +s zL )
131 simprr 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( y +s z ) <_s ( x +s zL ) )
132 118 120 122 130 131 sltletrd 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( y +s zL )
133 oveq2 
 |-  ( zO = zL -> ( y +s zO ) = ( y +s zL ) )
134 oveq2 
 |-  ( zO = zL -> ( x +s zO ) = ( x +s zL ) )
135 133 134 breq12d 
 |-  ( zO = zL -> ( ( y +s zO )  ( y +s zL )
136 135 imbi1d 
 |-  ( zO = zL -> ( ( ( y +s zO )  y  ( ( y +s zL )  y
137 simplr3 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( y +s zO )  y
138 simprl 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  zL e. ( _Left ` z ) )
139 elun1 
 |-  ( zL e. ( _Left ` z ) -> zL e. ( ( _Left ` z ) u. ( _Right ` z ) ) )
140 138 139 syl 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  zL e. ( ( _Left ` z ) u. ( _Right ` z ) ) )
141 136 137 140 rspcdva 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( ( y +s zL )  y
142 132 141 mpd 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  y
143 142 rexlimdvaa 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( E. zL e. ( _Left ` z ) ( y +s z ) <_s ( x +s zL ) -> y
144 112 143 jaod 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( ( E. xL e. ( _Left ` x ) ( y +s z ) <_s ( xL +s z ) \/ E. zL e. ( _Left ` z ) ( y +s z ) <_s ( x +s zL ) ) -> y
145 94 144 biimtrid 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( E. p e. ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) ( y +s z ) <_s p -> y
146 rexun 
 |-  ( E. q e. ( { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } ) q <_s ( x +s z ) <-> ( E. q e. { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } q <_s ( x +s z ) \/ E. q e. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } q <_s ( x +s z ) ) )
147 eqeq1 
 |-  ( c = q -> ( c = ( yR +s z ) <-> q = ( yR +s z ) ) )
148 147 rexbidv 
 |-  ( c = q -> ( E. yR e. ( _Right ` y ) c = ( yR +s z ) <-> E. yR e. ( _Right ` y ) q = ( yR +s z ) ) )
149 148 rexab 
 |-  ( E. q e. { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } q <_s ( x +s z ) <-> E. q ( E. yR e. ( _Right ` y ) q = ( yR +s z ) /\ q <_s ( x +s z ) ) )
150 rexcom4 
 |-  ( E. yR e. ( _Right ` y ) E. q ( q = ( yR +s z ) /\ q <_s ( x +s z ) ) <-> E. q E. yR e. ( _Right ` y ) ( q = ( yR +s z ) /\ q <_s ( x +s z ) ) )
151 r19.41v 
 |-  ( E. yR e. ( _Right ` y ) ( q = ( yR +s z ) /\ q <_s ( x +s z ) ) <-> ( E. yR e. ( _Right ` y ) q = ( yR +s z ) /\ q <_s ( x +s z ) ) )
152 151 exbii 
 |-  ( E. q E. yR e. ( _Right ` y ) ( q = ( yR +s z ) /\ q <_s ( x +s z ) ) <-> E. q ( E. yR e. ( _Right ` y ) q = ( yR +s z ) /\ q <_s ( x +s z ) ) )
153 150 152 bitri 
 |-  ( E. yR e. ( _Right ` y ) E. q ( q = ( yR +s z ) /\ q <_s ( x +s z ) ) <-> E. q ( E. yR e. ( _Right ` y ) q = ( yR +s z ) /\ q <_s ( x +s z ) ) )
154 ovex 
 |-  ( yR +s z ) e. _V
155 breq1 
 |-  ( q = ( yR +s z ) -> ( q <_s ( x +s z ) <-> ( yR +s z ) <_s ( x +s z ) ) )
156 154 155 ceqsexv 
 |-  ( E. q ( q = ( yR +s z ) /\ q <_s ( x +s z ) ) <-> ( yR +s z ) <_s ( x +s z ) )
157 156 rexbii 
 |-  ( E. yR e. ( _Right ` y ) E. q ( q = ( yR +s z ) /\ q <_s ( x +s z ) ) <-> E. yR e. ( _Right ` y ) ( yR +s z ) <_s ( x +s z ) )
158 153 157 bitr3i 
 |-  ( E. q ( E. yR e. ( _Right ` y ) q = ( yR +s z ) /\ q <_s ( x +s z ) ) <-> E. yR e. ( _Right ` y ) ( yR +s z ) <_s ( x +s z ) )
159 149 158 bitri 
 |-  ( E. q e. { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } q <_s ( x +s z ) <-> E. yR e. ( _Right ` y ) ( yR +s z ) <_s ( x +s z ) )
160 eqeq1 
 |-  ( d = q -> ( d = ( y +s zR ) <-> q = ( y +s zR ) ) )
161 160 rexbidv 
 |-  ( d = q -> ( E. zR e. ( _Right ` z ) d = ( y +s zR ) <-> E. zR e. ( _Right ` z ) q = ( y +s zR ) ) )
162 161 rexab 
 |-  ( E. q e. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } q <_s ( x +s z ) <-> E. q ( E. zR e. ( _Right ` z ) q = ( y +s zR ) /\ q <_s ( x +s z ) ) )
163 rexcom4 
 |-  ( E. zR e. ( _Right ` z ) E. q ( q = ( y +s zR ) /\ q <_s ( x +s z ) ) <-> E. q E. zR e. ( _Right ` z ) ( q = ( y +s zR ) /\ q <_s ( x +s z ) ) )
164 r19.41v 
 |-  ( E. zR e. ( _Right ` z ) ( q = ( y +s zR ) /\ q <_s ( x +s z ) ) <-> ( E. zR e. ( _Right ` z ) q = ( y +s zR ) /\ q <_s ( x +s z ) ) )
165 164 exbii 
 |-  ( E. q E. zR e. ( _Right ` z ) ( q = ( y +s zR ) /\ q <_s ( x +s z ) ) <-> E. q ( E. zR e. ( _Right ` z ) q = ( y +s zR ) /\ q <_s ( x +s z ) ) )
166 163 165 bitri 
 |-  ( E. zR e. ( _Right ` z ) E. q ( q = ( y +s zR ) /\ q <_s ( x +s z ) ) <-> E. q ( E. zR e. ( _Right ` z ) q = ( y +s zR ) /\ q <_s ( x +s z ) ) )
167 ovex 
 |-  ( y +s zR ) e. _V
168 breq1 
 |-  ( q = ( y +s zR ) -> ( q <_s ( x +s z ) <-> ( y +s zR ) <_s ( x +s z ) ) )
169 167 168 ceqsexv 
 |-  ( E. q ( q = ( y +s zR ) /\ q <_s ( x +s z ) ) <-> ( y +s zR ) <_s ( x +s z ) )
170 169 rexbii 
 |-  ( E. zR e. ( _Right ` z ) E. q ( q = ( y +s zR ) /\ q <_s ( x +s z ) ) <-> E. zR e. ( _Right ` z ) ( y +s zR ) <_s ( x +s z ) )
171 166 170 bitr3i 
 |-  ( E. q ( E. zR e. ( _Right ` z ) q = ( y +s zR ) /\ q <_s ( x +s z ) ) <-> E. zR e. ( _Right ` z ) ( y +s zR ) <_s ( x +s z ) )
172 162 171 bitri 
 |-  ( E. q e. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } q <_s ( x +s z ) <-> E. zR e. ( _Right ` z ) ( y +s zR ) <_s ( x +s z ) )
173 159 172 orbi12i 
 |-  ( ( E. q e. { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } q <_s ( x +s z ) \/ E. q e. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } q <_s ( x +s z ) ) <-> ( E. yR e. ( _Right ` y ) ( yR +s z ) <_s ( x +s z ) \/ E. zR e. ( _Right ` z ) ( y +s zR ) <_s ( x +s z ) ) )
174 146 173 bitri 
 |-  ( E. q e. ( { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } ) q <_s ( x +s z ) <-> ( E. yR e. ( _Right ` y ) ( yR +s z ) <_s ( x +s z ) \/ E. zR e. ( _Right ` z ) ( y +s zR ) <_s ( x +s z ) ) )
175 simpll2 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  y e. No )
176 rightssno 
 |-  ( _Right ` y ) C_ No
177 176 sseli 
 |-  ( yR e. ( _Right ` y ) -> yR e. No )
178 177 adantr 
 |-  ( ( yR e. ( _Right ` y ) /\ ( yR +s z ) <_s ( x +s z ) ) -> yR e. No )
179 178 adantl 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  yR e. No )
180 simpll1 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  x e. No )
181 rightval 
 |-  ( _Right ` y ) = { yR e. ( _Old ` ( bday ` y ) ) | y
182 181 reqabi 
 |-  ( yR e. ( _Right ` y ) <-> ( yR e. ( _Old ` ( bday ` y ) ) /\ y
183 182 simprbi 
 |-  ( yR e. ( _Right ` y ) -> y
184 183 adantr 
 |-  ( ( yR e. ( _Right ` y ) /\ ( yR +s z ) <_s ( x +s z ) ) -> y
185 184 adantl 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  y
186 simprr 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( yR +s z ) <_s ( x +s z ) )
187 simpll3 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  z e. No )
188 sleadd1im 
 |-  ( ( yR e. No /\ x e. No /\ z e. No ) -> ( ( yR +s z ) <_s ( x +s z ) -> yR <_s x ) )
189 179 180 187 188 syl3anc 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( ( yR +s z ) <_s ( x +s z ) -> yR <_s x ) )
190 186 189 mpd 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  yR <_s x )
191 175 179 180 185 190 sltletrd 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  y
192 191 rexlimdvaa 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( E. yR e. ( _Right ` y ) ( yR +s z ) <_s ( x +s z ) -> y
193 simpll2 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  y e. No )
194 rightssno 
 |-  ( _Right ` z ) C_ No
195 194 sseli 
 |-  ( zR e. ( _Right ` z ) -> zR e. No )
196 195 adantr 
 |-  ( ( zR e. ( _Right ` z ) /\ ( y +s zR ) <_s ( x +s z ) ) -> zR e. No )
197 196 adantl 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  zR e. No )
198 193 197 addscld 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( y +s zR ) e. No )
199 simpll1 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  x e. No )
200 simpll3 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  z e. No )
201 199 200 addscld 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( x +s z ) e. No )
202 199 197 addscld 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( x +s zR ) e. No )
203 simprr 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( y +s zR ) <_s ( x +s z ) )
204 200 197 199 3jca 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( z e. No /\ zR e. No /\ x e. No ) )
205 rightval 
 |-  ( _Right ` z ) = { zR e. ( _Old ` ( bday ` z ) ) | z
206 205 reqabi 
 |-  ( zR e. ( _Right ` z ) <-> ( zR e. ( _Old ` ( bday ` z ) ) /\ z
207 206 simprbi 
 |-  ( zR e. ( _Right ` z ) -> z
208 207 adantr 
 |-  ( ( zR e. ( _Right ` z ) /\ ( y +s zR ) <_s ( x +s z ) ) -> z
209 208 adantl 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  z
210 sltadd2im 
 |-  ( ( z e. No /\ zR e. No /\ x e. No ) -> ( z  ( x +s z )
211 204 209 210 sylc 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( x +s z )
212 198 201 202 203 211 slelttrd 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( y +s zR )
213 oveq2 
 |-  ( zO = zR -> ( y +s zO ) = ( y +s zR ) )
214 oveq2 
 |-  ( zO = zR -> ( x +s zO ) = ( x +s zR ) )
215 213 214 breq12d 
 |-  ( zO = zR -> ( ( y +s zO )  ( y +s zR )
216 215 imbi1d 
 |-  ( zO = zR -> ( ( ( y +s zO )  y  ( ( y +s zR )  y
217 simplr3 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( y +s zO )  y
218 simprl 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  zR e. ( _Right ` z ) )
219 elun2 
 |-  ( zR e. ( _Right ` z ) -> zR e. ( ( _Left ` z ) u. ( _Right ` z ) ) )
220 218 219 syl 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  zR e. ( ( _Left ` z ) u. ( _Right ` z ) ) )
221 216 217 220 rspcdva 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( ( y +s zR )  y
222 212 221 mpd 
 |-  ( ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  y
223 222 rexlimdvaa 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( E. zR e. ( _Right ` z ) ( y +s zR ) <_s ( x +s z ) -> y
224 192 223 jaod 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( ( E. yR e. ( _Right ` y ) ( yR +s z ) <_s ( x +s z ) \/ E. zR e. ( _Right ` z ) ( y +s zR ) <_s ( x +s z ) ) -> y
225 174 224 biimtrid 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( E. q e. ( { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } ) q <_s ( x +s z ) -> y
226 145 225 jaod 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( ( E. p e. ( { a | E. xL e. ( _Left ` x ) a = ( xL +s z ) } u. { b | E. zL e. ( _Left ` z ) b = ( x +s zL ) } ) ( y +s z ) <_s p \/ E. q e. ( { c | E. yR e. ( _Right ` y ) c = ( yR +s z ) } u. { d | E. zR e. ( _Right ` z ) d = ( y +s zR ) } ) q <_s ( x +s z ) ) -> y
227 65 226 sylbid 
 |-  ( ( ( x e. No /\ y e. No /\ z e. No ) /\ ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( ( y +s z )  y
228 227 ex 
 |-  ( ( x e. No /\ y e. No /\ z e. No ) -> ( ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) A. zO e. ( ( _Left ` z ) u. ( _Right ` z ) ) ( ( yO +s zO )  yO  yO  y  y  yO  yO  y  ( ( y +s z )  y
229 4 8 12 16 20 22 25 29 33 37 228 no3inds 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( B +s C )  B
230 addscl 
 |-  ( ( B e. No /\ C e. No ) -> ( B +s C ) e. No )
231 230 3adant1 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( B +s C ) e. No )
232 addscl 
 |-  ( ( A e. No /\ C e. No ) -> ( A +s C ) e. No )
233 232 3adant2 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( A +s C ) e. No )
234 sltnle 
 |-  ( ( ( B +s C ) e. No /\ ( A +s C ) e. No ) -> ( ( B +s C )  -. ( A +s C ) <_s ( B +s C ) ) )
235 231 233 234 syl2anc 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( B +s C )  -. ( A +s C ) <_s ( B +s C ) ) )
236 sltnle 
 |-  ( ( B e. No /\ A e. No ) -> ( B  -. A <_s B ) )
237 236 ancoms 
 |-  ( ( A e. No /\ B e. No ) -> ( B  -. A <_s B ) )
238 237 3adant3 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( B  -. A <_s B ) )
239 229 235 238 3imtr3d 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( -. ( A +s C ) <_s ( B +s C ) -> -. A <_s B ) )
240 239 con4d 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( A <_s B -> ( A +s C ) <_s ( B +s C ) ) )
241 sleadd1im 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( A +s C ) <_s ( B +s C ) -> A <_s B ) )
242 240 241 impbid 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( A <_s B <-> ( A +s C ) <_s ( B +s C ) ) )