MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sleadd1 Structured version   Visualization version   GIF version
Theorem sleadd1 27932
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 7353 . . . . . . 7 (𝑥 = 𝑥𝑂 → (𝑥 +s 𝑧) = (𝑥𝑂 +s 𝑧))
21breq2d 5101 . . . . . 6 (𝑥 = 𝑥𝑂 → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧)))
3 breq2 5093 . . . . . 6 (𝑥 = 𝑥𝑂 → (𝑦 <s 𝑥 ↔ 𝑦 <s 𝑥𝑂))
42, 3imbi12d 344 . . . . 5 (𝑥 = 𝑥𝑂 → (((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦 <s 𝑥) ↔ ((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂)))
5 oveq1 7353 . . . . . . 7 (𝑦 = 𝑦𝑂 → (𝑦 +s 𝑧) = (𝑦𝑂 +s 𝑧))
65breq1d 5099 . . . . . 6 (𝑦 = 𝑦𝑂 → ((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) ↔ (𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧)))
7 breq1 5092 . . . . . 6 (𝑦 = 𝑦𝑂 → (𝑦 <s 𝑥𝑂 ↔ 𝑦𝑂 <s 𝑥𝑂))
86, 7imbi12d 344 . . . . 5 (𝑦 = 𝑦𝑂 → (((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ↔ ((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂)))
9 oveq2 7354 . . . . . . 7 (𝑧 = 𝑧𝑂 → (𝑦𝑂 +s 𝑧) = (𝑦𝑂 +s 𝑧𝑂))
10 oveq2 7354 . . . . . . 7 (𝑧 = 𝑧𝑂 → (𝑥𝑂 +s 𝑧) = (𝑥𝑂 +s 𝑧𝑂))
119, 10breq12d 5102 . . . . . 6 (𝑧 = 𝑧𝑂 → ((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) ↔ (𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂)))
1211imbi1d 341 . . . . 5 (𝑧 = 𝑧𝑂 → (((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ↔ ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂)))
13 oveq1 7353 . . . . . . 7 (𝑥 = 𝑥𝑂 → (𝑥 +s 𝑧𝑂) = (𝑥𝑂 +s 𝑧𝑂))
1413breq2d 5101 . . . . . 6 (𝑥 = 𝑥𝑂 → ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) ↔ (𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂)))
15 breq2 5093 . . . . . 6 (𝑥 = 𝑥𝑂 → (𝑦𝑂 <s 𝑥 ↔ 𝑦𝑂 <s 𝑥𝑂))
1614, 15imbi12d 344 . . . . 5 (𝑥 = 𝑥𝑂 → (((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ↔ ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂)))
17 oveq1 7353 . . . . . . 7 (𝑦 = 𝑦𝑂 → (𝑦 +s 𝑧𝑂) = (𝑦𝑂 +s 𝑧𝑂))
1817breq1d 5099 . . . . . 6 (𝑦 = 𝑦𝑂 → ((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) ↔ (𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂)))
19 breq1 5092 . . . . . 6 (𝑦 = 𝑦𝑂 → (𝑦 <s 𝑥 ↔ 𝑦𝑂 <s 𝑥))
2018, 19imbi12d 344 . . . . 5 (𝑦 = 𝑦𝑂 → (((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥) ↔ ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥)))
2117breq1d 5099 . . . . . 6 (𝑦 = 𝑦𝑂 → ((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) ↔ (𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂)))
2221, 7imbi12d 344 . . . . 5 (𝑦 = 𝑦𝑂 → (((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂) ↔ ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂)))
23 oveq2 7354 . . . . . . 7 (𝑧 = 𝑧𝑂 → (𝑥 +s 𝑧) = (𝑥 +s 𝑧𝑂))
249, 23breq12d 5102 . . . . . 6 (𝑧 = 𝑧𝑂 → ((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂)))
2524imbi1d 341 . . . . 5 (𝑧 = 𝑧𝑂 → (((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥) ↔ ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥)))
26 oveq1 7353 . . . . . . 7 (𝑥 = 𝐴 → (𝑥 +s 𝑧) = (𝐴 +s 𝑧))
2726breq2d 5101 . . . . . 6 (𝑥 = 𝐴 → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (𝑦 +s 𝑧) <s (𝐴 +s 𝑧)))
28 breq2 5093 . . . . . 6 (𝑥 = 𝐴 → (𝑦 <s 𝑥 ↔ 𝑦 <s 𝐴))
2927, 28imbi12d 344 . . . . 5 (𝑥 = 𝐴 → (((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦 <s 𝑥) ↔ ((𝑦 +s 𝑧) <s (𝐴 +s 𝑧) → 𝑦 <s 𝐴)))
30 oveq1 7353 . . . . . . 7 (𝑦 = 𝐵 → (𝑦 +s 𝑧) = (𝐵 +s 𝑧))
3130breq1d 5099 . . . . . 6 (𝑦 = 𝐵 → ((𝑦 +s 𝑧) <s (𝐴 +s 𝑧) ↔ (𝐵 +s 𝑧) <s (𝐴 +s 𝑧)))
32 breq1 5092 . . . . . 6 (𝑦 = 𝐵 → (𝑦 <s 𝐴 ↔ 𝐵 <s 𝐴))
3331, 32imbi12d 344 . . . . 5 (𝑦 = 𝐵 → (((𝑦 +s 𝑧) <s (𝐴 +s 𝑧) → 𝑦 <s 𝐴) ↔ ((𝐵 +s 𝑧) <s (𝐴 +s 𝑧) → 𝐵 <s 𝐴)))
34 oveq2 7354 . . . . . . 7 (𝑧 = 𝐶 → (𝐵 +s 𝑧) = (𝐵 +s 𝐶))
35 oveq2 7354 . . . . . . 7 (𝑧 = 𝐶 → (𝐴 +s 𝑧) = (𝐴 +s 𝐶))
3634, 35breq12d 5102 . . . . . 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 27921 . . . . . . . . . . 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 7379 . . . . . . . . . . . 12 (𝑦 +s 𝑧) ∈ V
4544snnz 4726 . . . . . . . . . . 11 {(𝑦 +s 𝑧)} ≠ ∅
46 sslttr 27748 . . . . . . . . . . 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 27921 . . . . . . . . . . 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 7379 . . . . . . . . . . . 12 (𝑥 +s 𝑧) ∈ V
5554snnz 4726 . . . . . . . . . . 11 {(𝑥 +s 𝑧)} ≠ ∅
56 sslttr 27748 . . . . . . . . . . 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 27906 . . . . . . . . . 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 27906 . . . . . . . . . 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 𝑧𝑅)})))
6348, 58, 60, 62sltrecd 27763 . . . . . . . 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 4143 . . . . . . . . . 10 (∃𝑝 ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)})(𝑦 +s 𝑧) ≤s 𝑝 ↔ (∃𝑝 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} (𝑦 +s 𝑧) ≤s 𝑝 ∨ ∃𝑝 ∈ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)} (𝑦 +s 𝑧) ≤s 𝑝))
66 eqeq1 2735 . . . . . . . . . . . . . 14 (𝑎 = 𝑝 → (𝑎 = (𝑥𝐿 +s 𝑧) ↔ 𝑝 = (𝑥𝐿 +s 𝑧)))
6766rexbidv 3156 . . . . . . . . . . . . 13 (𝑎 = 𝑝 → (∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧) ↔ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑝 = (𝑥𝐿 +s 𝑧)))
6867rexab 3649 . . . . . . . . . . . 12 (∃𝑝 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} (𝑦 +s 𝑧) ≤s 𝑝 ↔ ∃𝑝(∃𝑥𝐿 ∈ ( L ‘𝑥)𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
69 rexcom4 3259 . . . . . . . . . . . . . 14 (∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑝(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
70 r19.41v 3162 . . . . . . . . . . . . . . 15 (∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ (∃𝑥𝐿 ∈ ( L ‘𝑥)𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
7170exbii 1849 . . . . . . . . . . . . . 14 (∃𝑝∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝(∃𝑥𝐿 ∈ ( L ‘𝑥)𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
7269, 71bitri 275 . . . . . . . . . . . . 13 (∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑝(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝(∃𝑥𝐿 ∈ ( L ‘𝑥)𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
73 ovex 7379 . . . . . . . . . . . . . . 15 (𝑥𝐿 +s 𝑧) ∈ V
74 breq2 5093 . . . . . . . . . . . . . . 15 (𝑝 = (𝑥𝐿 +s 𝑧) → ((𝑦 +s 𝑧) ≤s 𝑝 ↔ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧)))
7573, 74ceqsexv 3486 . . . . . . . . . . . . . 14 (∃𝑝(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))
7675rexbii 3079 . . . . . . . . . . . . 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 2735 . . . . . . . . . . . . . 14 (𝑏 = 𝑝 → (𝑏 = (𝑥 +s 𝑧𝐿) ↔ 𝑝 = (𝑥 +s 𝑧𝐿)))
8079rexbidv 3156 . . . . . . . . . . . . 13 (𝑏 = 𝑝 → (∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿) ↔ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧𝐿)))
8180rexab 3649 . . . . . . . . . . . 12 (∃𝑝 ∈ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)} (𝑦 +s 𝑧) ≤s 𝑝 ↔ ∃𝑝(∃𝑧𝐿 ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
82 rexcom4 3259 . . . . . . . . . . . . . 14 (∃𝑧𝐿 ∈ ( L ‘𝑧)∃𝑝(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
83 r19.41v 3162 . . . . . . . . . . . . . . 15 (∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ (∃𝑧𝐿 ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
8483exbii 1849 . . . . . . . . . . . . . 14 (∃𝑝∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝(∃𝑧𝐿 ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
8582, 84bitri 275 . . . . . . . . . . . . 13 (∃𝑧𝐿 ∈ ( L ‘𝑧)∃𝑝(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝(∃𝑧𝐿 ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
86 ovex 7379 . . . . . . . . . . . . . . 15 (𝑥 +s 𝑧𝐿) ∈ V
87 breq2 5093 . . . . . . . . . . . . . . 15 (𝑝 = (𝑥 +s 𝑧𝐿) → ((𝑦 +s 𝑧) ≤s 𝑝 ↔ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿)))
8886, 87ceqsexv 3486 . . . . . . . . . . . . . 14 (∃𝑝(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))
8988rexbii 3079 . . . . . . . . . . . . 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 914 . . . . . . . . . 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 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 )
95 leftssno 27826 . . . . . . . . . . . . . . 15 ( L ‘𝑥) ⊆ No
9695sseli 3925 . . . . . . . . . . . . . 14 (𝑥𝐿 ∈ ( L ‘𝑥) → 𝑥𝐿 ∈ No )
9796adantr 480 . . . . . . . . . . . . 13 ((𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧)) → 𝑥𝐿 ∈ No )
9897adantl 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 )
99 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 )
100 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 𝑧))
101 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 )
102 sleadd1im 27930 . . . . . . . . . . . . . 14 ((𝑦 ∈ No ∧ 𝑥𝐿 ∈ No ∧ 𝑧 ∈ No ) → ((𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧) → 𝑦 ≤s 𝑥𝐿))
10394, 98, 101, 102syl3anc 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 𝑥𝐿))
104100, 103mpd 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 𝑥𝐿)
105 leftlt 27808 . . . . . . . . . . . . . 14 (𝑥𝐿 ∈ ( L ‘𝑥) → 𝑥𝐿 <s 𝑥)
106105adantr 480 . . . . . . . . . . . . 13 ((𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧)) → 𝑥𝐿 <s 𝑥)
107106adantl 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 𝑥)
10894, 98, 99, 104, 107slelttrd 27700 . . . . . . . . . . 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 𝑥)
109108rexlimdvaa 3134 . . . . . . . . . 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 𝑥))
110 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 )
111 leftssno 27826 . . . . . . . . . . . . . . . . 17 ( L ‘𝑧) ⊆ No
112111sseli 3925 . . . . . . . . . . . . . . . 16 (𝑧𝐿 ∈ ( L ‘𝑧) → 𝑧𝐿 ∈ No )
113112adantr 480 . . . . . . . . . . . . . . 15 ((𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿)) → 𝑧𝐿 ∈ No )
114113adantl 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 )
115110, 114addscld 27923 . . . . . . . . . . . . 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 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 )
117110, 116addscld 27923 . . . . . . . . . . . . 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 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 )
119118, 114addscld 27923 . . . . . . . . . . . . 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 )
120 leftlt 27808 . . . . . . . . . . . . . . . 16 (𝑧𝐿 ∈ ( L ‘𝑧) → 𝑧𝐿 <s 𝑧)
121120adantr 480 . . . . . . . . . . . . . . 15 ((𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿)) → 𝑧𝐿 <s 𝑧)
122121adantl 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 𝑧)
123 sltadd2im 27929 . . . . . . . . . . . . . . 15 ((𝑧𝐿 ∈ No ∧ 𝑧 ∈ No ∧ 𝑦 ∈ No ) → (𝑧𝐿 <s 𝑧 → (𝑦 +s 𝑧𝐿) <s (𝑦 +s 𝑧)))
124114, 116, 110, 123syl3anc 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 𝑧)))
125122, 124mpd 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 𝑧))
126 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 𝑧𝐿))
127115, 117, 119, 125, 126sltletrd 27699 . . . . . . . . . . . 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 𝑧𝐿))
128 oveq2 7354 . . . . . . . . . . . . . . 15 (𝑧𝑂 = 𝑧𝐿 → (𝑦 +s 𝑧𝑂) = (𝑦 +s 𝑧𝐿))
129 oveq2 7354 . . . . . . . . . . . . . . 15 (𝑧𝑂 = 𝑧𝐿 → (𝑥 +s 𝑧𝑂) = (𝑥 +s 𝑧𝐿))
130128, 129breq12d 5102 . . . . . . . . . . . . . 14 (𝑧𝑂 = 𝑧𝐿 → ((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) ↔ (𝑦 +s 𝑧𝐿) <s (𝑥 +s 𝑧𝐿)))
131130imbi1d 341 . . . . . . . . . . . . 13 (𝑧𝑂 = 𝑧𝐿 → (((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥) ↔ ((𝑦 +s 𝑧𝐿) <s (𝑥 +s 𝑧𝐿) → 𝑦 <s 𝑥)))
132 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 𝑥))
133 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 ‘𝑧))
134 elun1 4129 . . . . . . . . . . . . . 14 (𝑧𝐿 ∈ ( L ‘𝑧) → 𝑧𝐿 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧)))
135133, 134syl 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 ‘𝑧)))
136131, 132, 135rspcdva 3573 . . . . . . . . . . . 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 𝑥))
137127, 136mpd 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 𝑥)
138137rexlimdvaa 3134 . . . . . . . . . 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 𝑥))
139109, 138jaod 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 𝑥))
14093, 139biimtrid 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 𝑥))
141 rexun 4143 . . . . . . . . . 10 (∃𝑞 ∈ ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})𝑞 ≤s (𝑥 +s 𝑧) ↔ (∃𝑞 ∈ {𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)}𝑞 ≤s (𝑥 +s 𝑧) ∨ ∃𝑞 ∈ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}𝑞 ≤s (𝑥 +s 𝑧)))
142 eqeq1 2735 . . . . . . . . . . . . . 14 (𝑐 = 𝑞 → (𝑐 = (𝑦𝑅 +s 𝑧) ↔ 𝑞 = (𝑦𝑅 +s 𝑧)))
143142rexbidv 3156 . . . . . . . . . . . . 13 (𝑐 = 𝑞 → (∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧) ↔ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧)))
144143rexab 3649 . . . . . . . . . . . 12 (∃𝑞 ∈ {𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)}𝑞 ≤s (𝑥 +s 𝑧) ↔ ∃𝑞(∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
145 rexcom4 3259 . . . . . . . . . . . . . 14 (∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑞(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
146 r19.41v 3162 . . . . . . . . . . . . . . 15 (∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ (∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
147146exbii 1849 . . . . . . . . . . . . . 14 (∃𝑞∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞(∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
148145, 147bitri 275 . . . . . . . . . . . . 13 (∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑞(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞(∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
149 ovex 7379 . . . . . . . . . . . . . . 15 (𝑦𝑅 +s 𝑧) ∈ V
150 breq1 5092 . . . . . . . . . . . . . . 15 (𝑞 = (𝑦𝑅 +s 𝑧) → (𝑞 ≤s (𝑥 +s 𝑧) ↔ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧)))
151149, 150ceqsexv 3486 . . . . . . . . . . . . . 14 (∃𝑞(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))
152151rexbii 3079 . . . . . . . . . . . . 13 (∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑞(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))
153148, 152bitr3i 277 . . . . . . . . . . . 12 (∃𝑞(∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))
154144, 153bitri 275 . . . . . . . . . . 11 (∃𝑞 ∈ {𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)}𝑞 ≤s (𝑥 +s 𝑧) ↔ ∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))
155 eqeq1 2735 . . . . . . . . . . . . . 14 (𝑑 = 𝑞 → (𝑑 = (𝑦 +s 𝑧𝑅) ↔ 𝑞 = (𝑦 +s 𝑧𝑅)))
156155rexbidv 3156 . . . . . . . . . . . . 13 (𝑑 = 𝑞 → (∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅) ↔ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅)))
157156rexab 3649 . . . . . . . . . . . 12 (∃𝑞 ∈ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}𝑞 ≤s (𝑥 +s 𝑧) ↔ ∃𝑞(∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
158 rexcom4 3259 . . . . . . . . . . . . . 14 (∃𝑧𝑅 ∈ ( R ‘𝑧)∃𝑞(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
159 r19.41v 3162 . . . . . . . . . . . . . . 15 (∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ (∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
160159exbii 1849 . . . . . . . . . . . . . 14 (∃𝑞∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞(∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
161158, 160bitri 275 . . . . . . . . . . . . 13 (∃𝑧𝑅 ∈ ( R ‘𝑧)∃𝑞(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞(∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
162 ovex 7379 . . . . . . . . . . . . . . 15 (𝑦 +s 𝑧𝑅) ∈ V
163 breq1 5092 . . . . . . . . . . . . . . 15 (𝑞 = (𝑦 +s 𝑧𝑅) → (𝑞 ≤s (𝑥 +s 𝑧) ↔ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧)))
164162, 163ceqsexv 3486 . . . . . . . . . . . . . 14 (∃𝑞(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))
165164rexbii 3079 . . . . . . . . . . . . 13 (∃𝑧𝑅 ∈ ( R ‘𝑧)∃𝑞(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))
166161, 165bitr3i 277 . . . . . . . . . . . 12 (∃𝑞(∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))
167157, 166bitri 275 . . . . . . . . . . 11 (∃𝑞 ∈ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}𝑞 ≤s (𝑥 +s 𝑧) ↔ ∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))
168154, 167orbi12i 914 . . . . . . . . . 10 ((∃𝑞 ∈ {𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)}𝑞 ≤s (𝑥 +s 𝑧) ∨ ∃𝑞 ∈ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}𝑞 ≤s (𝑥 +s 𝑧)) ↔ (∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧) ∨ ∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧)))
169141, 168bitri 275 . . . . . . . . 9 (∃𝑞 ∈ ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})𝑞 ≤s (𝑥 +s 𝑧) ↔ (∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧) ∨ ∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧)))
170 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 )
171 rightssno 27827 . . . . . . . . . . . . . . 15 ( R ‘𝑦) ⊆ No
172171sseli 3925 . . . . . . . . . . . . . 14 (𝑦𝑅 ∈ ( R ‘𝑦) → 𝑦𝑅 ∈ No )
173172adantr 480 . . . . . . . . . . . . 13 ((𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧)) → 𝑦𝑅 ∈ No )
174173adantl 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 )
175 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 )
176 rightgt 27809 . . . . . . . . . . . . . 14 (𝑦𝑅 ∈ ( R ‘𝑦) → 𝑦 <s 𝑦𝑅)
177176adantr 480 . . . . . . . . . . . . 13 ((𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧)) → 𝑦 <s 𝑦𝑅)
178177adantl 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 𝑦𝑅)
179 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 𝑧))
180 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 )
181 sleadd1im 27930 . . . . . . . . . . . . . 14 ((𝑦𝑅 ∈ No ∧ 𝑥 ∈ No ∧ 𝑧 ∈ No ) → ((𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧) → 𝑦𝑅 ≤s 𝑥))
182174, 175, 180, 181syl3anc 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 𝑥))
183179, 182mpd 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 𝑥)
184170, 174, 175, 178, 183sltletrd 27699 . . . . . . . . . . 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 𝑥)
185184rexlimdvaa 3134 . . . . . . . . . 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 𝑥))
186 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 )
187 rightssno 27827 . . . . . . . . . . . . . . . . 17 ( R ‘𝑧) ⊆ No
188187sseli 3925 . . . . . . . . . . . . . . . 16 (𝑧𝑅 ∈ ( R ‘𝑧) → 𝑧𝑅 ∈ No )
189188adantr 480 . . . . . . . . . . . . . . 15 ((𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧)) → 𝑧𝑅 ∈ No )
190189adantl 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 )
191186, 190addscld 27923 . . . . . . . . . . . . 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 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 )
193 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 )
194192, 193addscld 27923 . . . . . . . . . . . . 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 )
195192, 190addscld 27923 . . . . . . . . . . . . 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 )
196 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 𝑧))
197193, 190, 1923jca 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 ))
198 rightgt 27809 . . . . . . . . . . . . . . . 16 (𝑧𝑅 ∈ ( R ‘𝑧) → 𝑧 <s 𝑧𝑅)
199198adantr 480 . . . . . . . . . . . . . . 15 ((𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧)) → 𝑧 <s 𝑧𝑅)
200199adantl 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 𝑧𝑅)
201 sltadd2im 27929 . . . . . . . . . . . . . 14 ((𝑧 ∈ No ∧ 𝑧𝑅 ∈ No ∧ 𝑥 ∈ No ) → (𝑧 <s 𝑧𝑅 → (𝑥 +s 𝑧) <s (𝑥 +s 𝑧𝑅)))
202197, 200, 201sylc 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 𝑧𝑅))
203191, 194, 195, 196, 202slelttrd 27700 . . . . . . . . . . . 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 𝑧𝑅))
204 oveq2 7354 . . . . . . . . . . . . . . 15 (𝑧𝑂 = 𝑧𝑅 → (𝑦 +s 𝑧𝑂) = (𝑦 +s 𝑧𝑅))
205 oveq2 7354 . . . . . . . . . . . . . . 15 (𝑧𝑂 = 𝑧𝑅 → (𝑥 +s 𝑧𝑂) = (𝑥 +s 𝑧𝑅))
206204, 205breq12d 5102 . . . . . . . . . . . . . 14 (𝑧𝑂 = 𝑧𝑅 → ((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) ↔ (𝑦 +s 𝑧𝑅) <s (𝑥 +s 𝑧𝑅)))
207206imbi1d 341 . . . . . . . . . . . . 13 (𝑧𝑂 = 𝑧𝑅 → (((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥) ↔ ((𝑦 +s 𝑧𝑅) <s (𝑥 +s 𝑧𝑅) → 𝑦 <s 𝑥)))
208 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 𝑥))
209 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 ‘𝑧))
210 elun2 4130 . . . . . . . . . . . . . 14 (𝑧𝑅 ∈ ( R ‘𝑧) → 𝑧𝑅 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧)))
211209, 210syl 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 ‘𝑧)))
212207, 208, 211rspcdva 3573 . . . . . . . . . . . 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 𝑥))
213203, 212mpd 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 𝑥)
214213rexlimdvaa 3134 . . . . . . . . . 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 𝑥))
215185, 214jaod 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 𝑥))
216169, 215biimtrid 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 𝑥))
217140, 216jaod 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 𝑥))
21864, 217sylbid 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 𝑥))
219218ex 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 𝑥)))
2204, 8, 12, 16, 20, 22, 25, 29, 33, 37, 219no3inds 27901 . . . 4 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐵 +s 𝐶) <s (𝐴 +s 𝐶) → 𝐵 <s 𝐴))
221 addscl 27924 . . . . . 6 ((𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐵 +s 𝐶) ∈ No )
2222213adant1 1130 . . . . 5 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐵 +s 𝐶) ∈ No )
223 addscl 27924 . . . . . 6 ((𝐴 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 +s 𝐶) ∈ No )
2242233adant2 1131 . . . . 5 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 +s 𝐶) ∈ No )
225 sltnle 27692 . . . . 5 (((𝐵 +s 𝐶) ∈ No ∧ (𝐴 +s 𝐶) ∈ No ) → ((𝐵 +s 𝐶) <s (𝐴 +s 𝐶) ↔ ¬ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶)))
226222, 224, 225syl2anc 584 . . . 4 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐵 +s 𝐶) <s (𝐴 +s 𝐶) ↔ ¬ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶)))
227 sltnle 27692 . . . . . 6 ((𝐵 ∈ No ∧ 𝐴 ∈ No ) → (𝐵 <s 𝐴 ↔ ¬ 𝐴 ≤s 𝐵))
228227ancoms 458 . . . . 5 ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐵 <s 𝐴 ↔ ¬ 𝐴 ≤s 𝐵))
2292283adant3 1132 . . . 4 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐵 <s 𝐴 ↔ ¬ 𝐴 ≤s 𝐵))
230220, 226, 2293imtr3d 293 . . 3 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (¬ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶) → ¬ 𝐴 ≤s 𝐵))
231230con4d 115 . 2 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 ≤s 𝐵 → (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶)))
232 sleadd1im 27930 . 2 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶) → 𝐴 ≤s 𝐵))
233231, 232impbid 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 1541  ∃wex 1780   ∈ wcel 2111  {cab 2709   ≠ wne 2928  ∀wral 3047  ∃wrex 3056   ∪ cun 3895  ∅c0 4280  {csn 4573   class class class wbr 5089  ‘cfv 6481  (class class class)co 7346   No csur 27578   <s cslt 27579   ≤s csle 27683   <<s csslt 27720   |s cscut 27722   L cleft 27786   R cright 27787   +s cadds 27902
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5215  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-tp 4578  df-op 4580  df-ot 4582  df-uni 4857  df-int 4896  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-se 5568  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6248  df-ord 6309  df-on 6310  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-riota 7303  df-ov 7349  df-oprab 7350  df-mpo 7351  df-1st 7921  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-1o 8385  df-2o 8386  df-nadd 8581  df-no 27581  df-slt 27582  df-bday 27583  df-sle 27684  df-sslt 27721  df-scut 27723  df-0s 27768  df-made 27788  df-old 27789  df-left 27791  df-right 27792  df-norec2 27892  df-adds 27903
This theorem is referenced by:  sleadd2  27933  addscan2  27936  sleadd1d  27938  nnsge1  28271  zsoring  28332
  Copyright terms: Public domain W3C validator