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 48 58 60 62 sltrecd 
 |-  ( ( 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 ) ) ) )
64 63 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 ) ) ) )
65 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 ) )
66 eqeq1 
 |-  ( a = p -> ( a = ( xL +s z ) <-> p = ( xL +s z ) ) )
67 66 rexbidv 
 |-  ( a = p -> ( E. xL e. ( _Left ` x ) a = ( xL +s z ) <-> E. xL e. ( _Left ` x ) p = ( xL +s z ) ) )
68 67 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 ) )
69 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 ) )
70 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 ) )
71 70 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 ) )
72 69 71 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 ) )
73 ovex 
 |-  ( xL +s z ) e. _V
74 breq2 
 |-  ( p = ( xL +s z ) -> ( ( y +s z ) <_s p <-> ( y +s z ) <_s ( xL +s z ) ) )
75 73 74 ceqsexv 
 |-  ( E. p ( p = ( xL +s z ) /\ ( y +s z ) <_s p ) <-> ( y +s z ) <_s ( xL +s z ) )
76 75 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 ) )
77 72 76 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 ) )
78 68 77 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 ) )
79 eqeq1 
 |-  ( b = p -> ( b = ( x +s zL ) <-> p = ( x +s zL ) ) )
80 79 rexbidv 
 |-  ( b = p -> ( E. zL e. ( _Left ` z ) b = ( x +s zL ) <-> E. zL e. ( _Left ` z ) p = ( x +s zL ) ) )
81 80 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 ) )
82 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 ) )
83 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 ) )
84 83 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 ) )
85 82 84 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 ) )
86 ovex 
 |-  ( x +s zL ) e. _V
87 breq2 
 |-  ( p = ( x +s zL ) -> ( ( y +s z ) <_s p <-> ( y +s z ) <_s ( x +s zL ) ) )
88 86 87 ceqsexv 
 |-  ( E. p ( p = ( x +s zL ) /\ ( y +s z ) <_s p ) <-> ( y +s z ) <_s ( x +s zL ) )
89 88 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 ) )
90 85 89 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 ) )
91 81 90 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 ) )
92 78 91 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 ) ) )
93 65 92 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 ) ) )
94 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 )
95 leftssno 
 |-  ( _Left ` x ) C_ No
96 95 sseli 
 |-  ( xL e. ( _Left ` x ) -> xL e. No )
97 96 adantr 
 |-  ( ( xL e. ( _Left ` x ) /\ ( y +s z ) <_s ( xL +s z ) ) -> xL e. No )
98 97 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 )
99 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 )
100 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 ) )
101 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 )
102 sleadd1im 
 |-  ( ( y e. No /\ xL e. No /\ z e. No ) -> ( ( y +s z ) <_s ( xL +s z ) -> y <_s xL ) )
103 94 98 101 102 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 ) )
104 100 103 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 )
105 leftlt 
 |-  ( xL e. ( _Left ` x ) -> xL
106 105 adantr 
 |-  ( ( xL e. ( _Left ` x ) /\ ( y +s z ) <_s ( xL +s z ) ) -> xL
107 106 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
108 94 98 99 104 107 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
109 108 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
110 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 )
111 leftssno 
 |-  ( _Left ` z ) C_ No
112 111 sseli 
 |-  ( zL e. ( _Left ` z ) -> zL e. No )
113 112 adantr 
 |-  ( ( zL e. ( _Left ` z ) /\ ( y +s z ) <_s ( x +s zL ) ) -> zL e. No )
114 113 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 )
115 110 114 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 )
116 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 )
117 110 116 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 )
118 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 )
119 118 114 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 )
120 leftlt 
 |-  ( zL e. ( _Left ` z ) -> zL
121 120 adantr 
 |-  ( ( zL e. ( _Left ` z ) /\ ( y +s z ) <_s ( x +s zL ) ) -> zL
122 121 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
123 sltadd2im 
 |-  ( ( zL e. No /\ z e. No /\ y e. No ) -> ( zL  ( y +s zL )
124 114 116 110 123 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 )
125 122 124 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 )
126 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 ) )
127 115 117 119 125 126 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 )
128 oveq2 
 |-  ( zO = zL -> ( y +s zO ) = ( y +s zL ) )
129 oveq2 
 |-  ( zO = zL -> ( x +s zO ) = ( x +s zL ) )
