MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  leadds1 Structured version   Visualization version   GIF version
Theorem leadds1 27997
Description: Addition to both sides of surreal less-than or equal. Theorem 5 of [Conway] p. 18. (Contributed by Scott Fenton, 21-Jan-2025.)
Assertion
Ref Expression
leadds1 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 ≤s 𝐵 ↔ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶)))
Proof of Theorem leadds1
Dummy variables 𝑥 𝑦 𝑧 𝑎 𝑏 𝑐 𝑑 𝑝 𝑞 𝑥𝐿 𝑦𝐿 𝑧𝐿 𝑥𝑅 𝑦𝑅 𝑧𝑅 𝑥𝑂 𝑦𝑂 𝑧𝑂 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 7375 . . . . . . 7 (𝑥 = 𝑥𝑂 → (𝑥 +s 𝑧) = (𝑥𝑂 +s 𝑧))
21breq2d 5112 . . . . . 6 (𝑥 = 𝑥𝑂 → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧)))
3 breq2 5104 . . . . . 6 (𝑥 = 𝑥𝑂 → (𝑦 <s 𝑥 ↔ 𝑦 <s 𝑥𝑂))
42, 3imbi12d 344 . . . . 5 (𝑥 = 𝑥𝑂 → (((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦 <s 𝑥) ↔ ((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂)))
5 oveq1 7375 . . . . . . 7 (𝑦 = 𝑦𝑂 → (𝑦 +s 𝑧) = (𝑦𝑂 +s 𝑧))
65breq1d 5110 . . . . . 6 (𝑦 = 𝑦𝑂 → ((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) ↔ (𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧)))
7 breq1 5103 . . . . . 6 (𝑦 = 𝑦𝑂 → (𝑦 <s 𝑥𝑂 ↔ 𝑦𝑂 <s 𝑥𝑂))
86, 7imbi12d 344 . . . . 5 (𝑦 = 𝑦𝑂 → (((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ↔ ((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂)))
9 oveq2 7376 . . . . . . 7 (𝑧 = 𝑧𝑂 → (𝑦𝑂 +s 𝑧) = (𝑦𝑂 +s 𝑧𝑂))
10 oveq2 7376 . . . . . . 7 (𝑧 = 𝑧𝑂 → (𝑥𝑂 +s 𝑧) = (𝑥𝑂 +s 𝑧𝑂))
119, 10breq12d 5113 . . . . . 6 (𝑧 = 𝑧𝑂 → ((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) ↔ (𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂)))
1211imbi1d 341 . . . . 5 (𝑧 = 𝑧𝑂 → (((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ↔ ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂)))
13 oveq1 7375 . . . . . . 7 (𝑥 = 𝑥𝑂 → (𝑥 +s 𝑧𝑂) = (𝑥𝑂 +s 𝑧𝑂))
1413breq2d 5112 . . . . . 6 (𝑥 = 𝑥𝑂 → ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) ↔ (𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂)))
15 breq2 5104 . . . . . 6 (𝑥 = 𝑥𝑂 → (𝑦𝑂 <s 𝑥 ↔ 𝑦𝑂 <s 𝑥𝑂))
1614, 15imbi12d 344 . . . . 5 (𝑥 = 𝑥𝑂 → (((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ↔ ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂)))
17 oveq1 7375 . . . . . . 7 (𝑦 = 𝑦𝑂 → (𝑦 +s 𝑧𝑂) = (𝑦𝑂 +s 𝑧𝑂))
1817breq1d 5110 . . . . . 6 (𝑦 = 𝑦𝑂 → ((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) ↔ (𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂)))
19 breq1 5103 . . . . . 6 (𝑦 = 𝑦𝑂 → (𝑦 <s 𝑥 ↔ 𝑦𝑂 <s 𝑥))
2018, 19imbi12d 344 . . . . 5 (𝑦 = 𝑦𝑂 → (((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥) ↔ ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥)))
2117breq1d 5110 . . . . . 6 (𝑦 = 𝑦𝑂 → ((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) ↔ (𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂)))
2221, 7imbi12d 344 . . . . 5 (𝑦 = 𝑦𝑂 → (((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂) ↔ ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂)))
23 oveq2 7376 . . . . . . 7 (𝑧 = 𝑧𝑂 → (𝑥 +s 𝑧) = (𝑥 +s 𝑧𝑂))
249, 23breq12d 5113 . . . . . 6 (𝑧 = 𝑧𝑂 → ((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂)))
2524imbi1d 341 . . . . 5 (𝑧 = 𝑧𝑂 → (((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥) ↔ ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥)))
26 oveq1 7375 . . . . . . 7 (𝑥 = 𝐴 → (𝑥 +s 𝑧) = (𝐴 +s 𝑧))
2726breq2d 5112 . . . . . 6 (𝑥 = 𝐴 → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (𝑦 +s 𝑧) <s (𝐴 +s 𝑧)))
28 breq2 5104 . . . . . 6 (𝑥 = 𝐴 → (𝑦 <s 𝑥 ↔ 𝑦 <s 𝐴))
2927, 28imbi12d 344 . . . . 5 (𝑥 = 𝐴 → (((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦 <s 𝑥) ↔ ((𝑦 +s 𝑧) <s (𝐴 +s 𝑧) → 𝑦 <s 𝐴)))
30 oveq1 7375 . . . . . . 7 (𝑦 = 𝐵 → (𝑦 +s 𝑧) = (𝐵 +s 𝑧))
3130breq1d 5110 . . . . . 6 (𝑦 = 𝐵 → ((𝑦 +s 𝑧) <s (𝐴 +s 𝑧) ↔ (𝐵 +s 𝑧) <s (𝐴 +s 𝑧)))
32 breq1 5103 . . . . . 6 (𝑦 = 𝐵 → (𝑦 <s 𝐴 ↔ 𝐵 <s 𝐴))
3331, 32imbi12d 344 . . . . 5 (𝑦 = 𝐵 → (((𝑦 +s 𝑧) <s (𝐴 +s 𝑧) → 𝑦 <s 𝐴) ↔ ((𝐵 +s 𝑧) <s (𝐴 +s 𝑧) → 𝐵 <s 𝐴)))
34 oveq2 7376 . . . . . . 7 (𝑧 = 𝐶 → (𝐵 +s 𝑧) = (𝐵 +s 𝐶))
35 oveq2 7376 . . . . . . 7 (𝑧 = 𝐶 → (𝐴 +s 𝑧) = (𝐴 +s 𝐶))
3634, 35breq12d 5113 . . . . . 6 (𝑧 = 𝐶 → ((𝐵 +s 𝑧) <s (𝐴 +s 𝑧) ↔ (𝐵 +s 𝐶) <s (𝐴 +s 𝐶)))
3736imbi1d 341 . . . . 5 (𝑧 = 𝐶 → (((𝐵 +s 𝑧) <s (𝐴 +s 𝑧) → 𝐵 <s 𝐴) ↔ ((𝐵 +s 𝐶) <s (𝐴 +s 𝐶) → 𝐵 <s 𝐴)))
38 simp2 1138 . . . . . . . . . . . 12 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → 𝑦 ∈ No )
39 simp3 1139 . . . . . . . . . . . 12 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → 𝑧 ∈ No )
4038, 39addcuts 27986 . . . . . . . . . . 11 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ((𝑦 +s 𝑧) ∈ No ∧ ({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) <<s {(𝑦 +s 𝑧)} ∧ {(𝑦 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})))
41 simp2 1138 . . . . . . . . . . 11 (((𝑦 +s 𝑧) ∈ No ∧ ({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) <<s {(𝑦 +s 𝑧)} ∧ {(𝑦 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})) → ({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) <<s {(𝑦 +s 𝑧)})
4240, 41syl 17 . . . . . . . . . 10 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) <<s {(𝑦 +s 𝑧)})
4340simp3d 1145 . . . . . . . . . 10 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → {(𝑦 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}))
44 ovex 7401 . . . . . . . . . . . 12 (𝑦 +s 𝑧) ∈ V
4544snnz 4735 . . . . . . . . . . 11 {(𝑦 +s 𝑧)} ≠ ∅
46 sltstr 27795 . . . . . . . . . . 11 ((({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) <<s {(𝑦 +s 𝑧)} ∧ {(𝑦 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}) ∧ {(𝑦 +s 𝑧)} ≠ ∅) → ({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) <<s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}))
4745, 46mp3an3 1453 . . . . . . . . . 10 ((({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) <<s {(𝑦 +s 𝑧)} ∧ {(𝑦 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})) → ({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) <<s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}))
4842, 43, 47syl2anc 585 . . . . . . . . 9 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) <<s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}))
49 simp1 1137 . . . . . . . . . . . 12 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → 𝑥 ∈ No )
5049, 39addcuts 27986 . . . . . . . . . . 11 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ((𝑥 +s 𝑧) ∈ No ∧ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) <<s {(𝑥 +s 𝑧)} ∧ {(𝑥 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)})))
51 simp2 1138 . . . . . . . . . . 11 (((𝑥 +s 𝑧) ∈ No ∧ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) <<s {(𝑥 +s 𝑧)} ∧ {(𝑥 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)})) → ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) <<s {(𝑥 +s 𝑧)})
5250, 51syl 17 . . . . . . . . . 10 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) <<s {(𝑥 +s 𝑧)})
5350simp3d 1145 . . . . . . . . . 10 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → {(𝑥 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)}))
54 ovex 7401 . . . . . . . . . . . 12 (𝑥 +s 𝑧) ∈ V
5554snnz 4735 . . . . . . . . . . 11 {(𝑥 +s 𝑧)} ≠ ∅
56 sltstr 27795 . . . . . . . . . . 11 ((({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) <<s {(𝑥 +s 𝑧)} ∧ {(𝑥 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)}) ∧ {(𝑥 +s 𝑧)} ≠ ∅) → ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) <<s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)}))
5755, 56mp3an3 1453 . . . . . . . . . 10 ((({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) <<s {(𝑥 +s 𝑧)} ∧ {(𝑥 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)})) → ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) <<s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)}))
5852, 53, 57syl2anc 585 . . . . . . . . 9 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) <<s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)}))
59 addsval2 27971 . . . . . . . . . 10 ((𝑦 ∈ No ∧ 𝑧 ∈ No ) → (𝑦 +s 𝑧) = (({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) |s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})))
60593adant1 1131 . . . . . . . . 9 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → (𝑦 +s 𝑧) = (({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) |s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})))
61 addsval2 27971 . . . . . . . . . 10 ((𝑥 ∈ No ∧ 𝑧 ∈ No ) → (𝑥 +s 𝑧) = (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) |s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)})))
62613adant2 1132 . . . . . . . . 9 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → (𝑥 +s 𝑧) = (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) |s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)})))
6348, 58, 60, 62ltsrecd 27810 . . . . . . . 8 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (∃𝑝 ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)})(𝑦 +s 𝑧) ≤s 𝑝 ∨ ∃𝑞 ∈ ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})𝑞 ≤s (𝑥 +s 𝑧))))
6463adantr 480 . . . . . . 7 (((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (∃𝑝 ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)})(𝑦 +s 𝑧) ≤s 𝑝 ∨ ∃𝑞 ∈ ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})𝑞 ≤s (𝑥 +s 𝑧))))
65 rexun 4150 . . . . . . . . . 10 (∃𝑝 ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)})(𝑦 +s 𝑧) ≤s 𝑝 ↔ (∃𝑝 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} (𝑦 +s 𝑧) ≤s 𝑝 ∨ ∃𝑝 ∈ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)} (𝑦 +s 𝑧) ≤s 𝑝))
66 eqeq1 2741 . . . . . . . . . . . . . 14 (𝑎 = 𝑝 → (𝑎 = (𝑥𝐿 +s 𝑧) ↔ 𝑝 = (𝑥𝐿 +s 𝑧)))
6766rexbidv 3162 . . . . . . . . . . . . 13 (𝑎 = 𝑝 → (∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧) ↔ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑝 = (𝑥𝐿 +s 𝑧)))
6867rexab 3655 . . . . . . . . . . . 12 (∃𝑝 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} (𝑦 +s 𝑧) ≤s 𝑝 ↔ ∃𝑝(∃𝑥𝐿 ∈ ( L ‘𝑥)𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
69 rexcom4 3265 . . . . . . . . . . . . . 14 (∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑝(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
70 r19.41v 3168 . . . . . . . . . . . . . . 15 (∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ (∃𝑥𝐿 ∈ ( L ‘𝑥)𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
7170exbii 1850 . . . . . . . . . . . . . 14 (∃𝑝∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝(∃𝑥𝐿 ∈ ( L ‘𝑥)𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
7269, 71bitri 275 . . . . . . . . . . . . 13 (∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑝(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝(∃𝑥𝐿 ∈ ( L ‘𝑥)𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
73 ovex 7401 . . . . . . . . . . . . . . 15 (𝑥𝐿 +s 𝑧) ∈ V
74 breq2 5104 . . . . . . . . . . . . . . 15 (𝑝 = (𝑥𝐿 +s 𝑧) → ((𝑦 +s 𝑧) ≤s 𝑝 ↔ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧)))
7573, 74ceqsexv 3492 . . . . . . . . . . . . . 14 (∃𝑝(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))
7675rexbii 3085 . . . . . . . . . . . . 13 (∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑝(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))
7772, 76bitr3i 277 . . . . . . . . . . . 12 (∃𝑝(∃𝑥𝐿 ∈ ( L ‘𝑥)𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))
7868, 77bitri 275 . . . . . . . . . . 11 (∃𝑝 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} (𝑦 +s 𝑧) ≤s 𝑝 ↔ ∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))
79 eqeq1 2741 . . . . . . . . . . . . . 14 (𝑏 = 𝑝 → (𝑏 = (𝑥 +s 𝑧𝐿) ↔ 𝑝 = (𝑥 +s 𝑧𝐿)))
8079rexbidv 3162 . . . . . . . . . . . . 13 (𝑏 = 𝑝 → (∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿) ↔ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧𝐿)))
8180rexab 3655 . . . . . . . . . . . 12 (∃𝑝 ∈ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)} (𝑦 +s 𝑧) ≤s 𝑝 ↔ ∃𝑝(∃𝑧𝐿 ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
82 rexcom4 3265 . . . . . . . . . . . . . 14 (∃𝑧𝐿 ∈ ( L ‘𝑧)∃𝑝(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
83 r19.41v 3168 . . . . . . . . . . . . . . 15 (∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ (∃𝑧𝐿 ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
8483exbii 1850 . . . . . . . . . . . . . 14 (∃𝑝∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝(∃𝑧𝐿 ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
8582, 84bitri 275 . . . . . . . . . . . . 13 (∃𝑧𝐿 ∈ ( L ‘𝑧)∃𝑝(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝(∃𝑧𝐿 ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
86 ovex 7401 . . . . . . . . . . . . . . 15 (𝑥 +s 𝑧𝐿) ∈ V
87 breq2 5104 . . . . . . . . . . . . . . 15 (𝑝 = (𝑥 +s 𝑧𝐿) → ((𝑦 +s 𝑧) ≤s 𝑝 ↔ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿)))
8886, 87ceqsexv 3492 . . . . . . . . . . . . . 14 (∃𝑝(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))
8988rexbii 3085 . . . . . . . . . . . . 13 (∃𝑧𝐿 ∈ ( L ‘𝑧)∃𝑝(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))
9085, 89bitr3i 277 . . . . . . . . . . . 12 (∃𝑝(∃𝑧𝐿 ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))
9181, 90bitri 275 . . . . . . . . . . 11 (∃𝑝 ∈ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)} (𝑦 +s 𝑧) ≤s 𝑝 ↔ ∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))
9278, 91orbi12i 915 . . . . . . . . . 10 ((∃𝑝 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} (𝑦 +s 𝑧) ≤s 𝑝 ∨ ∃𝑝 ∈ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)} (𝑦 +s 𝑧) ≤s 𝑝) ↔ (∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧) ∨ ∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿)))
9365, 92bitri 275 . . . . . . . . 9 (∃𝑝 ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)})(𝑦 +s 𝑧) ≤s 𝑝 ↔ (∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧) ∨ ∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿)))
94 simpll2 1215 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))) → 𝑦 ∈ No )
95 leftno 27885 . . . . . . . . . . . . . 14 (𝑥𝐿 ∈ ( L ‘𝑥) → 𝑥𝐿 ∈ No )
9695adantr 480 . . . . . . . . . . . . 13 ((𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧)) → 𝑥𝐿 ∈ No )
9796adantl 481 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))) → 𝑥𝐿 ∈ No )
98 simpll1 1214 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))) → 𝑥 ∈ No )
99 simprr 773 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))) → (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))
100 simpll3 1216 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))) → 𝑧 ∈ No )
101 leadds1im 27995 . . . . . . . . . . . . . 14 ((𝑦 ∈ No ∧ 𝑥𝐿 ∈ No ∧ 𝑧 ∈ No ) → ((𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧) → 𝑦 ≤s 𝑥𝐿))
10294, 97, 100, 101syl3anc 1374 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))) → ((𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧) → 𝑦 ≤s 𝑥𝐿))
10399, 102mpd 15 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))) → 𝑦 ≤s 𝑥𝐿)
104 leftlt 27861 . . . . . . . . . . . . . 14 (𝑥𝐿 ∈ ( L ‘𝑥) → 𝑥𝐿 <s 𝑥)
105104adantr 480 . . . . . . . . . . . . 13 ((𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧)) → 𝑥𝐿 <s 𝑥)
106105adantl 481 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))) → 𝑥𝐿 <s 𝑥)
10794, 97, 98, 103, 106leltstrd 27745 . . . . . . . . . . 11 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))) → 𝑦 <s 𝑥)
108107rexlimdvaa 3140 . . . . . . . . . 10 (((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) → (∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧) → 𝑦 <s 𝑥))
109 simpll2 1215 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → 𝑦 ∈ No )
110 leftno 27885 . . . . . . . . . . . . . . . 16 (𝑧𝐿 ∈ ( L ‘𝑧) → 𝑧𝐿 ∈ No )
111110adantr 480 . . . . . . . . . . . . . . 15 ((𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿)) → 𝑧𝐿 ∈ No )
112111adantl 481 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → 𝑧𝐿 ∈ No )
113109, 112addscld 27988 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → (𝑦 +s 𝑧𝐿) ∈ No )
114 simpll3 1216 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → 𝑧 ∈ No )
115109, 114addscld 27988 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → (𝑦 +s 𝑧) ∈ No )
116 simpll1 1214 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → 𝑥 ∈ No )
117116, 112addscld 27988 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → (𝑥 +s 𝑧𝐿) ∈ No )
118 leftlt 27861 . . . . . . . . . . . . . . . 16 (𝑧𝐿 ∈ ( L ‘𝑧) → 𝑧𝐿 <s 𝑧)
119118adantr 480 . . . . . . . . . . . . . . 15 ((𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿)) → 𝑧𝐿 <s 𝑧)
120119adantl 481 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → 𝑧𝐿 <s 𝑧)
121 ltadds2im 27994 . . . . . . . . . . . . . . 15 ((𝑧𝐿 ∈ No ∧ 𝑧 ∈ No ∧ 𝑦 ∈ No ) → (𝑧𝐿 <s 𝑧 → (𝑦 +s 𝑧𝐿) <s (𝑦 +s 𝑧)))
122112, 114, 109, 121syl3anc 1374 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → (𝑧𝐿 <s 𝑧 → (𝑦 +s 𝑧𝐿) <s (𝑦 +s 𝑧)))
123120, 122mpd 15 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → (𝑦 +s 𝑧𝐿) <s (𝑦 +s 𝑧))
124 simprr 773 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))
125113, 115, 117, 123, 124ltlestrd 27744 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → (𝑦 +s 𝑧𝐿) <s (𝑥 +s 𝑧𝐿))
126 oveq2 7376 . . . . . . . . . . . . . . 15 (𝑧𝑂 = 𝑧𝐿 → (𝑦 +s 𝑧𝑂) = (𝑦 +s 𝑧𝐿))
127 oveq2 7376 . . . . . . . . . . . . . . 15 (𝑧𝑂 = 𝑧𝐿 → (𝑥 +s 𝑧𝑂) = (𝑥 +s 𝑧𝐿))
128126, 127breq12d 5113 . . . . . . . . . . . . . 14 (𝑧𝑂 = 𝑧𝐿 → ((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) ↔ (𝑦 +s 𝑧𝐿) <s (𝑥 +s 𝑧𝐿)))
129128imbi1d 341 . . . . . . . . . . . . 13 (𝑧𝑂 = 𝑧𝐿 → (((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥) ↔ ((𝑦 +s 𝑧𝐿) <s (𝑥 +s 𝑧𝐿) → 𝑦 <s 𝑥)))
130 simplr3 1219 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))
131 simprl 771 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → 𝑧𝐿 ∈ ( L ‘𝑧))
132 elun1 4136 . . . . . . . . . . . . . 14 (𝑧𝐿 ∈ ( L ‘𝑧) → 𝑧𝐿 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧)))
133131, 132syl 17 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → 𝑧𝐿 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧)))
134129, 130, 133rspcdva 3579 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → ((𝑦 +s 𝑧𝐿) <s (𝑥 +s 𝑧𝐿) → 𝑦 <s 𝑥))
135125, 134mpd 15 . . . . . . . . . . 11 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → 𝑦 <s 𝑥)
136135rexlimdvaa 3140 . . . . . . . . . 10 (((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) → (∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿) → 𝑦 <s 𝑥))
137108, 136jaod 860 . . . . . . . . 9 (((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) → ((∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧) ∨ ∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿)) → 𝑦 <s 𝑥))
13893, 137biimtrid 242 . . . . . . . 8 (((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) → (∃𝑝 ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)})(𝑦 +s 𝑧) ≤s 𝑝 → 𝑦 <s 𝑥))
139 rexun 4150 . . . . . . . . . 10 (∃𝑞 ∈ ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})𝑞 ≤s (𝑥 +s 𝑧) ↔ (∃𝑞 ∈ {𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)}𝑞 ≤s (𝑥 +s 𝑧) ∨ ∃𝑞 ∈ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}𝑞 ≤s (𝑥 +s 𝑧)))
140 eqeq1 2741 . . . . . . . . . . . . . 14 (𝑐 = 𝑞 → (𝑐 = (𝑦𝑅 +s 𝑧) ↔ 𝑞 = (𝑦𝑅 +s 𝑧)))
141140rexbidv 3162 . . . . . . . . . . . . 13 (𝑐 = 𝑞 → (∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧) ↔ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧)))
142141rexab 3655 . . . . . . . . . . . 12 (∃𝑞 ∈ {𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)}𝑞 ≤s (𝑥 +s 𝑧) ↔ ∃𝑞(∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
143 rexcom4 3265 . . . . . . . . . . . . . 14 (∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑞(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
144 r19.41v 3168 . . . . . . . . . . . . . . 15 (∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ (∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
145144exbii 1850 . . . . . . . . . . . . . 14 (∃𝑞∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞(∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
146143, 145bitri 275 . . . . . . . . . . . . 13 (∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑞(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞(∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
147 ovex 7401 . . . . . . . . . . . . . . 15 (𝑦𝑅 +s 𝑧) ∈ V
148 breq1 5103 . . . . . . . . . . . . . . 15 (𝑞 = (𝑦𝑅 +s 𝑧) → (𝑞 ≤s (𝑥 +s 𝑧) ↔ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧)))
149147, 148ceqsexv 3492 . . . . . . . . . . . . . 14 (∃𝑞(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))
150149rexbii 3085 . . . . . . . . . . . . 13 (∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑞(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))
151146, 150bitr3i 277 . . . . . . . . . . . 12 (∃𝑞(∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))
152142, 151bitri 275 . . . . . . . . . . 11 (∃𝑞 ∈ {𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)}𝑞 ≤s (𝑥 +s 𝑧) ↔ ∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))
153 eqeq1 2741 . . . . . . . . . . . . . 14 (𝑑 = 𝑞 → (𝑑 = (𝑦 +s 𝑧𝑅) ↔ 𝑞 = (𝑦 +s 𝑧𝑅)))
154153rexbidv 3162 . . . . . . . . . . . . 13 (𝑑 = 𝑞 → (∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅) ↔ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅)))
155154rexab 3655 . . . . . . . . . . . 12 (∃𝑞 ∈ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}𝑞 ≤s (𝑥 +s 𝑧) ↔ ∃𝑞(∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
156 rexcom4 3265 . . . . . . . . . . . . . 14 (∃𝑧𝑅 ∈ ( R ‘𝑧)∃𝑞(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
157 r19.41v 3168 . . . . . . . . . . . . . . 15 (∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ (∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
158157exbii 1850 . . . . . . . . . . . . . 14 (∃𝑞∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞(∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
159156, 158bitri 275 . . . . . . . . . . . . 13 (∃𝑧𝑅 ∈ ( R ‘𝑧)∃𝑞(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞(∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
160 ovex 7401 . . . . . . . . . . . . . . 15 (𝑦 +s 𝑧𝑅) ∈ V
161 breq1 5103 . . . . . . . . . . . . . . 15 (𝑞 = (𝑦 +s 𝑧𝑅) → (𝑞 ≤s (𝑥 +s 𝑧) ↔ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧)))
162160, 161ceqsexv 3492 . . . . . . . . . . . . . 14 (∃𝑞(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))
163162rexbii 3085 . . . . . . . . . . . . 13 (∃𝑧𝑅 ∈ ( R ‘𝑧)∃𝑞(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))
164159, 163bitr3i 277 . . . . . . . . . . . 12 (∃𝑞(∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))
165155, 164bitri 275 . . . . . . . . . . 11 (∃𝑞 ∈ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}𝑞 ≤s (𝑥 +s 𝑧) ↔ ∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))
166152, 165orbi12i 915 . . . . . . . . . 10 ((∃𝑞 ∈ {𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)}𝑞 ≤s (𝑥 +s 𝑧) ∨ ∃𝑞 ∈ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}𝑞 ≤s (𝑥 +s 𝑧)) ↔ (∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧) ∨ ∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧)))
167139, 166bitri 275 . . . . . . . . 9 (∃𝑞 ∈ ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})𝑞 ≤s (𝑥 +s 𝑧) ↔ (∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧) ∨ ∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧)))
168 simpll2 1215 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))) → 𝑦 ∈ No )
169 rightno 27886 . . . . . . . . . . . . . 14 (𝑦𝑅 ∈ ( R ‘𝑦) → 𝑦𝑅 ∈ No )
170169adantr 480 . . . . . . . . . . . . 13 ((𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧)) → 𝑦𝑅 ∈ No )
171170adantl 481 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))) → 𝑦𝑅 ∈ No )
172 simpll1 1214 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))) → 𝑥 ∈ No )
173 rightgt 27862 . . . . . . . . . . . . . 14 (𝑦𝑅 ∈ ( R ‘𝑦) → 𝑦 <s 𝑦𝑅)
174173adantr 480 . . . . . . . . . . . . 13 ((𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧)) → 𝑦 <s 𝑦𝑅)
175174adantl 481 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))) → 𝑦 <s 𝑦𝑅)
176 simprr 773 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))) → (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))
177 simpll3 1216 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))) → 𝑧 ∈ No )
178 leadds1im 27995 . . . . . . . . . . . . . 14 ((𝑦𝑅 ∈ No ∧ 𝑥 ∈ No ∧ 𝑧 ∈ No ) → ((𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧) → 𝑦𝑅 ≤s 𝑥))
179171, 172, 177, 178syl3anc 1374 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))) → ((𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧) → 𝑦𝑅 ≤s 𝑥))
180176, 179mpd 15 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))) → 𝑦𝑅 ≤s 𝑥)
181168, 171, 172, 175, 180ltlestrd 27744 . . . . . . . . . . 11 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))) → 𝑦 <s 𝑥)
182181rexlimdvaa 3140 . . . . . . . . . 10 (((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) → (∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧) → 𝑦 <s 𝑥))
183 simpll2 1215 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → 𝑦 ∈ No )
184 rightno 27886 . . . . . . . . . . . . . . . 16 (𝑧𝑅 ∈ ( R ‘𝑧) → 𝑧𝑅 ∈ No )
185184adantr 480 . . . . . . . . . . . . . . 15 ((𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧)) → 𝑧𝑅 ∈ No )
186185adantl 481 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → 𝑧𝑅 ∈ No )
187183, 186addscld 27988 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → (𝑦 +s 𝑧𝑅) ∈ No )
188 simpll1 1214 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → 𝑥 ∈ No )
189 simpll3 1216 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → 𝑧 ∈ No )
190188, 189addscld 27988 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → (𝑥 +s 𝑧) ∈ No )
191188, 186addscld 27988 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → (𝑥 +s 𝑧𝑅) ∈ No )
192 simprr 773 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))
193189, 186, 1883jca 1129 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → (𝑧 ∈ No ∧ 𝑧𝑅 ∈ No ∧ 𝑥 ∈ No ))
194 rightgt 27862 . . . . . . . . . . . . . . . 16 (𝑧𝑅 ∈ ( R ‘𝑧) → 𝑧 <s 𝑧𝑅)
195194adantr 480 . . . . . . . . . . . . . . 15 ((𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧)) → 𝑧 <s 𝑧𝑅)
196195adantl 481 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → 𝑧 <s 𝑧𝑅)
197 ltadds2im 27994 . . . . . . . . . . . . . 14 ((𝑧 ∈ No ∧ 𝑧𝑅 ∈ No ∧ 𝑥 ∈ No ) → (𝑧 <s 𝑧𝑅 → (𝑥 +s 𝑧) <s (𝑥 +s 𝑧𝑅)))
198193, 196, 197sylc 65 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → (𝑥 +s 𝑧) <s (𝑥 +s 𝑧𝑅))
199187, 190, 191, 192, 198leltstrd 27745 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → (𝑦 +s 𝑧𝑅) <s (𝑥 +s 𝑧𝑅))
200 oveq2 7376 . . . . . . . . . . . . . . 15 (𝑧𝑂 = 𝑧𝑅 → (𝑦 +s 𝑧𝑂) = (𝑦 +s 𝑧𝑅))
201 oveq2 7376 . . . . . . . . . . . . . . 15 (𝑧𝑂 = 𝑧𝑅 → (𝑥 +s 𝑧𝑂) = (𝑥 +s 𝑧𝑅))
202200, 201breq12d 5113 . . . . . . . . . . . . . 14 (𝑧𝑂 = 𝑧𝑅 → ((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) ↔ (𝑦 +s 𝑧𝑅) <s (𝑥 +s 𝑧𝑅)))
203202imbi1d 341 . . . . . . . . . . . . 13 (𝑧𝑂 = 𝑧𝑅 → (((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥) ↔ ((𝑦 +s 𝑧𝑅) <s (𝑥 +s 𝑧𝑅) → 𝑦 <s 𝑥)))
204 simplr3 1219 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))
205 simprl 771 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → 𝑧𝑅 ∈ ( R ‘𝑧))
206 elun2 4137 . . . . . . . . . . . . . 14 (𝑧𝑅 ∈ ( R ‘𝑧) → 𝑧𝑅 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧)))
207205, 206syl 17 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → 𝑧𝑅 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧)))
208203, 204, 207rspcdva 3579 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → ((𝑦 +s 𝑧𝑅) <s (𝑥 +s 𝑧𝑅) → 𝑦 <s 𝑥))
209199, 208mpd 15 . . . . . . . . . . 11 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → 𝑦 <s 𝑥)
210209rexlimdvaa 3140 . . . . . . . . . 10 (((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) → (∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧) → 𝑦 <s 𝑥))
211182, 210jaod 860 . . . . . . . . 9 (((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) → ((∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧) ∨ ∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧)) → 𝑦 <s 𝑥))
212167, 211biimtrid 242 . . . . . . . 8 (((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) → (∃𝑞 ∈ ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})𝑞 ≤s (𝑥 +s 𝑧) → 𝑦 <s 𝑥))
213138, 212jaod 860 . . . . . . 7 (((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) → ((∃𝑝 ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)})(𝑦 +s 𝑧) ≤s 𝑝 ∨ ∃𝑞 ∈ ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})𝑞 ≤s (𝑥 +s 𝑧)) → 𝑦 <s 𝑥))
21464, 213sylbid 240 . . . . . 6 (((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦 <s 𝑥))
215214ex 412 . . . . 5 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → (((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥)) → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦 <s 𝑥)))
2164, 8, 12, 16, 20, 22, 25, 29, 33, 37, 215no3inds 27966 . . . 4 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐵 +s 𝐶) <s (𝐴 +s 𝐶) → 𝐵 <s 𝐴))
217 addscl 27989 . . . . . 6 ((𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐵 +s 𝐶) ∈ No )
2182173adant1 1131 . . . . 5 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐵 +s 𝐶) ∈ No )
219 addscl 27989 . . . . . 6 ((𝐴 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 +s 𝐶) ∈ No )
2202193adant2 1132 . . . . 5 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 +s 𝐶) ∈ No )
221 ltnles 27733 . . . . 5 (((𝐵 +s 𝐶) ∈ No ∧ (𝐴 +s 𝐶) ∈ No ) → ((𝐵 +s 𝐶) <s (𝐴 +s 𝐶) ↔ ¬ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶)))
222218, 220, 221syl2anc 585 . . . 4 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐵 +s 𝐶) <s (𝐴 +s 𝐶) ↔ ¬ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶)))
223 ltnles 27733 . . . . . 6 ((𝐵 ∈ No ∧ 𝐴 ∈ No ) → (𝐵 <s 𝐴 ↔ ¬ 𝐴 ≤s 𝐵))
224223ancoms 458 . . . . 5 ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐵 <s 𝐴 ↔ ¬ 𝐴 ≤s 𝐵))
2252243adant3 1133 . . . 4 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐵 <s 𝐴 ↔ ¬ 𝐴 ≤s 𝐵))
226216, 222, 2253imtr3d 293 . . 3 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (¬ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶) → ¬ 𝐴 ≤s 𝐵))
227226con4d 115 . 2 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 ≤s 𝐵 → (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶)))
228 leadds1im 27995 . 2 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶) → 𝐴 ≤s 𝐵))
229227, 228impbid 212 1 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 ≤s 𝐵 ↔ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087   = wceq 1542  ∃wex 1781   ∈ wcel 2114  {cab 2715   ≠ wne 2933  ∀wral 3052  ∃wrex 3062   ∪ cun 3901  ∅c0 4287  {csn 4582   class class class wbr 5100  ‘cfv 6500  (class class class)co 7368   No csur 27619   <s clts 27620   ≤s cles 27724   <<s cslts 27765   |s ccuts 27767   L cleft 27833   R cright 27834   +s cadds 27967
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-tp 4587  df-op 4589  df-ot 4591  df-uni 4866  df-int 4905  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-se 5586  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-1st 7943  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-1o 8407  df-2o 8408  df-nadd 8604  df-no 27622  df-lts 27623  df-bday 27624  df-les 27725  df-slts 27766  df-cuts 27768  df-0s 27815  df-made 27835  df-old 27836  df-left 27838  df-right 27839  df-norec2 27957  df-adds 27968
This theorem is referenced by:  leadds2  27998  addscan2  28001  leadds1d  28003  nnsge1  28351  zsoring  28417
  Copyright terms: Public domain W3C validator