MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sleadd1 Structured version   Visualization version   GIF version
Theorem sleadd1 27953
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
sleadd1 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 ≤s 𝐵 ↔ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶)))
Proof of Theorem sleadd1
Dummy variables 𝑥 𝑦 𝑧 𝑎 𝑏 𝑐 𝑑 𝑝 𝑞 𝑥𝐿 𝑦𝐿 𝑧𝐿 𝑥𝑅 𝑦𝑅 𝑧𝑅 𝑥𝑂 𝑦𝑂 𝑧𝑂 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 7417 . . . . . . 7 (𝑥 = 𝑥𝑂 → (𝑥 +s 𝑧) = (𝑥𝑂 +s 𝑧))
21breq2d 5136 . . . . . 6 (𝑥 = 𝑥𝑂 → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧)))
3 breq2 5128 . . . . . 6 (𝑥 = 𝑥𝑂 → (𝑦 <s 𝑥 ↔ 𝑦 <s 𝑥𝑂))
42, 3imbi12d 344 . . . . 5 (𝑥 = 𝑥𝑂 → (((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦 <s 𝑥) ↔ ((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂)))
5 oveq1 7417 . . . . . . 7 (𝑦 = 𝑦𝑂 → (𝑦 +s 𝑧) = (𝑦𝑂 +s 𝑧))
65breq1d 5134 . . . . . 6 (𝑦 = 𝑦𝑂 → ((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) ↔ (𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧)))
7 breq1 5127 . . . . . 6 (𝑦 = 𝑦𝑂 → (𝑦 <s 𝑥𝑂 ↔ 𝑦𝑂 <s 𝑥𝑂))
86, 7imbi12d 344 . . . . 5 (𝑦 = 𝑦𝑂 → (((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ↔ ((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂)))
9 oveq2 7418 . . . . . . 7 (𝑧 = 𝑧𝑂 → (𝑦𝑂 +s 𝑧) = (𝑦𝑂 +s 𝑧𝑂))
10 oveq2 7418 . . . . . . 7 (𝑧 = 𝑧𝑂 → (𝑥𝑂 +s 𝑧) = (𝑥𝑂 +s 𝑧𝑂))
119, 10breq12d 5137 . . . . . 6 (𝑧 = 𝑧𝑂 → ((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) ↔ (𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂)))
1211imbi1d 341 . . . . 5 (𝑧 = 𝑧𝑂 → (((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ↔ ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂)))
13 oveq1 7417 . . . . . . 7 (𝑥 = 𝑥𝑂 → (𝑥 +s 𝑧𝑂) = (𝑥𝑂 +s 𝑧𝑂))
1413breq2d 5136 . . . . . 6 (𝑥 = 𝑥𝑂 → ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) ↔ (𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂)))
15 breq2 5128 . . . . . 6 (𝑥 = 𝑥𝑂 → (𝑦𝑂 <s 𝑥 ↔ 𝑦𝑂 <s 𝑥𝑂))
1614, 15imbi12d 344 . . . . 5 (𝑥 = 𝑥𝑂 → (((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ↔ ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂)))
17 oveq1 7417 . . . . . . 7 (𝑦 = 𝑦𝑂 → (𝑦 +s 𝑧𝑂) = (𝑦𝑂 +s 𝑧𝑂))
1817breq1d 5134 . . . . . 6 (𝑦 = 𝑦𝑂 → ((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) ↔ (𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂)))
19 breq1 5127 . . . . . 6 (𝑦 = 𝑦𝑂 → (𝑦 <s 𝑥 ↔ 𝑦𝑂 <s 𝑥))
2018, 19imbi12d 344 . . . . 5 (𝑦 = 𝑦𝑂 → (((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥) ↔ ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥)))
2117breq1d 5134 . . . . . 6 (𝑦 = 𝑦𝑂 → ((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) ↔ (𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂)))
2221, 7imbi12d 344 . . . . 5 (𝑦 = 𝑦𝑂 → (((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂) ↔ ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂)))
23 oveq2 7418 . . . . . . 7 (𝑧 = 𝑧𝑂 → (𝑥 +s 𝑧) = (𝑥 +s 𝑧𝑂))
249, 23breq12d 5137 . . . . . 6 (𝑧 = 𝑧𝑂 → ((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂)))
2524imbi1d 341 . . . . 5 (𝑧 = 𝑧𝑂 → (((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥) ↔ ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥)))
26 oveq1 7417 . . . . . . 7 (𝑥 = 𝐴 → (𝑥 +s 𝑧) = (𝐴 +s 𝑧))
2726breq2d 5136 . . . . . 6 (𝑥 = 𝐴 → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (𝑦 +s 𝑧) <s (𝐴 +s 𝑧)))
28 breq2 5128 . . . . . 6 (𝑥 = 𝐴 → (𝑦 <s 𝑥 ↔ 𝑦 <s 𝐴))
2927, 28imbi12d 344 . . . . 5 (𝑥 = 𝐴 → (((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦 <s 𝑥) ↔ ((𝑦 +s 𝑧) <s (𝐴 +s 𝑧) → 𝑦 <s 𝐴)))
30 oveq1 7417 . . . . . . 7 (𝑦 = 𝐵 → (𝑦 +s 𝑧) = (𝐵 +s 𝑧))
3130breq1d 5134 . . . . . 6 (𝑦 = 𝐵 → ((𝑦 +s 𝑧) <s (𝐴 +s 𝑧) ↔ (𝐵 +s 𝑧) <s (𝐴 +s 𝑧)))
32 breq1 5127 . . . . . 6 (𝑦 = 𝐵 → (𝑦 <s 𝐴 ↔ 𝐵 <s 𝐴))
3331, 32imbi12d 344 . . . . 5 (𝑦 = 𝐵 → (((𝑦 +s 𝑧) <s (𝐴 +s 𝑧) → 𝑦 <s 𝐴) ↔ ((𝐵 +s 𝑧) <s (𝐴 +s 𝑧) → 𝐵 <s 𝐴)))
34 oveq2 7418 . . . . . . 7 (𝑧 = 𝐶 → (𝐵 +s 𝑧) = (𝐵 +s 𝐶))
35 oveq2 7418 . . . . . . 7 (𝑧 = 𝐶 → (𝐴 +s 𝑧) = (𝐴 +s 𝐶))
3634, 35breq12d 5137 . . . . . 6 (𝑧 = 𝐶 → ((𝐵 +s 𝑧) <s (𝐴 +s 𝑧) ↔ (𝐵 +s 𝐶) <s (𝐴 +s 𝐶)))
3736imbi1d 341 . . . . 5 (𝑧 = 𝐶 → (((𝐵 +s 𝑧) <s (𝐴 +s 𝑧) → 𝐵 <s 𝐴) ↔ ((𝐵 +s 𝐶) <s (𝐴 +s 𝐶) → 𝐵 <s 𝐴)))
38 simp2 1137 . . . . . . . . . . . 12 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → 𝑦 ∈ No )
39 simp3 1138 . . . . . . . . . . . 12 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → 𝑧 ∈ No )
4038, 39addscut 27942 . . . . . . . . . . 11 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ((𝑦 +s 𝑧) ∈ No ∧ ({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) <<s {(𝑦 +s 𝑧)} ∧ {(𝑦 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})))
41 simp2 1137 . . . . . . . . . . 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 1144 . . . . . . . . . 10 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → {(𝑦 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}))
44 ovex 7443 . . . . . . . . . . . 12 (𝑦 +s 𝑧) ∈ V
4544snnz 4757 . . . . . . . . . . 11 {(𝑦 +s 𝑧)} ≠ ∅
46 sslttr 27776 . . . . . . . . . . 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 1452 . . . . . . . . . 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 584 . . . . . . . . 9 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) <<s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}))
49 simp1 1136 . . . . . . . . . . . 12 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → 𝑥 ∈ No )
5049, 39addscut 27942 . . . . . . . . . . 11 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ((𝑥 +s 𝑧) ∈ No ∧ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) <<s {(𝑥 +s 𝑧)} ∧ {(𝑥 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)})))
51 simp2 1137 . . . . . . . . . . 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 1144 . . . . . . . . . 10 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → {(𝑥 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)}))
54 ovex 7443 . . . . . . . . . . . 12 (𝑥 +s 𝑧) ∈ V
5554snnz 4757 . . . . . . . . . . 11 {(𝑥 +s 𝑧)} ≠ ∅
56 sslttr 27776 . . . . . . . . . . 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 1452 . . . . . . . . . 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 584 . . . . . . . . 9 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) <<s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)}))
59 addsval2 27927 . . . . . . . . . 10 ((𝑦 ∈ No ∧ 𝑧 ∈ No ) → (𝑦 +s 𝑧) = (({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) |s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})))
60593adant1 1130 . . . . . . . . 9 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → (𝑦 +s 𝑧) = (({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) |s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})))
61 addsval2 27927 . . . . . . . . . 10 ((𝑥 ∈ No ∧ 𝑧 ∈ No ) → (𝑥 +s 𝑧) = (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) |s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)})))
62613adant2 1131 . . . . . . . . 9 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → (𝑥 +s 𝑧) = (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) |s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)})))
63 sltrec 27789 . . . . . . . . 9 (((({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) <<s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}) ∧ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) <<s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)})) ∧ ((𝑦 +s 𝑧) = (({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) |s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})) ∧ (𝑥 +s 𝑧) = (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) |s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)})))) → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (∃𝑝 ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)})(𝑦 +s 𝑧) ≤s 𝑝 ∨ ∃𝑞 ∈ ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})𝑞 ≤s (𝑥 +s 𝑧))))
6448, 58, 60, 62, 63syl22anc 838 . . . . . . . 8 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (∃𝑝 ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)})(𝑦 +s 𝑧) ≤s 𝑝 ∨ ∃𝑞 ∈ ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})𝑞 ≤s (𝑥 +s 𝑧))))
6564adantr 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 𝑧))))
66 rexun 4176 . . . . . . . . . 10 (∃𝑝 ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)})(𝑦 +s 𝑧) ≤s 𝑝 ↔ (∃𝑝 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} (𝑦 +s 𝑧) ≤s 𝑝 ∨ ∃𝑝 ∈ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)} (𝑦 +s 𝑧) ≤s 𝑝))
67 eqeq1 2740 . . . . . . . . . . . . . 14 (𝑎 = 𝑝 → (𝑎 = (𝑥𝐿 +s 𝑧) ↔ 𝑝 = (𝑥𝐿 +s 𝑧)))
6867rexbidv 3165 . . . . . . . . . . . . 13 (𝑎 = 𝑝 → (∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧) ↔ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑝 = (𝑥𝐿 +s 𝑧)))
6968rexab 3683 . . . . . . . . . . . 12 (∃𝑝 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} (𝑦 +s 𝑧) ≤s 𝑝 ↔ ∃𝑝(∃𝑥𝐿 ∈ ( L ‘𝑥)𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
70 rexcom4 3273 . . . . . . . . . . . . . 14 (∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑝(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
71 r19.41v 3175 . . . . . . . . . . . . . . 15 (∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ (∃𝑥𝐿 ∈ ( L ‘𝑥)𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
7271exbii 1848 . . . . . . . . . . . . . 14 (∃𝑝∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝(∃𝑥𝐿 ∈ ( L ‘𝑥)𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
7370, 72bitri 275 . . . . . . . . . . . . 13 (∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑝(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝(∃𝑥𝐿 ∈ ( L ‘𝑥)𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
74 ovex 7443 . . . . . . . . . . . . . . 15 (𝑥𝐿 +s 𝑧) ∈ V
75 breq2 5128 . . . . . . . . . . . . . . 15 (𝑝 = (𝑥𝐿 +s 𝑧) → ((𝑦 +s 𝑧) ≤s 𝑝 ↔ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧)))
7674, 75ceqsexv 3516 . . . . . . . . . . . . . 14 (∃𝑝(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))
7776rexbii 3084 . . . . . . . . . . . . 13 (∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑝(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))
7873, 77bitr3i 277 . . . . . . . . . . . 12 (∃𝑝(∃𝑥𝐿 ∈ ( L ‘𝑥)𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))
7969, 78bitri 275 . . . . . . . . . . 11 (∃𝑝 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} (𝑦 +s 𝑧) ≤s 𝑝 ↔ ∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))
80 eqeq1 2740 . . . . . . . . . . . . . 14 (𝑏 = 𝑝 → (𝑏 = (𝑥 +s 𝑧𝐿) ↔ 𝑝 = (𝑥 +s 𝑧𝐿)))
8180rexbidv 3165 . . . . . . . . . . . . 13 (𝑏 = 𝑝 → (∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿) ↔ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧𝐿)))
8281rexab 3683 . . . . . . . . . . . 12 (∃𝑝 ∈ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)} (𝑦 +s 𝑧) ≤s 𝑝 ↔ ∃𝑝(∃𝑧𝐿 ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
83 rexcom4 3273 . . . . . . . . . . . . . 14 (∃𝑧𝐿 ∈ ( L ‘𝑧)∃𝑝(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
84 r19.41v 3175 . . . . . . . . . . . . . . 15 (∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ (∃𝑧𝐿 ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
8584exbii 1848 . . . . . . . . . . . . . 14 (∃𝑝∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝(∃𝑧𝐿 ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
8683, 85bitri 275 . . . . . . . . . . . . 13 (∃𝑧𝐿 ∈ ( L ‘𝑧)∃𝑝(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝(∃𝑧𝐿 ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
87 ovex 7443 . . . . . . . . . . . . . . 15 (𝑥 +s 𝑧𝐿) ∈ V
88 breq2 5128 . . . . . . . . . . . . . . 15 (𝑝 = (𝑥 +s 𝑧𝐿) → ((𝑦 +s 𝑧) ≤s 𝑝 ↔ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿)))
8987, 88ceqsexv 3516 . . . . . . . . . . . . . 14 (∃𝑝(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))
9089rexbii 3084 . . . . . . . . . . . . 13 (∃𝑧𝐿 ∈ ( L ‘𝑧)∃𝑝(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))
9186, 90bitr3i 277 . . . . . . . . . . . 12 (∃𝑝(∃𝑧𝐿 ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))
9282, 91bitri 275 . . . . . . . . . . 11 (∃𝑝 ∈ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)} (𝑦 +s 𝑧) ≤s 𝑝 ↔ ∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))
9379, 92orbi12i 914 . . . . . . . . . 10 ((∃𝑝 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} (𝑦 +s 𝑧) ≤s 𝑝 ∨ ∃𝑝 ∈ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)} (𝑦 +s 𝑧) ≤s 𝑝) ↔ (∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧) ∨ ∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿)))
9466, 93bitri 275 . . . . . . . . 9 (∃𝑝 ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)})(𝑦 +s 𝑧) ≤s 𝑝 ↔ (∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧) ∨ ∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿)))
95 simpll2 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 )
96 leftssno 27849 . . . . . . . . . . . . . . 15 ( L ‘𝑥) ⊆ No
9796sseli 3959 . . . . . . . . . . . . . 14 (𝑥𝐿 ∈ ( L ‘𝑥) → 𝑥𝐿 ∈ No )
9897adantr 480 . . . . . . . . . . . . 13 ((𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧)) → 𝑥𝐿 ∈ No )
9998adantl 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 )
100 simpll1 1213 . . . . . . . . . . . 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 )
101 simprr 772 . . . . . . . . . . . . 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 𝑧))
102 simpll3 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 )
103 sleadd1im 27951 . . . . . . . . . . . . . 14 ((𝑦 ∈ No ∧ 𝑥𝐿 ∈ No ∧ 𝑧 ∈ No ) → ((𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧) → 𝑦 ≤s 𝑥𝐿))
10495, 99, 102, 103syl3anc 1373 . . . . . . . . . . . . 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 𝑥𝐿))
105101, 104mpd 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 𝑥𝐿)
106 leftlt 27832 . . . . . . . . . . . . . 14 (𝑥𝐿 ∈ ( L ‘𝑥) → 𝑥𝐿 <s 𝑥)
107106adantr 480 . . . . . . . . . . . . 13 ((𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧)) → 𝑥𝐿 <s 𝑥)
108107adantl 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 𝑥)
10995, 99, 100, 105, 108slelttrd 27730 . . . . . . . . . . 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 𝑥)
110109rexlimdvaa 3143 . . . . . . . . . 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 𝑥))
111 simpll2 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 )
112 leftssno 27849 . . . . . . . . . . . . . . . . 17 ( L ‘𝑧) ⊆ No
113112sseli 3959 . . . . . . . . . . . . . . . 16 (𝑧𝐿 ∈ ( L ‘𝑧) → 𝑧𝐿 ∈ No )
114113adantr 480 . . . . . . . . . . . . . . 15 ((𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿)) → 𝑧𝐿 ∈ No )
115114adantl 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 )
116111, 115addscld 27944 . . . . . . . . . . . . 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 )
117 simpll3 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 )
118111, 117addscld 27944 . . . . . . . . . . . . 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 )
119 simpll1 1213 . . . . . . . . . . . . . 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 )
120119, 115addscld 27944 . . . . . . . . . . . . 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 )
121 leftlt 27832 . . . . . . . . . . . . . . . 16 (𝑧𝐿 ∈ ( L ‘𝑧) → 𝑧𝐿 <s 𝑧)
122121adantr 480 . . . . . . . . . . . . . . 15 ((𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿)) → 𝑧𝐿 <s 𝑧)
123122adantl 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 𝑧)
124 sltadd2im 27950 . . . . . . . . . . . . . . 15 ((𝑧𝐿 ∈ No ∧ 𝑧 ∈ No ∧ 𝑦 ∈ No ) → (𝑧𝐿 <s 𝑧 → (𝑦 +s 𝑧𝐿) <s (𝑦 +s 𝑧)))
125115, 117, 111, 124syl3anc 1373 . . . . . . . . . . . . . 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 𝑧)))
126123, 125mpd 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 𝑧))
127 simprr 772 . . . . . . . . . . . . 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 𝑧𝐿))
128116, 118, 120, 126, 127sltletrd 27729 . . . . . . . . . . . 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 𝑧𝐿))
129 oveq2 7418 . . . . . . . . . . . . . . 15 (𝑧𝑂 = 𝑧𝐿 → (𝑦 +s 𝑧𝑂) = (𝑦 +s 𝑧𝐿))
130 oveq2 7418 . . . . . . . . . . . . . . 15 (𝑧𝑂 = 𝑧𝐿 → (𝑥 +s 𝑧𝑂) = (𝑥 +s 𝑧𝐿))
131129, 130breq12d 5137 . . . . . . . . . . . . . 14 (𝑧𝑂 = 𝑧𝐿 → ((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) ↔ (𝑦 +s 𝑧𝐿) <s (𝑥 +s 𝑧𝐿)))
132131imbi1d 341 . . . . . . . . . . . . 13 (𝑧𝑂 = 𝑧𝐿 → (((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥) ↔ ((𝑦 +s 𝑧𝐿) <s (𝑥 +s 𝑧𝐿) → 𝑦 <s 𝑥)))
133 simplr3 1218 . . . . . . . . . . . . 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 𝑥))
134 simprl 770 . . . . . . . . . . . . . 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 ‘𝑧))
135 elun1 4162 . . . . . . . . . . . . . 14 (𝑧𝐿 ∈ ( L ‘𝑧) → 𝑧𝐿 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧)))
136134, 135syl 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 ‘𝑧)))
137132, 133, 136rspcdva 3607 . . . . . . . . . . . 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 𝑥))
138128, 137mpd 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 𝑥)
139138rexlimdvaa 3143 . . . . . . . . . 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 𝑥))
140110, 139jaod 859 . . . . . . . . 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 𝑥))
14194, 140biimtrid 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 𝑥))
142 rexun 4176 . . . . . . . . . 10 (∃𝑞 ∈ ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})𝑞 ≤s (𝑥 +s 𝑧) ↔ (∃𝑞 ∈ {𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)}𝑞 ≤s (𝑥 +s 𝑧) ∨ ∃𝑞 ∈ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}𝑞 ≤s (𝑥 +s 𝑧)))
143 eqeq1 2740 . . . . . . . . . . . . . 14 (𝑐 = 𝑞 → (𝑐 = (𝑦𝑅 +s 𝑧) ↔ 𝑞 = (𝑦𝑅 +s 𝑧)))
144143rexbidv 3165 . . . . . . . . . . . . 13 (𝑐 = 𝑞 → (∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧) ↔ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧)))
145144rexab 3683 . . . . . . . . . . . 12 (∃𝑞 ∈ {𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)}𝑞 ≤s (𝑥 +s 𝑧) ↔ ∃𝑞(∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
146 rexcom4 3273 . . . . . . . . . . . . . 14 (∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑞(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
147 r19.41v 3175 . . . . . . . . . . . . . . 15 (∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ (∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
148147exbii 1848 . . . . . . . . . . . . . 14 (∃𝑞∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞(∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
149146, 148bitri 275 . . . . . . . . . . . . 13 (∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑞(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞(∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
150 ovex 7443 . . . . . . . . . . . . . . 15 (𝑦𝑅 +s 𝑧) ∈ V
151 breq1 5127 . . . . . . . . . . . . . . 15 (𝑞 = (𝑦𝑅 +s 𝑧) → (𝑞 ≤s (𝑥 +s 𝑧) ↔ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧)))
152150, 151ceqsexv 3516 . . . . . . . . . . . . . 14 (∃𝑞(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))
153152rexbii 3084 . . . . . . . . . . . . 13 (∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑞(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))
154149, 153bitr3i 277 . . . . . . . . . . . 12 (∃𝑞(∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))
155145, 154bitri 275 . . . . . . . . . . 11 (∃𝑞 ∈ {𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)}𝑞 ≤s (𝑥 +s 𝑧) ↔ ∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))
156 eqeq1 2740 . . . . . . . . . . . . . 14 (𝑑 = 𝑞 → (𝑑 = (𝑦 +s 𝑧𝑅) ↔ 𝑞 = (𝑦 +s 𝑧𝑅)))
157156rexbidv 3165 . . . . . . . . . . . . 13 (𝑑 = 𝑞 → (∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅) ↔ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅)))
158157rexab 3683 . . . . . . . . . . . 12 (∃𝑞 ∈ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}𝑞 ≤s (𝑥 +s 𝑧) ↔ ∃𝑞(∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
159 rexcom4 3273 . . . . . . . . . . . . . 14 (∃𝑧𝑅 ∈ ( R ‘𝑧)∃𝑞(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
160 r19.41v 3175 . . . . . . . . . . . . . . 15 (∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ (∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
161160exbii 1848 . . . . . . . . . . . . . 14 (∃𝑞∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞(∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
162159, 161bitri 275 . . . . . . . . . . . . 13 (∃𝑧𝑅 ∈ ( R ‘𝑧)∃𝑞(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞(∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
163 ovex 7443 . . . . . . . . . . . . . . 15 (𝑦 +s 𝑧𝑅) ∈ V
164 breq1 5127 . . . . . . . . . . . . . . 15 (𝑞 = (𝑦 +s 𝑧𝑅) → (𝑞 ≤s (𝑥 +s 𝑧) ↔ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧)))
165163, 164ceqsexv 3516 . . . . . . . . . . . . . 14 (∃𝑞(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))
166165rexbii 3084 . . . . . . . . . . . . 13 (∃𝑧𝑅 ∈ ( R ‘𝑧)∃𝑞(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))
167162, 166bitr3i 277 . . . . . . . . . . . 12 (∃𝑞(∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))
168158, 167bitri 275 . . . . . . . . . . 11 (∃𝑞 ∈ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}𝑞 ≤s (𝑥 +s 𝑧) ↔ ∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))
169155, 168orbi12i 914 . . . . . . . . . 10 ((∃𝑞 ∈ {𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)}𝑞 ≤s (𝑥 +s 𝑧) ∨ ∃𝑞 ∈ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}𝑞 ≤s (𝑥 +s 𝑧)) ↔ (∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧) ∨ ∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧)))
170142, 169bitri 275 . . . . . . . . 9 (∃𝑞 ∈ ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})𝑞 ≤s (𝑥 +s 𝑧) ↔ (∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧) ∨ ∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧)))
171 simpll2 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 )
172 rightssno 27850 . . . . . . . . . . . . . . 15 ( R ‘𝑦) ⊆ No
173172sseli 3959 . . . . . . . . . . . . . 14 (𝑦𝑅 ∈ ( R ‘𝑦) → 𝑦𝑅 ∈ No )
174173adantr 480 . . . . . . . . . . . . 13 ((𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧)) → 𝑦𝑅 ∈ No )
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 𝑧))) → 𝑦𝑅 ∈ No )
176 simpll1 1213 . . . . . . . . . . . 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 )
177 rightgt 27833 . . . . . . . . . . . . . 14 (𝑦𝑅 ∈ ( R ‘𝑦) → 𝑦 <s 𝑦𝑅)
178177adantr 480 . . . . . . . . . . . . 13 ((𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧)) → 𝑦 <s 𝑦𝑅)
179178adantl 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 𝑦𝑅)
180 simprr 772 . . . . . . . . . . . . 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 𝑧))
181 simpll3 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 )
182 sleadd1im 27951 . . . . . . . . . . . . . 14 ((𝑦𝑅 ∈ No ∧ 𝑥 ∈ No ∧ 𝑧 ∈ No ) → ((𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧) → 𝑦𝑅 ≤s 𝑥))
183175, 176, 181, 182syl3anc 1373 . . . . . . . . . . . . 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 𝑥))
184180, 183mpd 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 𝑥)
185171, 175, 176, 179, 184sltletrd 27729 . . . . . . . . . . 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 𝑥)
186185rexlimdvaa 3143 . . . . . . . . . 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 𝑥))
187 simpll2 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 )
188 rightssno 27850 . . . . . . . . . . . . . . . . 17 ( R ‘𝑧) ⊆ No
189188sseli 3959 . . . . . . . . . . . . . . . 16 (𝑧𝑅 ∈ ( R ‘𝑧) → 𝑧𝑅 ∈ No )
190189adantr 480 . . . . . . . . . . . . . . 15 ((𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧)) → 𝑧𝑅 ∈ No )
191190adantl 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 )
192187, 191addscld 27944 . . . . . . . . . . . . 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 )
193 simpll1 1213 . . . . . . . . . . . . . 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 )
194 simpll3 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 )
195193, 194addscld 27944 . . . . . . . . . . . . 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 )
196193, 191addscld 27944 . . . . . . . . . . . . 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 )
197 simprr 772 . . . . . . . . . . . . 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 𝑧))
198194, 191, 1933jca 1128 . . . . . . . . . . . . . 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 ))
199 rightgt 27833 . . . . . . . . . . . . . . . 16 (𝑧𝑅 ∈ ( R ‘𝑧) → 𝑧 <s 𝑧𝑅)
200199adantr 480 . . . . . . . . . . . . . . 15 ((𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧)) → 𝑧 <s 𝑧𝑅)
201200adantl 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 𝑧𝑅)
202 sltadd2im 27950 . . . . . . . . . . . . . 14 ((𝑧 ∈ No ∧ 𝑧𝑅 ∈ No ∧ 𝑥 ∈ No ) → (𝑧 <s 𝑧𝑅 → (𝑥 +s 𝑧) <s (𝑥 +s 𝑧𝑅)))
203198, 201, 202sylc 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 𝑧𝑅))
204192, 195, 196, 197, 203slelttrd 27730 . . . . . . . . . . . 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 𝑧𝑅))
205 oveq2 7418 . . . . . . . . . . . . . . 15 (𝑧𝑂 = 𝑧𝑅 → (𝑦 +s 𝑧𝑂) = (𝑦 +s 𝑧𝑅))
206 oveq2 7418 . . . . . . . . . . . . . . 15 (𝑧𝑂 = 𝑧𝑅 → (𝑥 +s 𝑧𝑂) = (𝑥 +s 𝑧𝑅))
207205, 206breq12d 5137 . . . . . . . . . . . . . 14 (𝑧𝑂 = 𝑧𝑅 → ((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) ↔ (𝑦 +s 𝑧𝑅) <s (𝑥 +s 𝑧𝑅)))
208207imbi1d 341 . . . . . . . . . . . . 13 (𝑧𝑂 = 𝑧𝑅 → (((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥) ↔ ((𝑦 +s 𝑧𝑅) <s (𝑥 +s 𝑧𝑅) → 𝑦 <s 𝑥)))
209 simplr3 1218 . . . . . . . . . . . . 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 𝑥))
210 simprl 770 . . . . . . . . . . . . . 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 ‘𝑧))
211 elun2 4163 . . . . . . . . . . . . . 14 (𝑧𝑅 ∈ ( R ‘𝑧) → 𝑧𝑅 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧)))
212210, 211syl 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 ‘𝑧)))
213208, 209, 212rspcdva 3607 . . . . . . . . . . . 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 𝑥))
214204, 213mpd 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 𝑥)
215214rexlimdvaa 3143 . . . . . . . . . 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 𝑥))
216186, 215jaod 859 . . . . . . . . 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 𝑥))
217170, 216biimtrid 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 𝑥))
218141, 217jaod 859 . . . . . . 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 𝑥))
21965, 218sylbid 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 𝑥))
220219ex 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 𝑥)))
2214, 8, 12, 16, 20, 22, 25, 29, 33, 37, 220no3inds 27922 . . . 4 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐵 +s 𝐶) <s (𝐴 +s 𝐶) → 𝐵 <s 𝐴))
222 addscl 27945 . . . . . 6 ((𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐵 +s 𝐶) ∈ No )
2232223adant1 1130 . . . . 5 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐵 +s 𝐶) ∈ No )
224 addscl 27945 . . . . . 6 ((𝐴 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 +s 𝐶) ∈ No )
2252243adant2 1131 . . . . 5 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 +s 𝐶) ∈ No )
226 sltnle 27722 . . . . 5 (((𝐵 +s 𝐶) ∈ No ∧ (𝐴 +s 𝐶) ∈ No ) → ((𝐵 +s 𝐶) <s (𝐴 +s 𝐶) ↔ ¬ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶)))
227223, 225, 226syl2anc 584 . . . 4 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐵 +s 𝐶) <s (𝐴 +s 𝐶) ↔ ¬ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶)))
228 sltnle 27722 . . . . . 6 ((𝐵 ∈ No ∧ 𝐴 ∈ No ) → (𝐵 <s 𝐴 ↔ ¬ 𝐴 ≤s 𝐵))
229228ancoms 458 . . . . 5 ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐵 <s 𝐴 ↔ ¬ 𝐴 ≤s 𝐵))
2302293adant3 1132 . . . 4 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐵 <s 𝐴 ↔ ¬ 𝐴 ≤s 𝐵))
231221, 227, 2303imtr3d 293 . . 3 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (¬ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶) → ¬ 𝐴 ≤s 𝐵))
232231con4d 115 . 2 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 ≤s 𝐵 → (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶)))
233 sleadd1im 27951 . 2 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶) → 𝐴 ≤s 𝐵))
234232, 233impbid 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 847   ∧ w3a 1086   = wceq 1540  ∃wex 1779   ∈ wcel 2109  {cab 2714   ≠ wne 2933  ∀wral 3052  ∃wrex 3061   ∪ cun 3929  ∅c0 4313  {csn 4606   class class class wbr 5124  ‘cfv 6536  (class class class)co 7410   No csur 27608   <s cslt 27609   ≤s csle 27713   <<s csslt 27749   |s cscut 27751   L cleft 27810   R cright 27811   +s cadds 27923
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-rep 5254  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rmo 3364  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-tp 4611  df-op 4613  df-ot 4615  df-uni 4889  df-int 4928  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-se 5612  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-ord 6360  df-on 6361  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-1st 7993  df-2nd 7994  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-1o 8485  df-2o 8486  df-nadd 8683  df-no 27611  df-slt 27612  df-bday 27613  df-sle 27714  df-sslt 27750  df-scut 27752  df-0s 27793  df-made 27812  df-old 27813  df-left 27815  df-right 27816  df-norec2 27913  df-adds 27924
This theorem is referenced by:  sleadd2  27954  addscan2  27957  sleadd1d  27959  nnsge1  28292
  Copyright terms: Public domain W3C validator