Metamath Proof Explorer

Theorem leadds1

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 leadds1 
|- ( ( 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 addcuts 
 |-  ( ( 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 sltstr 
 |-  ( ( ( { 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 addcuts 
 |-  ( ( 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 sltstr 
 |-  ( ( ( { 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 ltsrecd 
 |-  ( ( 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 leftno 
 |-  ( xL e. ( _Left ` x ) -> xL e. No )
96 95 adantr 
 |-  ( ( xL e. ( _Left ` x ) /\ ( y +s z ) <_s ( xL +s z ) ) -> xL e. No )
97 96 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 )
98 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 )
99 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 ) )
100 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 )
101 leadds1im 
 |-  ( ( y e. No /\ xL e. No /\ z e. No ) -> ( ( y +s z ) <_s ( xL +s z ) -> y <_s xL ) )
102 94 97 100 101 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 ) )
103 99 102 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 )
104 leftlt 
 |-  ( xL e. ( _Left ` x ) -> xL
105 104 adantr 
 |-  ( ( xL e. ( _Left ` x ) /\ ( y +s z ) <_s ( xL +s z ) ) -> xL
106 105 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
107 94 97 98 103 106 leltstrd 
 |-  ( ( ( ( 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
108 107 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
109 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 )
110 leftno 
 |-  ( zL e. ( _Left ` z ) -> zL e. No )
111 110 adantr 
 |-  ( ( zL e. ( _Left ` z ) /\ ( y +s z ) <_s ( x +s zL ) ) -> zL e. No )
112 111 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 )
113 109 112 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 )
114 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 )
115 109 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 z ) e. No )
116 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 )
117 116 112 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 )
118 leftlt 
 |-  ( zL e. ( _Left ` z ) -> zL
119 118 adantr 
 |-  ( ( zL e. ( _Left ` z ) /\ ( y +s z ) <_s ( x +s zL ) ) -> zL
120 119 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
121 ltadds2im 
 |-  ( ( zL e. No /\ z e. No /\ y e. No ) -> ( zL  ( y +s zL )
122 112 114 109 121 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 )
123 120 122 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 )
124 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 ) )
125 113 115 117 123 124 ltlestrd 
 |-  ( ( ( ( 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 oveq2 
 |-  ( zO = zL -> ( y +s zO ) = ( y +s zL ) )
127 oveq2 
 |-  ( zO = zL -> ( x +s zO ) = ( x +s zL ) )
128 126 127 breq12d 
 |-  ( zO = zL -> ( ( y +s zO )  ( y +s zL )
129 128 imbi1d 
 |-  ( zO = zL -> ( ( ( y +s zO )  y  ( ( y +s zL )  y
130 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
131 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 ) )
132 elun1 
 |-  ( zL e. ( _Left ` z ) -> zL e. ( ( _Left ` z ) u. ( _Right ` z ) ) )
133 131 132 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 ) ) )
134 129 130 133 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
135 125 134 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
136 135 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
137 108 136 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
138 93 137 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
139 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 ) ) )
140 eqeq1 
 |-  ( c = q -> ( c = ( yR +s z ) <-> q = ( yR +s z ) ) )
141 140 rexbidv 
 |-  ( c = q -> ( E. yR e. ( _Right ` y ) c = ( yR +s z ) <-> E. yR e. ( _Right ` y ) q = ( yR +s z ) ) )
142 141 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 ) ) )
143 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 ) ) )
144 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 ) ) )
145 144 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 ) ) )
146 143 145 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 ) ) )
147 ovex 
 |-  ( yR +s z ) e. _V
148 breq1 
 |-  ( q = ( yR +s z ) -> ( q <_s ( x +s z ) <-> ( yR +s z ) <_s ( x +s z ) ) )
149 147 148 ceqsexv 
 |-  ( E. q ( q = ( yR +s z ) /\ q <_s ( x +s z ) ) <-> ( yR +s z ) <_s ( x +s z ) )
150 149 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 ) )
151 146 150 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 ) )
152 142 151 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 ) )
153 eqeq1 
 |-  ( d = q -> ( d = ( y +s zR ) <-> q = ( y +s zR ) ) )
154 153 rexbidv 
 |-  ( d = q -> ( E. zR e. ( _Right ` z ) d = ( y +s zR ) <-> E. zR e. ( _Right ` z ) q = ( y +s zR ) ) )
155 154 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 ) ) )
156 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 ) ) )
157 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 ) ) )
158 157 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 ) ) )
159 156 158 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 ) ) )
160 ovex 
 |-  ( y +s zR ) e. _V
161 breq1 
 |-  ( q = ( y +s zR ) -> ( q <_s ( x +s z ) <-> ( y +s zR ) <_s ( x +s z ) ) )
162 160 161 ceqsexv 
 |-  ( E. q ( q = ( y +s zR ) /\ q <_s ( x +s z ) ) <-> ( y +s zR ) <_s ( x +s z ) )
163 162 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 ) )
164 159 163 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 ) )
165 155 164 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 ) )
166 152 165 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 ) ) )
167 139 166 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 ) ) )
168 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 )
169 rightno 
 |-  ( yR e. ( _Right ` y ) -> yR e. No )
170 169 adantr 
 |-  ( ( yR e. ( _Right ` y ) /\ ( yR +s z ) <_s ( x +s z ) ) -> yR e. No )
171 170 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 )
172 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 )
173 rightgt 
 |-  ( yR e. ( _Right ` y ) -> y
174 173 adantr 
 |-  ( ( yR e. ( _Right ` y ) /\ ( yR +s z ) <_s ( x +s z ) ) -> y
175 174 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
176 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 ) )
177 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 )
178 leadds1im 
 |-  ( ( yR e. No /\ x e. No /\ z e. No ) -> ( ( yR +s z ) <_s ( x +s z ) -> yR <_s x ) )
179 171 172 177 178 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 ) )
180 176 179 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 )
181 168 171 172 175 180 ltlestrd 
 |-  ( ( ( ( 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
182 181 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
183 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 )
184 rightno 
 |-  ( zR e. ( _Right ` z ) -> zR e. No )
185 184 adantr 
 |-  ( ( zR e. ( _Right ` z ) /\ ( y +s zR ) <_s ( x +s z ) ) -> zR e. No )
186 185 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 )
187 183 186 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 )
188 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 )
189 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 )
190 188 189 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 )
191 188 186 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 )
192 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 ) )
193 189 186 188 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 ) )
194 rightgt 
 |-  ( zR e. ( _Right ` z ) -> z
195 194 adantr 
 |-  ( ( zR e. ( _Right ` z ) /\ ( y +s zR ) <_s ( x +s z ) ) -> z
196 195 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
197 ltadds2im 
 |-  ( ( z e. No /\ zR e. No /\ x e. No ) -> ( z  ( x +s z )
198 193 196 197 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 )
199 187 190 191 192 198 leltstrd 
 |-  ( ( ( ( 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 )
200 oveq2 
 |-  ( zO = zR -> ( y +s zO ) = ( y +s zR ) )
201 oveq2 
 |-  ( zO = zR -> ( x +s zO ) = ( x +s zR ) )
202 200 201 breq12d 
 |-  ( zO = zR -> ( ( y +s zO )  ( y +s zR )
203 202 imbi1d 
 |-  ( zO = zR -> ( ( ( y +s zO )  y  ( ( y +s zR )  y
204 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
205 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 ) )
206 elun2 
 |-  ( zR e. ( _Right ` z ) -> zR e. ( ( _Left ` z ) u. ( _Right ` z ) ) )
207 205 206 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 ) ) )
208 203 204 207 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
209 199 208 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
210 209 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
211 182 210 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
212 167 211 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
213 138 212 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
214 64 213 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
215 214 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
216 4 8 12 16 20 22 25 29 33 37 215 no3inds 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( B +s C )  B
217 addscl 
 |-  ( ( B e. No /\ C e. No ) -> ( B +s C ) e. No )
218 217 3adant1 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( B +s C ) e. No )
219 addscl 
 |-  ( ( A e. No /\ C e. No ) -> ( A +s C ) e. No )
220 219 3adant2 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( A +s C ) e. No )
221 ltnles 
 |-  ( ( ( B +s C ) e. No /\ ( A +s C ) e. No ) -> ( ( B +s C )  -. ( A +s C ) <_s ( B +s C ) ) )
222 218 220 221 syl2anc 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( B +s C )  -. ( A +s C ) <_s ( B +s C ) ) )
223 ltnles 
 |-  ( ( B e. No /\ A e. No ) -> ( B  -. A <_s B ) )
224 223 ancoms 
 |-  ( ( A e. No /\ B e. No ) -> ( B  -. A <_s B ) )
225 224 3adant3 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( B  -. A <_s B ) )
226 216 222 225 3imtr3d 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( -. ( A +s C ) <_s ( B +s C ) -> -. A <_s B ) )
227 226 con4d 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( A <_s B -> ( A +s C ) <_s ( B +s C ) ) )
228 leadds1im 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( A +s C ) <_s ( B +s C ) -> A <_s B ) )
229 227 228 impbid 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( A <_s B <-> ( A +s C ) <_s ( B +s C ) ) )