130 128 129 breq12d 
 |-  ( zO = zL -> ( ( y +s zO )  ( y +s zL )
131 130 imbi1d 
 |-  ( zO = zL -> ( ( ( y +s zO )  y  ( ( y +s zL )  y
132 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
133 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 ) )
134 elun1 
 |-  ( zL e. ( _Left ` z ) -> zL e. ( ( _Left ` z ) u. ( _Right ` z ) ) )
135 133 134 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 ) ) )
136 131 132 135 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
137 127 136 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
138 137 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
139 109 138 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
140 93 139 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
141 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 ) ) )
142 eqeq1 
 |-  ( c = q -> ( c = ( yR +s z ) <-> q = ( yR +s z ) ) )
143 142 rexbidv 
 |-  ( c = q -> ( E. yR e. ( _Right ` y ) c = ( yR +s z ) <-> E. yR e. ( _Right ` y ) q = ( yR +s z ) ) )
144 143 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 ) ) )
145 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 ) ) )
146 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 ) ) )
147 146 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 ) ) )
148 145 147 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 ) ) )
149 ovex 
 |-  ( yR +s z ) e. _V
150 breq1 
 |-  ( q = ( yR +s z ) -> ( q <_s ( x +s z ) <-> ( yR +s z ) <_s ( x +s z ) ) )
151 149 150 ceqsexv 
 |-  ( E. q ( q = ( yR +s z ) /\ q <_s ( x +s z ) ) <-> ( yR +s z ) <_s ( x +s z ) )
152 151 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 ) )
153 148 152 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 ) )
154 144 153 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 ) )
155 eqeq1 
 |-  ( d = q -> ( d = ( y +s zR ) <-> q = ( y +s zR ) ) )
156 155 rexbidv 
 |-  ( d = q -> ( E. zR e. ( _Right ` z ) d = ( y +s zR ) <-> E. zR e. ( _Right ` z ) q = ( y +s zR ) ) )
157 156 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 ) ) )
158 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 ) ) )
159 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 ) ) )
160 159 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 ) ) )
161 158 160 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 ) ) )
162 ovex 
 |-  ( y +s zR ) e. _V
163 breq1 
 |-  ( q = ( y +s zR ) -> ( q <_s ( x +s z ) <-> ( y +s zR ) <_s ( x +s z ) ) )
164 162 163 ceqsexv 
 |-  ( E. q ( q = ( y +s zR ) /\ q <_s ( x +s z ) ) <-> ( y +s zR ) <_s ( x +s z ) )
165 164 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 ) )
166 161 165 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 ) )
167 157 166 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 ) )
168 154 167 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 ) ) )
169 141 168 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 ) ) )
170 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 )
171 rightssno 
 |-  ( _Right ` y ) C_ No
172 171 sseli 
 |-  ( yR e. ( _Right ` y ) -> yR e. No )
173 172 adantr 
 |-  ( ( yR e. ( _Right ` y ) /\ ( yR +s z ) <_s ( x +s z ) ) -> yR e. No )
174 173 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 )
175 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 )
176 rightgt 
 |-  ( yR e. ( _Right ` y ) -> y
177 176 adantr 
 |-  ( ( yR e. ( _Right ` y ) /\ ( yR +s z ) <_s ( x +s z ) ) -> y
178 177 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
179 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 ) )
180 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 )
181 sleadd1im 
 |-  ( ( yR e. No /\ x e. No /\ z e. No ) -> ( ( yR +s z ) <_s ( x +s z ) -> yR <_s x ) )
182 174 175 180 181 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 ) )
183 179 182 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 )
184 170 174 175 178 183 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
185 184 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
186 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 )
187 rightssno 
 |-  ( _Right ` z ) C_ No
188 187 sseli 
 |-  ( zR e. ( _Right ` z ) -> zR e. No )
189 188 adantr 
 |-  ( ( zR e. ( _Right ` z ) /\ ( y +s zR ) <_s ( x +s z ) ) -> zR e. No )
190 189 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 )
191 186 190 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 )
192 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 )
193 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 )
194 192 193 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 )
195 192 190 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 )
196 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 ) )
197 193 190 192 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 ) )
198 rightgt 
 |-  ( zR e. ( _Right ` z ) -> z
199 198 adantr 
 |-  ( ( zR e. ( _Right ` z ) /\ ( y +s zR ) <_s ( x +s z ) ) -> z
200 199 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
201 sltadd2im 
 |-  ( ( z e. No /\ zR e. No /\ x e. No ) -> ( z  ( x +s z )
202 197 200 201 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 )
203 191 194 195 196 202 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 )
204 oveq2 
 |-  ( zO = zR -> ( y +s zO ) = ( y +s zR ) )
205 oveq2 
 |-  ( zO = zR -> ( x +s zO ) = ( x +s zR ) )
206 204 205 breq12d 
 |-  ( zO = zR -> ( ( y +s zO )  ( y +s zR )
207 206 imbi1d 
 |-  ( zO = zR -> ( ( ( y +s zO )  y  ( ( y +s zR )  y
208 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
209 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 ) )
210 elun2 
 |-  ( zR e. ( _Right ` z ) -> zR e. ( ( _Left ` z ) u. ( _Right ` z ) ) )
211 209 210 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 ) ) )
212 207 208 211 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
213 203 212 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
214 213 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
215 185 214 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
216 169 215 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
217 140 216 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
218 64 217 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
219 218 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
220 4 8 12 16 20 22 25 29 33 37 219 no3inds 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( B +s C )  B
221 addscl 
 |-  ( ( B e. No /\ C e. No ) -> ( B +s C ) e. No )
222 221 3adant1 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( B +s C ) e. No )
223 addscl 
 |-  ( ( A e. No /\ C e. No ) -> ( A +s C ) e. No )
224 223 3adant2 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( A +s C ) e. No )
225 sltnle 
 |-  ( ( ( B +s C ) e. No /\ ( A +s C ) e. No ) -> ( ( B +s C )  -. ( A +s C ) <_s ( B +s C ) ) )
226 222 224 225 syl2anc 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( B +s C )  -. ( A +s C ) <_s ( B +s C ) ) )
227 sltnle 
 |-  ( ( B e. No /\ A e. No ) -> ( B  -. A <_s B ) )
228 227 ancoms 
 |-  ( ( A e. No /\ B e. No ) -> ( B  -. A <_s B ) )
229 228 3adant3 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( B  -. A <_s B ) )
230 220 226 229 3imtr3d 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( -. ( A +s C ) <_s ( B +s C ) -> -. A <_s B ) )
231 230 con4d 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( A <_s B -> ( A +s C ) <_s ( B +s C ) ) )
232 sleadd1im 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( A +s C ) <_s ( B +s C ) -> A <_s B ) )
233 231 232 impbid 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( A <_s B <-> ( A +s C ) <_s ( B +s C ) ) )