MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  leadds1 Structured version   Visualization version   GIF version
Theorem leadds1 28006
Description: Addition to both sides of surreal less-than or equal. Theorem 5 of [Conway] p. 18. (Contributed by Scott Fenton, 21-Jan-2025.)
Assertion
Ref Expression
leadds1 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 ≤s 𝐵 ↔ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶)))
Proof of Theorem leadds1
Dummy variables 𝑥 𝑦 𝑧 𝑎 𝑏 𝑐 𝑑 𝑝 𝑞 𝑥𝐿 𝑦𝐿 𝑧𝐿 𝑥𝑅 𝑦𝑅 𝑧𝑅 𝑥𝑂 𝑦𝑂 𝑧𝑂 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 7370 . . . . . . 7 (𝑥 = 𝑥𝑂 → (𝑥 +s 𝑧) = (𝑥𝑂 +s 𝑧))
21breq2d 5091 . . . . . 6 (𝑥 = 𝑥𝑂 → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧)))
3 breq2 5083 . . . . . 6 (𝑥 = 𝑥𝑂 → (𝑦 <s 𝑥 ↔ 𝑦 <s 𝑥𝑂))
42, 3imbi12d 345 . . . . 5 (𝑥 = 𝑥𝑂 → (((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦 <s 𝑥) ↔ ((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂)))
5 oveq1 7370 . . . . . . 7 (𝑦 = 𝑦𝑂 → (𝑦 +s 𝑧) = (𝑦𝑂 +s 𝑧))
65breq1d 5089 . . . . . 6 (𝑦 = 𝑦𝑂 → ((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) ↔ (𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧)))
7 breq1 5082 . . . . . 6 (𝑦 = 𝑦𝑂 → (𝑦 <s 𝑥𝑂 ↔ 𝑦𝑂 <s 𝑥𝑂))
86, 7imbi12d 345 . . . . 5 (𝑦 = 𝑦𝑂 → (((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ↔ ((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂)))
9 oveq2 7371 . . . . . . 7 (𝑧 = 𝑧𝑂 → (𝑦𝑂 +s 𝑧) = (𝑦𝑂 +s 𝑧𝑂))
10 oveq2 7371 . . . . . . 7 (𝑧 = 𝑧𝑂 → (𝑥𝑂 +s 𝑧) = (𝑥𝑂 +s 𝑧𝑂))
119, 10breq12d 5092 . . . . . 6 (𝑧 = 𝑧𝑂 → ((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) ↔ (𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂)))
1211imbi1d 342 . . . . 5 (𝑧 = 𝑧𝑂 → (((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ↔ ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂)))
13 oveq1 7370 . . . . . . 7 (𝑥 = 𝑥𝑂 → (𝑥 +s 𝑧𝑂) = (𝑥𝑂 +s 𝑧𝑂))
1413breq2d 5091 . . . . . 6 (𝑥 = 𝑥𝑂 → ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) ↔ (𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂)))
15 breq2 5083 . . . . . 6 (𝑥 = 𝑥𝑂 → (𝑦𝑂 <s 𝑥 ↔ 𝑦𝑂 <s 𝑥𝑂))
1614, 15imbi12d 345 . . . . 5 (𝑥 = 𝑥𝑂 → (((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ↔ ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂)))
17 oveq1 7370 . . . . . . 7 (𝑦 = 𝑦𝑂 → (𝑦 +s 𝑧𝑂) = (𝑦𝑂 +s 𝑧𝑂))
1817breq1d 5089 . . . . . 6 (𝑦 = 𝑦𝑂 → ((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) ↔ (𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂)))
19 breq1 5082 . . . . . 6 (𝑦 = 𝑦𝑂 → (𝑦 <s 𝑥 ↔ 𝑦𝑂 <s 𝑥))
2018, 19imbi12d 345 . . . . 5 (𝑦 = 𝑦𝑂 → (((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥) ↔ ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥)))
2117breq1d 5089 . . . . . 6 (𝑦 = 𝑦𝑂 → ((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) ↔ (𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂)))
2221, 7imbi12d 345 . . . . 5 (𝑦 = 𝑦𝑂 → (((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂) ↔ ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂)))
23 oveq2 7371 . . . . . . 7 (𝑧 = 𝑧𝑂 → (𝑥 +s 𝑧) = (𝑥 +s 𝑧𝑂))
249, 23breq12d 5092 . . . . . 6 (𝑧 = 𝑧𝑂 → ((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂)))
2524imbi1d 342 . . . . 5 (𝑧 = 𝑧𝑂 → (((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥) ↔ ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥)))
26 oveq1 7370 . . . . . . 7 (𝑥 = 𝐴 → (𝑥 +s 𝑧) = (𝐴 +s 𝑧))
2726breq2d 5091 . . . . . 6 (𝑥 = 𝐴 → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (𝑦 +s 𝑧) <s (𝐴 +s 𝑧)))
28 breq2 5083 . . . . . 6 (𝑥 = 𝐴 → (𝑦 <s 𝑥 ↔ 𝑦 <s 𝐴))
2927, 28imbi12d 345 . . . . 5 (𝑥 = 𝐴 → (((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦 <s 𝑥) ↔ ((𝑦 +s 𝑧) <s (𝐴 +s 𝑧) → 𝑦 <s 𝐴)))
30 oveq1 7370 . . . . . . 7 (𝑦 = 𝐵 → (𝑦 +s 𝑧) = (𝐵 +s 𝑧))
3130breq1d 5089 . . . . . 6 (𝑦 = 𝐵 → ((𝑦 +s 𝑧) <s (𝐴 +s 𝑧) ↔ (𝐵 +s 𝑧) <s (𝐴 +s 𝑧)))
32 breq1 5082 . . . . . 6 (𝑦 = 𝐵 → (𝑦 <s 𝐴 ↔ 𝐵 <s 𝐴))
3331, 32imbi12d 345 . . . . 5 (𝑦 = 𝐵 → (((𝑦 +s 𝑧) <s (𝐴 +s 𝑧) → 𝑦 <s 𝐴) ↔ ((𝐵 +s 𝑧) <s (𝐴 +s 𝑧) → 𝐵 <s 𝐴)))
34 oveq2 7371 . . . . . . 7 (𝑧 = 𝐶 → (𝐵 +s 𝑧) = (𝐵 +s 𝐶))
35 oveq2 7371 . . . . . . 7 (𝑧 = 𝐶 → (𝐴 +s 𝑧) = (𝐴 +s 𝐶))
3634, 35breq12d 5092 . . . . . 6 (𝑧 = 𝐶 → ((𝐵 +s 𝑧) <s (𝐴 +s 𝑧) ↔ (𝐵 +s 𝐶) <s (𝐴 +s 𝐶)))
3736imbi1d 342 . . . . 5 (𝑧 = 𝐶 → (((𝐵 +s 𝑧) <s (𝐴 +s 𝑧) → 𝐵 <s 𝐴) ↔ ((𝐵 +s 𝐶) <s (𝐴 +s 𝐶) → 𝐵 <s 𝐴)))
38 simp2 1143 . . . . . . . . . . . 12 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → 𝑦 ∈ No )
39 simp3 1144 . . . . . . . . . . . 12 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → 𝑧 ∈ No )
4038, 39addcuts 27995 . . . . . . . . . . 11 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ((𝑦 +s 𝑧) ∈ No ∧ ({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) <<s {(𝑦 +s 𝑧)} ∧ {(𝑦 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})))
41 simp2 1143 . . . . . . . . . . 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 1150 . . . . . . . . . 10 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → {(𝑦 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}))
44 ovex 7396 . . . . . . . . . . . 12 (𝑦 +s 𝑧) ∈ V
4544snnz 4715 . . . . . . . . . . 11 {(𝑦 +s 𝑧)} ≠ ∅
46 sltstr 27804 . . . . . . . . . . 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 1458 . . . . . . . . . 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 590 . . . . . . . . 9 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) <<s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}))
49 simp1 1142 . . . . . . . . . . . 12 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → 𝑥 ∈ No )
5049, 39addcuts 27995 . . . . . . . . . . 11 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ((𝑥 +s 𝑧) ∈ No ∧ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) <<s {(𝑥 +s 𝑧)} ∧ {(𝑥 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)})))
51 simp2 1143 . . . . . . . . . . 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 1150 . . . . . . . . . 10 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → {(𝑥 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)}))
54 ovex 7396 . . . . . . . . . . . 12 (𝑥 +s 𝑧) ∈ V
5554snnz 4715 . . . . . . . . . . 11 {(𝑥 +s 𝑧)} ≠ ∅
56 sltstr 27804 . . . . . . . . . . 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 1458 . . . . . . . . . 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 590 . . . . . . . . 9 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) <<s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)}))
59 addsval2 27980 . . . . . . . . . 10 ((𝑦 ∈ No ∧ 𝑧 ∈ No ) → (𝑦 +s 𝑧) = (({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) |s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})))
60593adant1 1136 . . . . . . . . 9 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → (𝑦 +s 𝑧) = (({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) |s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})))
61 addsval2 27980 . . . . . . . . . 10 ((𝑥 ∈ No ∧ 𝑧 ∈ No ) → (𝑥 +s 𝑧) = (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) |s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)})))
62613adant2 1137 . . . . . . . . 9 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → (𝑥 +s 𝑧) = (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) |s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)})))
6348, 58, 60, 62ltsrecd 27819 . . . . . . . 8 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (∃𝑝 ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)})(𝑦 +s 𝑧) ≤s 𝑝 ∨ ∃𝑞 ∈ ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})𝑞 ≤s (𝑥 +s 𝑧))))
6463adantr 481 . . . . . . 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 4132 . . . . . . . . . 10 (∃𝑝 ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)})(𝑦 +s 𝑧) ≤s 𝑝 ↔ (∃𝑝 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} (𝑦 +s 𝑧) ≤s 𝑝 ∨ ∃𝑝 ∈ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)} (𝑦 +s 𝑧) ≤s 𝑝))
66 eqeq1 2744 . . . . . . . . . . . . . 14 (𝑎 = 𝑝 → (𝑎 = (𝑥𝐿 +s 𝑧) ↔ 𝑝 = (𝑥𝐿 +s 𝑧)))
6766rexbidv 3164 . . . . . . . . . . . . 13 (𝑎 = 𝑝 → (∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧) ↔ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑝 = (𝑥𝐿 +s 𝑧)))
6867rexab 3643 . . . . . . . . . . . 12 (∃𝑝 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} (𝑦 +s 𝑧) ≤s 𝑝 ↔ ∃𝑝(∃𝑥𝐿 ∈ ( L ‘𝑥)𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
69 rexcom4 3267 . . . . . . . . . . . . . 14 (∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑝(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
70 r19.41v 3170 . . . . . . . . . . . . . . 15 (∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ (∃𝑥𝐿 ∈ ( L ‘𝑥)𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
7170exbii 1855 . . . . . . . . . . . . . 14 (∃𝑝∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝(∃𝑥𝐿 ∈ ( L ‘𝑥)𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
7269, 71bitri 276 . . . . . . . . . . . . 13 (∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑝(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝(∃𝑥𝐿 ∈ ( L ‘𝑥)𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
73 ovex 7396 . . . . . . . . . . . . . . 15 (𝑥𝐿 +s 𝑧) ∈ V
74 breq2 5083 . . . . . . . . . . . . . . 15 (𝑝 = (𝑥𝐿 +s 𝑧) → ((𝑦 +s 𝑧) ≤s 𝑝 ↔ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧)))
7573, 74ceqsexv 3481 . . . . . . . . . . . . . 14 (∃𝑝(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))
7675rexbii 3087 . . . . . . . . . . . . 13 (∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑝(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))
7772, 76bitr3i 278 . . . . . . . . . . . 12 (∃𝑝(∃𝑥𝐿 ∈ ( L ‘𝑥)𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))
7868, 77bitri 276 . . . . . . . . . . 11 (∃𝑝 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} (𝑦 +s 𝑧) ≤s 𝑝 ↔ ∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))
79 eqeq1 2744 . . . . . . . . . . . . . 14 (𝑏 = 𝑝 → (𝑏 = (𝑥 +s 𝑧𝐿) ↔ 𝑝 = (𝑥 +s 𝑧𝐿)))
8079rexbidv 3164 . . . . . . . . . . . . 13 (𝑏 = 𝑝 → (∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿) ↔ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧𝐿)))
8180rexab 3643 . . . . . . . . . . . 12 (∃𝑝 ∈ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)} (𝑦 +s 𝑧) ≤s 𝑝 ↔ ∃𝑝(∃𝑧𝐿 ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
82 rexcom4 3267 . . . . . . . . . . . . . 14 (∃𝑧𝐿 ∈ ( L ‘𝑧)∃𝑝(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
83 r19.41v 3170 . . . . . . . . . . . . . . 15 (∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ (∃𝑧𝐿 ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
8483exbii 1855 . . . . . . . . . . . . . 14 (∃𝑝∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝(∃𝑧𝐿 ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
8582, 84bitri 276 . . . . . . . . . . . . 13 (∃𝑧𝐿 ∈ ( L ‘𝑧)∃𝑝(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝(∃𝑧𝐿 ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
86 ovex 7396 . . . . . . . . . . . . . . 15 (𝑥 +s 𝑧𝐿) ∈ V
87 breq2 5083 . . . . . . . . . . . . . . 15 (𝑝 = (𝑥 +s 𝑧𝐿) → ((𝑦 +s 𝑧) ≤s 𝑝 ↔ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿)))
8886, 87ceqsexv 3481 . . . . . . . . . . . . . 14 (∃𝑝(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))
8988rexbii 3087 . . . . . . . . . . . . 13 (∃𝑧𝐿 ∈ ( L ‘𝑧)∃𝑝(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))
9085, 89bitr3i 278 . . . . . . . . . . . 12 (∃𝑝(∃𝑧𝐿 ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))
9181, 90bitri 276 . . . . . . . . . . 11 (∃𝑝 ∈ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)} (𝑦 +s 𝑧) ≤s 𝑝 ↔ ∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))
9278, 91orbi12i 920 . . . . . . . . . 10 ((∃𝑝 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} (𝑦 +s 𝑧) ≤s 𝑝 ∨ ∃𝑝 ∈ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)} (𝑦 +s 𝑧) ≤s 𝑝) ↔ (∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧) ∨ ∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿)))
9365, 92bitri 276 . . . . . . . . 9 (∃𝑝 ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)})(𝑦 +s 𝑧) ≤s 𝑝 ↔ (∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧) ∨ ∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿)))
94 simpll2 1220 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))) → 𝑦 ∈ No )
95 leftno 27894 . . . . . . . . . . . . . 14 (𝑥𝐿 ∈ ( L ‘𝑥) → 𝑥𝐿 ∈ No )
9695adantr 481 . . . . . . . . . . . . 13 ((𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧)) → 𝑥𝐿 ∈ No )
9796adantl 482 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))) → 𝑥𝐿 ∈ No )
98 simpll1 1219 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))) → 𝑥 ∈ No )
99 simprr 778 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))) → (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))
100 simpll3 1221 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))) → 𝑧 ∈ No )
101 leadds1im 28004 . . . . . . . . . . . . . 14 ((𝑦 ∈ No ∧ 𝑥𝐿 ∈ No ∧ 𝑧 ∈ No ) → ((𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧) → 𝑦 ≤s 𝑥𝐿))
10294, 97, 100, 101syl3anc 1379 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))) → ((𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧) → 𝑦 ≤s 𝑥𝐿))
10399, 102mpd 15 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))) → 𝑦 ≤s 𝑥𝐿)
104 leftlt 27870 . . . . . . . . . . . . . 14 (𝑥𝐿 ∈ ( L ‘𝑥) → 𝑥𝐿 <s 𝑥)
105104adantr 481 . . . . . . . . . . . . 13 ((𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧)) → 𝑥𝐿 <s 𝑥)
106105adantl 482 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))) → 𝑥𝐿 <s 𝑥)
10794, 97, 98, 103, 106leltstrd 27754 . . . . . . . . . . 11 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))) → 𝑦 <s 𝑥)
108107rexlimdvaa 3142 . . . . . . . . . 10 (((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) → (∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧) → 𝑦 <s 𝑥))
109 simpll2 1220 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → 𝑦 ∈ No )
110 leftno 27894 . . . . . . . . . . . . . . . 16 (𝑧𝐿 ∈ ( L ‘𝑧) → 𝑧𝐿 ∈ No )
111110adantr 481 . . . . . . . . . . . . . . 15 ((𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿)) → 𝑧𝐿 ∈ No )
112111adantl 482 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → 𝑧𝐿 ∈ No )
113109, 112addscld 27997 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → (𝑦 +s 𝑧𝐿) ∈ No )
114 simpll3 1221 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → 𝑧 ∈ No )
115109, 114addscld 27997 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → (𝑦 +s 𝑧) ∈ No )
116 simpll1 1219 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → 𝑥 ∈ No )
117116, 112addscld 27997 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → (𝑥 +s 𝑧𝐿) ∈ No )
118 leftlt 27870 . . . . . . . . . . . . . . . 16 (𝑧𝐿 ∈ ( L ‘𝑧) → 𝑧𝐿 <s 𝑧)
119118adantr 481 . . . . . . . . . . . . . . 15 ((𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿)) → 𝑧𝐿 <s 𝑧)
120119adantl 482 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → 𝑧𝐿 <s 𝑧)
121 ltadds2im 28003 . . . . . . . . . . . . . . 15 ((𝑧𝐿 ∈ No ∧ 𝑧 ∈ No ∧ 𝑦 ∈ No ) → (𝑧𝐿 <s 𝑧 → (𝑦 +s 𝑧𝐿) <s (𝑦 +s 𝑧)))
122112, 114, 109, 121syl3anc 1379 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → (𝑧𝐿 <s 𝑧 → (𝑦 +s 𝑧𝐿) <s (𝑦 +s 𝑧)))
123120, 122mpd 15 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → (𝑦 +s 𝑧𝐿) <s (𝑦 +s 𝑧))
124 simprr 778 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))
125113, 115, 117, 123, 124ltlestrd 27753 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → (𝑦 +s 𝑧𝐿) <s (𝑥 +s 𝑧𝐿))
126 oveq2 7371 . . . . . . . . . . . . . . 15 (𝑧𝑂 = 𝑧𝐿 → (𝑦 +s 𝑧𝑂) = (𝑦 +s 𝑧𝐿))
127 oveq2 7371 . . . . . . . . . . . . . . 15 (𝑧𝑂 = 𝑧𝐿 → (𝑥 +s 𝑧𝑂) = (𝑥 +s 𝑧𝐿))
128126, 127breq12d 5092 . . . . . . . . . . . . . 14 (𝑧𝑂 = 𝑧𝐿 → ((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) ↔ (𝑦 +s 𝑧𝐿) <s (𝑥 +s 𝑧𝐿)))
129128imbi1d 342 . . . . . . . . . . . . 13 (𝑧𝑂 = 𝑧𝐿 → (((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥) ↔ ((𝑦 +s 𝑧𝐿) <s (𝑥 +s 𝑧𝐿) → 𝑦 <s 𝑥)))
130 simplr3 1224 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))
131 simprl 776 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → 𝑧𝐿 ∈ ( L ‘𝑧))
132 elun1 4118 . . . . . . . . . . . . . 14 (𝑧𝐿 ∈ ( L ‘𝑧) → 𝑧𝐿 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧)))
133131, 132syl 17 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → 𝑧𝐿 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧)))
134129, 130, 133rspcdva 3568 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → ((𝑦 +s 𝑧𝐿) <s (𝑥 +s 𝑧𝐿) → 𝑦 <s 𝑥))
135125, 134mpd 15 . . . . . . . . . . 11 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → 𝑦 <s 𝑥)
136135rexlimdvaa 3142 . . . . . . . . . 10 (((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) → (∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿) → 𝑦 <s 𝑥))
137108, 136jaod 865 . . . . . . . . 9 (((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) → ((∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧) ∨ ∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿)) → 𝑦 <s 𝑥))
13893, 137biimtrid 243 . . . . . . . 8 (((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) → (∃𝑝 ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)})(𝑦 +s 𝑧) ≤s 𝑝 → 𝑦 <s 𝑥))
139 rexun 4132 . . . . . . . . . 10 (∃𝑞 ∈ ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})𝑞 ≤s (𝑥 +s 𝑧) ↔ (∃𝑞 ∈ {𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)}𝑞 ≤s (𝑥 +s 𝑧) ∨ ∃𝑞 ∈ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}𝑞 ≤s (𝑥 +s 𝑧)))
140 eqeq1 2744 . . . . . . . . . . . . . 14 (𝑐 = 𝑞 → (𝑐 = (𝑦𝑅 +s 𝑧) ↔ 𝑞 = (𝑦𝑅 +s 𝑧)))
141140rexbidv 3164 . . . . . . . . . . . . 13 (𝑐 = 𝑞 → (∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧) ↔ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧)))
142141rexab 3643 . . . . . . . . . . . 12 (∃𝑞 ∈ {𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)}𝑞 ≤s (𝑥 +s 𝑧) ↔ ∃𝑞(∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
143 rexcom4 3267 . . . . . . . . . . . . . 14 (∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑞(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
144 r19.41v 3170 . . . . . . . . . . . . . . 15 (∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ (∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
145144exbii 1855 . . . . . . . . . . . . . 14 (∃𝑞∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞(∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
146143, 145bitri 276 . . . . . . . . . . . . 13 (∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑞(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞(∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
147 ovex 7396 . . . . . . . . . . . . . . 15 (𝑦𝑅 +s 𝑧) ∈ V
148 breq1 5082 . . . . . . . . . . . . . . 15 (𝑞 = (𝑦𝑅 +s 𝑧) → (𝑞 ≤s (𝑥 +s 𝑧) ↔ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧)))
149147, 148ceqsexv 3481 . . . . . . . . . . . . . 14 (∃𝑞(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))
150149rexbii 3087 . . . . . . . . . . . . 13 (∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑞(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))
151146, 150bitr3i 278 . . . . . . . . . . . 12 (∃𝑞(∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))
152142, 151bitri 276 . . . . . . . . . . 11 (∃𝑞 ∈ {𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)}𝑞 ≤s (𝑥 +s 𝑧) ↔ ∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))
153 eqeq1 2744 . . . . . . . . . . . . . 14 (𝑑 = 𝑞 → (𝑑 = (𝑦 +s 𝑧𝑅) ↔ 𝑞 = (𝑦 +s 𝑧𝑅)))
154153rexbidv 3164 . . . . . . . . . . . . 13 (𝑑 = 𝑞 → (∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅) ↔ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅)))
155154rexab 3643 . . . . . . . . . . . 12 (∃𝑞 ∈ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}𝑞 ≤s (𝑥 +s 𝑧) ↔ ∃𝑞(∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
156 rexcom4 3267 . . . . . . . . . . . . . 14 (∃𝑧𝑅 ∈ ( R ‘𝑧)∃𝑞(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
157 r19.41v 3170 . . . . . . . . . . . . . . 15 (∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ (∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
158157exbii 1855 . . . . . . . . . . . . . 14 (∃𝑞∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞(∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
159156, 158bitri 276 . . . . . . . . . . . . 13 (∃𝑧𝑅 ∈ ( R ‘𝑧)∃𝑞(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞(∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
160 ovex 7396 . . . . . . . . . . . . . . 15 (𝑦 +s 𝑧𝑅) ∈ V
161 breq1 5082 . . . . . . . . . . . . . . 15 (𝑞 = (𝑦 +s 𝑧𝑅) → (𝑞 ≤s (𝑥 +s 𝑧) ↔ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧)))
162160, 161ceqsexv 3481 . . . . . . . . . . . . . 14 (∃𝑞(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))
163162rexbii 3087 . . . . . . . . . . . . 13 (∃𝑧𝑅 ∈ ( R ‘𝑧)∃𝑞(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))
164159, 163bitr3i 278 . . . . . . . . . . . 12 (∃𝑞(∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))
165155, 164bitri 276 . . . . . . . . . . 11 (∃𝑞 ∈ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}𝑞 ≤s (𝑥 +s 𝑧) ↔ ∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))
166152, 165orbi12i 920 . . . . . . . . . 10 ((∃𝑞 ∈ {𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)}𝑞 ≤s (𝑥 +s 𝑧) ∨ ∃𝑞 ∈ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}𝑞 ≤s (𝑥 +s 𝑧)) ↔ (∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧) ∨ ∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧)))
167139, 166bitri 276 . . . . . . . . 9 (∃𝑞 ∈ ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})𝑞 ≤s (𝑥 +s 𝑧) ↔ (∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧) ∨ ∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧)))
168 simpll2 1220 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))) → 𝑦 ∈ No )
169 rightno 27895 . . . . . . . . . . . . . 14 (𝑦𝑅 ∈ ( R ‘𝑦) → 𝑦𝑅 ∈ No )
170169adantr 481 . . . . . . . . . . . . 13 ((𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧)) → 𝑦𝑅 ∈ No )
171170adantl 482 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))) → 𝑦𝑅 ∈ No )
172 simpll1 1219 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))) → 𝑥 ∈ No )
173 rightgt 27871 . . . . . . . . . . . . . 14 (𝑦𝑅 ∈ ( R ‘𝑦) → 𝑦 <s 𝑦𝑅)
174173adantr 481 . . . . . . . . . . . . 13 ((𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧)) → 𝑦 <s 𝑦𝑅)
175174adantl 482 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))) → 𝑦 <s 𝑦𝑅)
176 simprr 778 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))) → (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))
177 simpll3 1221 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))) → 𝑧 ∈ No )
178 leadds1im 28004 . . . . . . . . . . . . . 14 ((𝑦𝑅 ∈ No ∧ 𝑥 ∈ No ∧ 𝑧 ∈ No ) → ((𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧) → 𝑦𝑅 ≤s 𝑥))
179171, 172, 177, 178syl3anc 1379 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))) → ((𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧) → 𝑦𝑅 ≤s 𝑥))
180176, 179mpd 15 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))) → 𝑦𝑅 ≤s 𝑥)
181168, 171, 172, 175, 180ltlestrd 27753 . . . . . . . . . . 11 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))) → 𝑦 <s 𝑥)
182181rexlimdvaa 3142 . . . . . . . . . 10 (((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) → (∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧) → 𝑦 <s 𝑥))
183 simpll2 1220 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → 𝑦 ∈ No )
184 rightno 27895 . . . . . . . . . . . . . . . 16 (𝑧𝑅 ∈ ( R ‘𝑧) → 𝑧𝑅 ∈ No )
185184adantr 481 . . . . . . . . . . . . . . 15 ((𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧)) → 𝑧𝑅 ∈ No )
186185adantl 482 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → 𝑧𝑅 ∈ No )
187183, 186addscld 27997 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → (𝑦 +s 𝑧𝑅) ∈ No )
188 simpll1 1219 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → 𝑥 ∈ No )
189 simpll3 1221 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → 𝑧 ∈ No )
190188, 189addscld 27997 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → (𝑥 +s 𝑧) ∈ No )
191188, 186addscld 27997 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → (𝑥 +s 𝑧𝑅) ∈ No )
192 simprr 778 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))
193189, 186, 1883jca 1134 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → (𝑧 ∈ No ∧ 𝑧𝑅 ∈ No ∧ 𝑥 ∈ No ))
194 rightgt 27871 . . . . . . . . . . . . . . . 16 (𝑧𝑅 ∈ ( R ‘𝑧) → 𝑧 <s 𝑧𝑅)
195194adantr 481 . . . . . . . . . . . . . . 15 ((𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧)) → 𝑧 <s 𝑧𝑅)
196195adantl 482 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → 𝑧 <s 𝑧𝑅)
197 ltadds2im 28003 . . . . . . . . . . . . . 14 ((𝑧 ∈ No ∧ 𝑧𝑅 ∈ No ∧ 𝑥 ∈ No ) → (𝑧 <s 𝑧𝑅 → (𝑥 +s 𝑧) <s (𝑥 +s 𝑧𝑅)))
198193, 196, 197sylc 65 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → (𝑥 +s 𝑧) <s (𝑥 +s 𝑧𝑅))
199187, 190, 191, 192, 198leltstrd 27754 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → (𝑦 +s 𝑧𝑅) <s (𝑥 +s 𝑧𝑅))
200 oveq2 7371 . . . . . . . . . . . . . . 15 (𝑧𝑂 = 𝑧𝑅 → (𝑦 +s 𝑧𝑂) = (𝑦 +s 𝑧𝑅))
201 oveq2 7371 . . . . . . . . . . . . . . 15 (𝑧𝑂 = 𝑧𝑅 → (𝑥 +s 𝑧𝑂) = (𝑥 +s 𝑧𝑅))
202200, 201breq12d 5092 . . . . . . . . . . . . . 14 (𝑧𝑂 = 𝑧𝑅 → ((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) ↔ (𝑦 +s 𝑧𝑅) <s (𝑥 +s 𝑧𝑅)))
203202imbi1d 342 . . . . . . . . . . . . 13 (𝑧𝑂 = 𝑧𝑅 → (((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥) ↔ ((𝑦 +s 𝑧𝑅) <s (𝑥 +s 𝑧𝑅) → 𝑦 <s 𝑥)))
204 simplr3 1224 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))
205 simprl 776 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → 𝑧𝑅 ∈ ( R ‘𝑧))
206 elun2 4119 . . . . . . . . . . . . . 14 (𝑧𝑅 ∈ ( R ‘𝑧) → 𝑧𝑅 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧)))
207205, 206syl 17 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → 𝑧𝑅 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧)))
208203, 204, 207rspcdva 3568 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → ((𝑦 +s 𝑧𝑅) <s (𝑥 +s 𝑧𝑅) → 𝑦 <s 𝑥))
209199, 208mpd 15 . . . . . . . . . . 11 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → 𝑦 <s 𝑥)
210209rexlimdvaa 3142 . . . . . . . . . 10 (((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) → (∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧) → 𝑦 <s 𝑥))
211182, 210jaod 865 . . . . . . . . 9 (((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) → ((∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧) ∨ ∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧)) → 𝑦 <s 𝑥))
212167, 211biimtrid 243 . . . . . . . 8 (((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) → (∃𝑞 ∈ ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})𝑞 ≤s (𝑥 +s 𝑧) → 𝑦 <s 𝑥))
213138, 212jaod 865 . . . . . . 7 (((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) → ((∃𝑝 ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)})(𝑦 +s 𝑧) ≤s 𝑝 ∨ ∃𝑞 ∈ ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})𝑞 ≤s (𝑥 +s 𝑧)) → 𝑦 <s 𝑥))
21464, 213sylbid 241 . . . . . 6 (((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦 <s 𝑥))
215214ex 413 . . . . 5 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → (((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥)) → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦 <s 𝑥)))
2164, 8, 12, 16, 20, 22, 25, 29, 33, 37, 215no3inds 27975 . . . 4 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐵 +s 𝐶) <s (𝐴 +s 𝐶) → 𝐵 <s 𝐴))
217 addscl 27998 . . . . . 6 ((𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐵 +s 𝐶) ∈ No )
2182173adant1 1136 . . . . 5 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐵 +s 𝐶) ∈ No )
219 addscl 27998 . . . . . 6 ((𝐴 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 +s 𝐶) ∈ No )
2202193adant2 1137 . . . . 5 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 +s 𝐶) ∈ No )
221 ltnles 27742 . . . . 5 (((𝐵 +s 𝐶) ∈ No ∧ (𝐴 +s 𝐶) ∈ No ) → ((𝐵 +s 𝐶) <s (𝐴 +s 𝐶) ↔ ¬ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶)))
222218, 220, 221syl2anc 590 . . . 4 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐵 +s 𝐶) <s (𝐴 +s 𝐶) ↔ ¬ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶)))
223 ltnles 27742 . . . . . 6 ((𝐵 ∈ No ∧ 𝐴 ∈ No ) → (𝐵 <s 𝐴 ↔ ¬ 𝐴 ≤s 𝐵))
224223ancoms 459 . . . . 5 ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐵 <s 𝐴 ↔ ¬ 𝐴 ≤s 𝐵))
2252243adant3 1138 . . . 4 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐵 <s 𝐴 ↔ ¬ 𝐴 ≤s 𝐵))
226216, 222, 2253imtr3d 294 . . 3 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (¬ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶) → ¬ 𝐴 ≤s 𝐵))
227226con4d 115 . 2 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 ≤s 𝐵 → (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶)))
228 leadds1im 28004 . 2 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶) → 𝐴 ≤s 𝐵))
229227, 228impbid 213 1 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 ≤s 𝐵 ↔ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 853   ∧ w3a 1092   = wceq 1547  ∃wex 1786   ∈ wcel 2119  {cab 2718   ≠ wne 2935  ∀wral 3054  ∃wrex 3064   ∪ cun 3888  ∅c0 4268  {csn 4562   class class class wbr 5079  ‘cfv 6492  (class class class)co 7363   No csur 27628   <s clts 27629   ≤s cles 27733   <<s cslts 27774   |s ccuts 27776   L cleft 27842   R cright 27843   +s cadds 27976
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-rep 5206  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rmo 3345  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-tp 4567  df-op 4569  df-ot 4571  df-uni 4846  df-int 4885  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-se 5579  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6259  df-ord 6320  df-on 6321  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7320  df-ov 7366  df-oprab 7367  df-mpo 7368  df-1st 7938  df-2nd 7939  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-1o 8402  df-2o 8403  df-nadd 8599  df-no 27631  df-lts 27632  df-bday 27633  df-les 27734  df-slts 27775  df-cuts 27777  df-0s 27824  df-made 27844  df-old 27845  df-left 27847  df-right 27848  df-norec2 27966  df-adds 27977
This theorem is referenced by:  leadds2  28007  addscan2  28010  leadds1d  28012  nnsge1  28360  zsoring  28426
  Copyright terms: Public domain W3C validator