Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sleadd1 Structured version   Visualization version   GIF version

Theorem sleadd1 34324
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 𝑥 𝑦 𝑧 𝑎 𝑏 𝑐 𝑑 𝑝 𝑞 𝑥L 𝑦L 𝑧L 𝑥R 𝑦R 𝑧R 𝑥O 𝑦O 𝑧O are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 7361 . . . . . . 7 (𝑥 = 𝑥O → (𝑥 +s 𝑧) = (𝑥O +s 𝑧))
21breq2d 5116 . . . . . 6 (𝑥 = 𝑥O → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (𝑦 +s 𝑧) <s (𝑥O +s 𝑧)))
3 breq2 5108 . . . . . 6 (𝑥 = 𝑥O → (𝑦 <s 𝑥𝑦 <s 𝑥O))
42, 3imbi12d 344 . . . . 5 (𝑥 = 𝑥O → (((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦 <s 𝑥) ↔ ((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O)))
5 oveq1 7361 . . . . . . 7 (𝑦 = 𝑦O → (𝑦 +s 𝑧) = (𝑦O +s 𝑧))
65breq1d 5114 . . . . . 6 (𝑦 = 𝑦O → ((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) ↔ (𝑦O +s 𝑧) <s (𝑥O +s 𝑧)))
7 breq1 5107 . . . . . 6 (𝑦 = 𝑦O → (𝑦 <s 𝑥O𝑦O <s 𝑥O))
86, 7imbi12d 344 . . . . 5 (𝑦 = 𝑦O → (((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ↔ ((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O)))
9 oveq2 7362 . . . . . . 7 (𝑧 = 𝑧O → (𝑦O +s 𝑧) = (𝑦O +s 𝑧O))
10 oveq2 7362 . . . . . . 7 (𝑧 = 𝑧O → (𝑥O +s 𝑧) = (𝑥O +s 𝑧O))
119, 10breq12d 5117 . . . . . 6 (𝑧 = 𝑧O → ((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) ↔ (𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O)))
1211imbi1d 341 . . . . 5 (𝑧 = 𝑧O → (((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ↔ ((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O)))
13 oveq1 7361 . . . . . . 7 (𝑥 = 𝑥O → (𝑥 +s 𝑧O) = (𝑥O +s 𝑧O))
1413breq2d 5116 . . . . . 6 (𝑥 = 𝑥O → ((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) ↔ (𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O)))
15 breq2 5108 . . . . . 6 (𝑥 = 𝑥O → (𝑦O <s 𝑥𝑦O <s 𝑥O))
1614, 15imbi12d 344 . . . . 5 (𝑥 = 𝑥O → (((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ↔ ((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O)))
17 oveq1 7361 . . . . . . 7 (𝑦 = 𝑦O → (𝑦 +s 𝑧O) = (𝑦O +s 𝑧O))
1817breq1d 5114 . . . . . 6 (𝑦 = 𝑦O → ((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) ↔ (𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O)))
19 breq1 5107 . . . . . 6 (𝑦 = 𝑦O → (𝑦 <s 𝑥𝑦O <s 𝑥))
2018, 19imbi12d 344 . . . . 5 (𝑦 = 𝑦O → (((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥) ↔ ((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥)))
2117breq1d 5114 . . . . . 6 (𝑦 = 𝑦O → ((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) ↔ (𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O)))
2221, 7imbi12d 344 . . . . 5 (𝑦 = 𝑦O → (((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O) ↔ ((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O)))
23 oveq2 7362 . . . . . . 7 (𝑧 = 𝑧O → (𝑥 +s 𝑧) = (𝑥 +s 𝑧O))
249, 23breq12d 5117 . . . . . 6 (𝑧 = 𝑧O → ((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) ↔ (𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O)))
2524imbi1d 341 . . . . 5 (𝑧 = 𝑧O → (((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥) ↔ ((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥)))
26 oveq1 7361 . . . . . . 7 (𝑥 = 𝐴 → (𝑥 +s 𝑧) = (𝐴 +s 𝑧))
2726breq2d 5116 . . . . . 6 (𝑥 = 𝐴 → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (𝑦 +s 𝑧) <s (𝐴 +s 𝑧)))
28 breq2 5108 . . . . . 6 (𝑥 = 𝐴 → (𝑦 <s 𝑥𝑦 <s 𝐴))
2927, 28imbi12d 344 . . . . 5 (𝑥 = 𝐴 → (((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦 <s 𝑥) ↔ ((𝑦 +s 𝑧) <s (𝐴 +s 𝑧) → 𝑦 <s 𝐴)))
30 oveq1 7361 . . . . . . 7 (𝑦 = 𝐵 → (𝑦 +s 𝑧) = (𝐵 +s 𝑧))
3130breq1d 5114 . . . . . 6 (𝑦 = 𝐵 → ((𝑦 +s 𝑧) <s (𝐴 +s 𝑧) ↔ (𝐵 +s 𝑧) <s (𝐴 +s 𝑧)))
32 breq1 5107 . . . . . 6 (𝑦 = 𝐵 → (𝑦 <s 𝐴𝐵 <s 𝐴))
3331, 32imbi12d 344 . . . . 5 (𝑦 = 𝐵 → (((𝑦 +s 𝑧) <s (𝐴 +s 𝑧) → 𝑦 <s 𝐴) ↔ ((𝐵 +s 𝑧) <s (𝐴 +s 𝑧) → 𝐵 <s 𝐴)))
34 oveq2 7362 . . . . . . 7 (𝑧 = 𝐶 → (𝐵 +s 𝑧) = (𝐵 +s 𝐶))
35 oveq2 7362 . . . . . . 7 (𝑧 = 𝐶 → (𝐴 +s 𝑧) = (𝐴 +s 𝐶))
3634, 35breq12d 5117 . . . . . 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 34315 . . . . . . . . . . 11 ((𝑥 No 𝑦 No 𝑧 No ) → ((𝑦 +s 𝑧) ∈ No ∧ ({𝑎 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑎 = (𝑦L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧L)}) <<s {(𝑦 +s 𝑧)} ∧ {(𝑦 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑐 = (𝑦R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧R)})))
41 simp2 1137 . . . . . . . . . . 11 (((𝑦 +s 𝑧) ∈ No ∧ ({𝑎 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑎 = (𝑦L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧L)}) <<s {(𝑦 +s 𝑧)} ∧ {(𝑦 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑐 = (𝑦R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧R)})) → ({𝑎 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑎 = (𝑦L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧L)}) <<s {(𝑦 +s 𝑧)})
4240, 41syl 17 . . . . . . . . . 10 ((𝑥 No 𝑦 No 𝑧 No ) → ({𝑎 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑎 = (𝑦L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧L)}) <<s {(𝑦 +s 𝑧)})
4340simp3d 1144 . . . . . . . . . 10 ((𝑥 No 𝑦 No 𝑧 No ) → {(𝑦 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑐 = (𝑦R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧R)}))
44 ovex 7387 . . . . . . . . . . . 12 (𝑦 +s 𝑧) ∈ V
4544snnz 4736 . . . . . . . . . . 11 {(𝑦 +s 𝑧)} ≠ ∅
46 sslttr 27142 . . . . . . . . . . 11 ((({𝑎 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑎 = (𝑦L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧L)}) <<s {(𝑦 +s 𝑧)} ∧ {(𝑦 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑐 = (𝑦R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧R)}) ∧ {(𝑦 +s 𝑧)} ≠ ∅) → ({𝑎 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑎 = (𝑦L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧L)}) <<s ({𝑐 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑐 = (𝑦R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧R)}))
4745, 46mp3an3 1450 . . . . . . . . . 10 ((({𝑎 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑎 = (𝑦L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧L)}) <<s {(𝑦 +s 𝑧)} ∧ {(𝑦 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑐 = (𝑦R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧R)})) → ({𝑎 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑎 = (𝑦L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧L)}) <<s ({𝑐 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑐 = (𝑦R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧R)}))
4842, 43, 47syl2anc 584 . . . . . . . . 9 ((𝑥 No 𝑦 No 𝑧 No ) → ({𝑎 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑎 = (𝑦L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧L)}) <<s ({𝑐 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑐 = (𝑦R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧R)}))
49 simp1 1136 . . . . . . . . . . . 12 ((𝑥 No 𝑦 No 𝑧 No ) → 𝑥 No )
5049, 39addscut 34315 . . . . . . . . . . 11 ((𝑥 No 𝑦 No 𝑧 No ) → ((𝑥 +s 𝑧) ∈ No ∧ ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧L)}) <<s {(𝑥 +s 𝑧)} ∧ {(𝑥 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧R)})))
51 simp2 1137 . . . . . . . . . . 11 (((𝑥 +s 𝑧) ∈ No ∧ ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧L)}) <<s {(𝑥 +s 𝑧)} ∧ {(𝑥 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧R)})) → ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧L)}) <<s {(𝑥 +s 𝑧)})
5250, 51syl 17 . . . . . . . . . 10 ((𝑥 No 𝑦 No 𝑧 No ) → ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧L)}) <<s {(𝑥 +s 𝑧)})
5350simp3d 1144 . . . . . . . . . 10 ((𝑥 No 𝑦 No 𝑧 No ) → {(𝑥 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧R)}))
54 ovex 7387 . . . . . . . . . . . 12 (𝑥 +s 𝑧) ∈ V
5554snnz 4736 . . . . . . . . . . 11 {(𝑥 +s 𝑧)} ≠ ∅
56 sslttr 27142 . . . . . . . . . . 11 ((({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧L)}) <<s {(𝑥 +s 𝑧)} ∧ {(𝑥 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧R)}) ∧ {(𝑥 +s 𝑧)} ≠ ∅) → ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧L)}) <<s ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧R)}))
5755, 56mp3an3 1450 . . . . . . . . . 10 ((({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧L)}) <<s {(𝑥 +s 𝑧)} ∧ {(𝑥 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧R)})) → ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧L)}) <<s ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧R)}))
5852, 53, 57syl2anc 584 . . . . . . . . 9 ((𝑥 No 𝑦 No 𝑧 No ) → ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧L)}) <<s ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧R)}))
59 addsval2 34301 . . . . . . . . . 10 ((𝑦 No 𝑧 No ) → (𝑦 +s 𝑧) = (({𝑎 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑎 = (𝑦L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧L)}) |s ({𝑐 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑐 = (𝑦R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧R)})))
60593adant1 1130 . . . . . . . . 9 ((𝑥 No 𝑦 No 𝑧 No ) → (𝑦 +s 𝑧) = (({𝑎 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑎 = (𝑦L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧L)}) |s ({𝑐 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑐 = (𝑦R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧R)})))
61 addsval2 34301 . . . . . . . . . 10 ((𝑥 No 𝑧 No ) → (𝑥 +s 𝑧) = (({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧L)}) |s ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧R)})))
62613adant2 1131 . . . . . . . . 9 ((𝑥 No 𝑦 No 𝑧 No ) → (𝑥 +s 𝑧) = (({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧L)}) |s ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧R)})))
63 sltrec 27155 . . . . . . . . 9 (((({𝑎 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑎 = (𝑦L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧L)}) <<s ({𝑐 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑐 = (𝑦R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧R)}) ∧ ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧L)}) <<s ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧R)})) ∧ ((𝑦 +s 𝑧) = (({𝑎 ∣ ∃𝑦L ∈ ( L ‘𝑦)𝑎 = (𝑦L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧L)}) |s ({𝑐 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑐 = (𝑦R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧R)})) ∧ (𝑥 +s 𝑧) = (({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧L)}) |s ({𝑐 ∣ ∃𝑥R ∈ ( R ‘𝑥)𝑐 = (𝑥R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧R)})))) → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (∃𝑝 ∈ ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧L)})(𝑦 +s 𝑧) ≤s 𝑝 ∨ ∃𝑞 ∈ ({𝑐 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑐 = (𝑦R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧R)})𝑞 ≤s (𝑥 +s 𝑧))))
6448, 58, 60, 62, 63syl22anc 837 . . . . . . . 8 ((𝑥 No 𝑦 No 𝑧 No ) → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (∃𝑝 ∈ ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧L)})(𝑦 +s 𝑧) ≤s 𝑝 ∨ ∃𝑞 ∈ ({𝑐 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑐 = (𝑦R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧R)})𝑞 ≤s (𝑥 +s 𝑧))))
6564adantr 481 . . . . . . 7 (((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (∃𝑝 ∈ ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧L)})(𝑦 +s 𝑧) ≤s 𝑝 ∨ ∃𝑞 ∈ ({𝑐 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑐 = (𝑦R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧R)})𝑞 ≤s (𝑥 +s 𝑧))))
66 rexun 4149 . . . . . . . . . 10 (∃𝑝 ∈ ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧L)})(𝑦 +s 𝑧) ≤s 𝑝 ↔ (∃𝑝 ∈ {𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s 𝑧)} (𝑦 +s 𝑧) ≤s 𝑝 ∨ ∃𝑝 ∈ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧L)} (𝑦 +s 𝑧) ≤s 𝑝))
67 eqeq1 2740 . . . . . . . . . . . . . 14 (𝑎 = 𝑝 → (𝑎 = (𝑥L +s 𝑧) ↔ 𝑝 = (𝑥L +s 𝑧)))
6867rexbidv 3174 . . . . . . . . . . . . 13 (𝑎 = 𝑝 → (∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s 𝑧) ↔ ∃𝑥L ∈ ( L ‘𝑥)𝑝 = (𝑥L +s 𝑧)))
6968rexab 3651 . . . . . . . . . . . 12 (∃𝑝 ∈ {𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s 𝑧)} (𝑦 +s 𝑧) ≤s 𝑝 ↔ ∃𝑝(∃𝑥L ∈ ( L ‘𝑥)𝑝 = (𝑥L +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
70 rexcom4 3270 . . . . . . . . . . . . . 14 (∃𝑥L ∈ ( L ‘𝑥)∃𝑝(𝑝 = (𝑥L +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝𝑥L ∈ ( L ‘𝑥)(𝑝 = (𝑥L +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
71 r19.41v 3184 . . . . . . . . . . . . . . 15 (∃𝑥L ∈ ( L ‘𝑥)(𝑝 = (𝑥L +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ (∃𝑥L ∈ ( L ‘𝑥)𝑝 = (𝑥L +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
7271exbii 1850 . . . . . . . . . . . . . 14 (∃𝑝𝑥L ∈ ( L ‘𝑥)(𝑝 = (𝑥L +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝(∃𝑥L ∈ ( L ‘𝑥)𝑝 = (𝑥L +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
7370, 72bitri 274 . . . . . . . . . . . . 13 (∃𝑥L ∈ ( L ‘𝑥)∃𝑝(𝑝 = (𝑥L +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝(∃𝑥L ∈ ( L ‘𝑥)𝑝 = (𝑥L +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
74 ovex 7387 . . . . . . . . . . . . . . 15 (𝑥L +s 𝑧) ∈ V
75 breq2 5108 . . . . . . . . . . . . . . 15 (𝑝 = (𝑥L +s 𝑧) → ((𝑦 +s 𝑧) ≤s 𝑝 ↔ (𝑦 +s 𝑧) ≤s (𝑥L +s 𝑧)))
7674, 75ceqsexv 3493 . . . . . . . . . . . . . 14 (∃𝑝(𝑝 = (𝑥L +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ (𝑦 +s 𝑧) ≤s (𝑥L +s 𝑧))
7776rexbii 3096 . . . . . . . . . . . . 13 (∃𝑥L ∈ ( L ‘𝑥)∃𝑝(𝑝 = (𝑥L +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑥L ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥L +s 𝑧))
7873, 77bitr3i 276 . . . . . . . . . . . 12 (∃𝑝(∃𝑥L ∈ ( L ‘𝑥)𝑝 = (𝑥L +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑥L ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥L +s 𝑧))
7969, 78bitri 274 . . . . . . . . . . 11 (∃𝑝 ∈ {𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s 𝑧)} (𝑦 +s 𝑧) ≤s 𝑝 ↔ ∃𝑥L ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥L +s 𝑧))
80 eqeq1 2740 . . . . . . . . . . . . . 14 (𝑏 = 𝑝 → (𝑏 = (𝑥 +s 𝑧L) ↔ 𝑝 = (𝑥 +s 𝑧L)))
8180rexbidv 3174 . . . . . . . . . . . . 13 (𝑏 = 𝑝 → (∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧L) ↔ ∃𝑧L ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧L)))
8281rexab 3651 . . . . . . . . . . . 12 (∃𝑝 ∈ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧L)} (𝑦 +s 𝑧) ≤s 𝑝 ↔ ∃𝑝(∃𝑧L ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧L) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
83 rexcom4 3270 . . . . . . . . . . . . . 14 (∃𝑧L ∈ ( L ‘𝑧)∃𝑝(𝑝 = (𝑥 +s 𝑧L) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝𝑧L ∈ ( L ‘𝑧)(𝑝 = (𝑥 +s 𝑧L) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
84 r19.41v 3184 . . . . . . . . . . . . . . 15 (∃𝑧L ∈ ( L ‘𝑧)(𝑝 = (𝑥 +s 𝑧L) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ (∃𝑧L ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧L) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
8584exbii 1850 . . . . . . . . . . . . . 14 (∃𝑝𝑧L ∈ ( L ‘𝑧)(𝑝 = (𝑥 +s 𝑧L) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝(∃𝑧L ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧L) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
8683, 85bitri 274 . . . . . . . . . . . . 13 (∃𝑧L ∈ ( L ‘𝑧)∃𝑝(𝑝 = (𝑥 +s 𝑧L) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝(∃𝑧L ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧L) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
87 ovex 7387 . . . . . . . . . . . . . . 15 (𝑥 +s 𝑧L) ∈ V
88 breq2 5108 . . . . . . . . . . . . . . 15 (𝑝 = (𝑥 +s 𝑧L) → ((𝑦 +s 𝑧) ≤s 𝑝 ↔ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L)))
8987, 88ceqsexv 3493 . . . . . . . . . . . . . 14 (∃𝑝(𝑝 = (𝑥 +s 𝑧L) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L))
9089rexbii 3096 . . . . . . . . . . . . 13 (∃𝑧L ∈ ( L ‘𝑧)∃𝑝(𝑝 = (𝑥 +s 𝑧L) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑧L ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L))
9186, 90bitr3i 276 . . . . . . . . . . . 12 (∃𝑝(∃𝑧L ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧L) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑧L ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L))
9282, 91bitri 274 . . . . . . . . . . 11 (∃𝑝 ∈ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧L)} (𝑦 +s 𝑧) ≤s 𝑝 ↔ ∃𝑧L ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L))
9379, 92orbi12i 913 . . . . . . . . . 10 ((∃𝑝 ∈ {𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s 𝑧)} (𝑦 +s 𝑧) ≤s 𝑝 ∨ ∃𝑝 ∈ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧L)} (𝑦 +s 𝑧) ≤s 𝑝) ↔ (∃𝑥L ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥L +s 𝑧) ∨ ∃𝑧L ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L)))
9466, 93bitri 274 . . . . . . . . 9 (∃𝑝 ∈ ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧L)})(𝑦 +s 𝑧) ≤s 𝑝 ↔ (∃𝑥L ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥L +s 𝑧) ∨ ∃𝑧L ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L)))
95 simpll2 1213 . . . . . . . . . . . 12 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑥L ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥L +s 𝑧))) → 𝑦 No )
96 leftssno 27206 . . . . . . . . . . . . . . 15 ( L ‘𝑥) ⊆ No
9796sseli 3939 . . . . . . . . . . . . . 14 (𝑥L ∈ ( L ‘𝑥) → 𝑥L No )
9897adantr 481 . . . . . . . . . . . . 13 ((𝑥L ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥L +s 𝑧)) → 𝑥L No )
9998adantl 482 . . . . . . . . . . . 12 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑥L ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥L +s 𝑧))) → 𝑥L No )
100 simpll1 1212 . . . . . . . . . . . 12 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑥L ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥L +s 𝑧))) → 𝑥 No )
101 simprr 771 . . . . . . . . . . . . 13 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑥L ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥L +s 𝑧))) → (𝑦 +s 𝑧) ≤s (𝑥L +s 𝑧))
102 simpll3 1214 . . . . . . . . . . . . . 14 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑥L ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥L +s 𝑧))) → 𝑧 No )
103 sleadd1im 34322 . . . . . . . . . . . . . 14 ((𝑦 No 𝑥L No 𝑧 No ) → ((𝑦 +s 𝑧) ≤s (𝑥L +s 𝑧) → 𝑦 ≤s 𝑥L))
10495, 99, 102, 103syl3anc 1371 . . . . . . . . . . . . 13 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑥L ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥L +s 𝑧))) → ((𝑦 +s 𝑧) ≤s (𝑥L +s 𝑧) → 𝑦 ≤s 𝑥L))
105101, 104mpd 15 . . . . . . . . . . . 12 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑥L ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥L +s 𝑧))) → 𝑦 ≤s 𝑥L)
106 leftval 27189 . . . . . . . . . . . . . . . 16 ( L ‘𝑥) = {𝑥L ∈ ( O ‘( bday 𝑥)) ∣ 𝑥L <s 𝑥}
107106rabeq2i 3428 . . . . . . . . . . . . . . 15 (𝑥L ∈ ( L ‘𝑥) ↔ (𝑥L ∈ ( O ‘( bday 𝑥)) ∧ 𝑥L <s 𝑥))
108107simprbi 497 . . . . . . . . . . . . . 14 (𝑥L ∈ ( L ‘𝑥) → 𝑥L <s 𝑥)
109108adantr 481 . . . . . . . . . . . . 13 ((𝑥L ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥L +s 𝑧)) → 𝑥L <s 𝑥)
110109adantl 482 . . . . . . . . . . . 12 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑥L ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥L +s 𝑧))) → 𝑥L <s 𝑥)
11195, 99, 100, 105, 110slelttrd 27105 . . . . . . . . . . 11 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑥L ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥L +s 𝑧))) → 𝑦 <s 𝑥)
112111rexlimdvaa 3152 . . . . . . . . . 10 (((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) → (∃𝑥L ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥L +s 𝑧) → 𝑦 <s 𝑥))
113 simpll2 1213 . . . . . . . . . . . . . 14 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧L ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L))) → 𝑦 No )
114 leftssno 27206 . . . . . . . . . . . . . . . . 17 ( L ‘𝑧) ⊆ No
115114sseli 3939 . . . . . . . . . . . . . . . 16 (𝑧L ∈ ( L ‘𝑧) → 𝑧L No )
116115adantr 481 . . . . . . . . . . . . . . 15 ((𝑧L ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L)) → 𝑧L No )
117116adantl 482 . . . . . . . . . . . . . 14 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧L ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L))) → 𝑧L No )
118113, 117addscld 34316 . . . . . . . . . . . . 13 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧L ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L))) → (𝑦 +s 𝑧L) ∈ No )
119 simpll3 1214 . . . . . . . . . . . . . 14 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧L ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L))) → 𝑧 No )
120113, 119addscld 34316 . . . . . . . . . . . . 13 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧L ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L))) → (𝑦 +s 𝑧) ∈ No )
121 simpll1 1212 . . . . . . . . . . . . . 14 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧L ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L))) → 𝑥 No )
122121, 117addscld 34316 . . . . . . . . . . . . 13 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧L ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L))) → (𝑥 +s 𝑧L) ∈ No )
123 leftval 27189 . . . . . . . . . . . . . . . . . 18 ( L ‘𝑧) = {𝑧L ∈ ( O ‘( bday 𝑧)) ∣ 𝑧L <s 𝑧}
124123rabeq2i 3428 . . . . . . . . . . . . . . . . 17 (𝑧L ∈ ( L ‘𝑧) ↔ (𝑧L ∈ ( O ‘( bday 𝑧)) ∧ 𝑧L <s 𝑧))
125124simprbi 497 . . . . . . . . . . . . . . . 16 (𝑧L ∈ ( L ‘𝑧) → 𝑧L <s 𝑧)
126125adantr 481 . . . . . . . . . . . . . . 15 ((𝑧L ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L)) → 𝑧L <s 𝑧)
127126adantl 482 . . . . . . . . . . . . . 14 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧L ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L))) → 𝑧L <s 𝑧)
128 sltadd2im 34321 . . . . . . . . . . . . . . 15 ((𝑧L No 𝑧 No 𝑦 No ) → (𝑧L <s 𝑧 → (𝑦 +s 𝑧L) <s (𝑦 +s 𝑧)))
129117, 119, 113, 128syl3anc 1371 . . . . . . . . . . . . . 14 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧L ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L))) → (𝑧L <s 𝑧 → (𝑦 +s 𝑧L) <s (𝑦 +s 𝑧)))
130127, 129mpd 15 . . . . . . . . . . . . 13 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧L ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L))) → (𝑦 +s 𝑧L) <s (𝑦 +s 𝑧))
131 simprr 771 . . . . . . . . . . . . 13 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧L ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L))) → (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L))
132118, 120, 122, 130, 131sltletrd 27104 . . . . . . . . . . . 12 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧L ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L))) → (𝑦 +s 𝑧L) <s (𝑥 +s 𝑧L))
133 oveq2 7362 . . . . . . . . . . . . . . 15 (𝑧O = 𝑧L → (𝑦 +s 𝑧O) = (𝑦 +s 𝑧L))
134 oveq2 7362 . . . . . . . . . . . . . . 15 (𝑧O = 𝑧L → (𝑥 +s 𝑧O) = (𝑥 +s 𝑧L))
135133, 134breq12d 5117 . . . . . . . . . . . . . 14 (𝑧O = 𝑧L → ((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) ↔ (𝑦 +s 𝑧L) <s (𝑥 +s 𝑧L)))
136135imbi1d 341 . . . . . . . . . . . . 13 (𝑧O = 𝑧L → (((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥) ↔ ((𝑦 +s 𝑧L) <s (𝑥 +s 𝑧L) → 𝑦 <s 𝑥)))
137 simplr3 1217 . . . . . . . . . . . . 13 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧L ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L))) → ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))
138 simprl 769 . . . . . . . . . . . . . 14 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧L ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L))) → 𝑧L ∈ ( L ‘𝑧))
139 elun1 4135 . . . . . . . . . . . . . 14 (𝑧L ∈ ( L ‘𝑧) → 𝑧L ∈ (( L ‘𝑧) ∪ ( R ‘𝑧)))
140138, 139syl 17 . . . . . . . . . . . . 13 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧L ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L))) → 𝑧L ∈ (( L ‘𝑧) ∪ ( R ‘𝑧)))
141136, 137, 140rspcdva 3581 . . . . . . . . . . . 12 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧L ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L))) → ((𝑦 +s 𝑧L) <s (𝑥 +s 𝑧L) → 𝑦 <s 𝑥))
142132, 141mpd 15 . . . . . . . . . . 11 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧L ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L))) → 𝑦 <s 𝑥)
143142rexlimdvaa 3152 . . . . . . . . . 10 (((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) → (∃𝑧L ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L) → 𝑦 <s 𝑥))
144112, 143jaod 857 . . . . . . . . 9 (((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) → ((∃𝑥L ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥L +s 𝑧) ∨ ∃𝑧L ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L)) → 𝑦 <s 𝑥))
14594, 144biimtrid 241 . . . . . . . 8 (((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) → (∃𝑝 ∈ ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧L)})(𝑦 +s 𝑧) ≤s 𝑝𝑦 <s 𝑥))
146 rexun 4149 . . . . . . . . . 10 (∃𝑞 ∈ ({𝑐 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑐 = (𝑦R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧R)})𝑞 ≤s (𝑥 +s 𝑧) ↔ (∃𝑞 ∈ {𝑐 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑐 = (𝑦R +s 𝑧)}𝑞 ≤s (𝑥 +s 𝑧) ∨ ∃𝑞 ∈ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧R)}𝑞 ≤s (𝑥 +s 𝑧)))
147 eqeq1 2740 . . . . . . . . . . . . . 14 (𝑐 = 𝑞 → (𝑐 = (𝑦R +s 𝑧) ↔ 𝑞 = (𝑦R +s 𝑧)))
148147rexbidv 3174 . . . . . . . . . . . . 13 (𝑐 = 𝑞 → (∃𝑦R ∈ ( R ‘𝑦)𝑐 = (𝑦R +s 𝑧) ↔ ∃𝑦R ∈ ( R ‘𝑦)𝑞 = (𝑦R +s 𝑧)))
149148rexab 3651 . . . . . . . . . . . 12 (∃𝑞 ∈ {𝑐 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑐 = (𝑦R +s 𝑧)}𝑞 ≤s (𝑥 +s 𝑧) ↔ ∃𝑞(∃𝑦R ∈ ( R ‘𝑦)𝑞 = (𝑦R +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
150 rexcom4 3270 . . . . . . . . . . . . . 14 (∃𝑦R ∈ ( R ‘𝑦)∃𝑞(𝑞 = (𝑦R +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞𝑦R ∈ ( R ‘𝑦)(𝑞 = (𝑦R +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
151 r19.41v 3184 . . . . . . . . . . . . . . 15 (∃𝑦R ∈ ( R ‘𝑦)(𝑞 = (𝑦R +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ (∃𝑦R ∈ ( R ‘𝑦)𝑞 = (𝑦R +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
152151exbii 1850 . . . . . . . . . . . . . 14 (∃𝑞𝑦R ∈ ( R ‘𝑦)(𝑞 = (𝑦R +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞(∃𝑦R ∈ ( R ‘𝑦)𝑞 = (𝑦R +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
153150, 152bitri 274 . . . . . . . . . . . . 13 (∃𝑦R ∈ ( R ‘𝑦)∃𝑞(𝑞 = (𝑦R +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞(∃𝑦R ∈ ( R ‘𝑦)𝑞 = (𝑦R +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
154 ovex 7387 . . . . . . . . . . . . . . 15 (𝑦R +s 𝑧) ∈ V
155 breq1 5107 . . . . . . . . . . . . . . 15 (𝑞 = (𝑦R +s 𝑧) → (𝑞 ≤s (𝑥 +s 𝑧) ↔ (𝑦R +s 𝑧) ≤s (𝑥 +s 𝑧)))
156154, 155ceqsexv 3493 . . . . . . . . . . . . . 14 (∃𝑞(𝑞 = (𝑦R +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ (𝑦R +s 𝑧) ≤s (𝑥 +s 𝑧))
157156rexbii 3096 . . . . . . . . . . . . 13 (∃𝑦R ∈ ( R ‘𝑦)∃𝑞(𝑞 = (𝑦R +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑦R ∈ ( R ‘𝑦)(𝑦R +s 𝑧) ≤s (𝑥 +s 𝑧))
158153, 157bitr3i 276 . . . . . . . . . . . 12 (∃𝑞(∃𝑦R ∈ ( R ‘𝑦)𝑞 = (𝑦R +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑦R ∈ ( R ‘𝑦)(𝑦R +s 𝑧) ≤s (𝑥 +s 𝑧))
159149, 158bitri 274 . . . . . . . . . . 11 (∃𝑞 ∈ {𝑐 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑐 = (𝑦R +s 𝑧)}𝑞 ≤s (𝑥 +s 𝑧) ↔ ∃𝑦R ∈ ( R ‘𝑦)(𝑦R +s 𝑧) ≤s (𝑥 +s 𝑧))
160 eqeq1 2740 . . . . . . . . . . . . . 14 (𝑑 = 𝑞 → (𝑑 = (𝑦 +s 𝑧R) ↔ 𝑞 = (𝑦 +s 𝑧R)))
161160rexbidv 3174 . . . . . . . . . . . . 13 (𝑑 = 𝑞 → (∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧R) ↔ ∃𝑧R ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧R)))
162161rexab 3651 . . . . . . . . . . . 12 (∃𝑞 ∈ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧R)}𝑞 ≤s (𝑥 +s 𝑧) ↔ ∃𝑞(∃𝑧R ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧R) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
163 rexcom4 3270 . . . . . . . . . . . . . 14 (∃𝑧R ∈ ( R ‘𝑧)∃𝑞(𝑞 = (𝑦 +s 𝑧R) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞𝑧R ∈ ( R ‘𝑧)(𝑞 = (𝑦 +s 𝑧R) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
164 r19.41v 3184 . . . . . . . . . . . . . . 15 (∃𝑧R ∈ ( R ‘𝑧)(𝑞 = (𝑦 +s 𝑧R) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ (∃𝑧R ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧R) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
165164exbii 1850 . . . . . . . . . . . . . 14 (∃𝑞𝑧R ∈ ( R ‘𝑧)(𝑞 = (𝑦 +s 𝑧R) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞(∃𝑧R ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧R) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
166163, 165bitri 274 . . . . . . . . . . . . 13 (∃𝑧R ∈ ( R ‘𝑧)∃𝑞(𝑞 = (𝑦 +s 𝑧R) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞(∃𝑧R ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧R) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
167 ovex 7387 . . . . . . . . . . . . . . 15 (𝑦 +s 𝑧R) ∈ V
168 breq1 5107 . . . . . . . . . . . . . . 15 (𝑞 = (𝑦 +s 𝑧R) → (𝑞 ≤s (𝑥 +s 𝑧) ↔ (𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧)))
169167, 168ceqsexv 3493 . . . . . . . . . . . . . 14 (∃𝑞(𝑞 = (𝑦 +s 𝑧R) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ (𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧))
170169rexbii 3096 . . . . . . . . . . . . 13 (∃𝑧R ∈ ( R ‘𝑧)∃𝑞(𝑞 = (𝑦 +s 𝑧R) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑧R ∈ ( R ‘𝑧)(𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧))
171166, 170bitr3i 276 . . . . . . . . . . . 12 (∃𝑞(∃𝑧R ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧R) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑧R ∈ ( R ‘𝑧)(𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧))
172162, 171bitri 274 . . . . . . . . . . 11 (∃𝑞 ∈ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧R)}𝑞 ≤s (𝑥 +s 𝑧) ↔ ∃𝑧R ∈ ( R ‘𝑧)(𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧))
173159, 172orbi12i 913 . . . . . . . . . 10 ((∃𝑞 ∈ {𝑐 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑐 = (𝑦R +s 𝑧)}𝑞 ≤s (𝑥 +s 𝑧) ∨ ∃𝑞 ∈ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧R)}𝑞 ≤s (𝑥 +s 𝑧)) ↔ (∃𝑦R ∈ ( R ‘𝑦)(𝑦R +s 𝑧) ≤s (𝑥 +s 𝑧) ∨ ∃𝑧R ∈ ( R ‘𝑧)(𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧)))
174146, 173bitri 274 . . . . . . . . 9 (∃𝑞 ∈ ({𝑐 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑐 = (𝑦R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧R)})𝑞 ≤s (𝑥 +s 𝑧) ↔ (∃𝑦R ∈ ( R ‘𝑦)(𝑦R +s 𝑧) ≤s (𝑥 +s 𝑧) ∨ ∃𝑧R ∈ ( R ‘𝑧)(𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧)))
175 simpll2 1213 . . . . . . . . . . . 12 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑦R ∈ ( R ‘𝑦) ∧ (𝑦R +s 𝑧) ≤s (𝑥 +s 𝑧))) → 𝑦 No )
176 rightssno 27207 . . . . . . . . . . . . . . 15 ( R ‘𝑦) ⊆ No
177176sseli 3939 . . . . . . . . . . . . . 14 (𝑦R ∈ ( R ‘𝑦) → 𝑦R No )
178177adantr 481 . . . . . . . . . . . . 13 ((𝑦R ∈ ( R ‘𝑦) ∧ (𝑦R +s 𝑧) ≤s (𝑥 +s 𝑧)) → 𝑦R No )
179178adantl 482 . . . . . . . . . . . 12 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑦R ∈ ( R ‘𝑦) ∧ (𝑦R +s 𝑧) ≤s (𝑥 +s 𝑧))) → 𝑦R No )
180 simpll1 1212 . . . . . . . . . . . 12 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑦R ∈ ( R ‘𝑦) ∧ (𝑦R +s 𝑧) ≤s (𝑥 +s 𝑧))) → 𝑥 No )
181 rightval 27190 . . . . . . . . . . . . . . . 16 ( R ‘𝑦) = {𝑦R ∈ ( O ‘( bday 𝑦)) ∣ 𝑦 <s 𝑦R}
182181rabeq2i 3428 . . . . . . . . . . . . . . 15 (𝑦R ∈ ( R ‘𝑦) ↔ (𝑦R ∈ ( O ‘( bday 𝑦)) ∧ 𝑦 <s 𝑦R))
183182simprbi 497 . . . . . . . . . . . . . 14 (𝑦R ∈ ( R ‘𝑦) → 𝑦 <s 𝑦R)
184183adantr 481 . . . . . . . . . . . . 13 ((𝑦R ∈ ( R ‘𝑦) ∧ (𝑦R +s 𝑧) ≤s (𝑥 +s 𝑧)) → 𝑦 <s 𝑦R)
185184adantl 482 . . . . . . . . . . . 12 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑦R ∈ ( R ‘𝑦) ∧ (𝑦R +s 𝑧) ≤s (𝑥 +s 𝑧))) → 𝑦 <s 𝑦R)
186 simprr 771 . . . . . . . . . . . . 13 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑦R ∈ ( R ‘𝑦) ∧ (𝑦R +s 𝑧) ≤s (𝑥 +s 𝑧))) → (𝑦R +s 𝑧) ≤s (𝑥 +s 𝑧))
187 simpll3 1214 . . . . . . . . . . . . . 14 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑦R ∈ ( R ‘𝑦) ∧ (𝑦R +s 𝑧) ≤s (𝑥 +s 𝑧))) → 𝑧 No )
188 sleadd1im 34322 . . . . . . . . . . . . . 14 ((𝑦R No 𝑥 No 𝑧 No ) → ((𝑦R +s 𝑧) ≤s (𝑥 +s 𝑧) → 𝑦R ≤s 𝑥))
189179, 180, 187, 188syl3anc 1371 . . . . . . . . . . . . 13 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑦R ∈ ( R ‘𝑦) ∧ (𝑦R +s 𝑧) ≤s (𝑥 +s 𝑧))) → ((𝑦R +s 𝑧) ≤s (𝑥 +s 𝑧) → 𝑦R ≤s 𝑥))
190186, 189mpd 15 . . . . . . . . . . . 12 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑦R ∈ ( R ‘𝑦) ∧ (𝑦R +s 𝑧) ≤s (𝑥 +s 𝑧))) → 𝑦R ≤s 𝑥)
191175, 179, 180, 185, 190sltletrd 27104 . . . . . . . . . . 11 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑦R ∈ ( R ‘𝑦) ∧ (𝑦R +s 𝑧) ≤s (𝑥 +s 𝑧))) → 𝑦 <s 𝑥)
192191rexlimdvaa 3152 . . . . . . . . . 10 (((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) → (∃𝑦R ∈ ( R ‘𝑦)(𝑦R +s 𝑧) ≤s (𝑥 +s 𝑧) → 𝑦 <s 𝑥))
193 simpll2 1213 . . . . . . . . . . . . . 14 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧R ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧))) → 𝑦 No )
194 rightssno 27207 . . . . . . . . . . . . . . . . 17 ( R ‘𝑧) ⊆ No
195194sseli 3939 . . . . . . . . . . . . . . . 16 (𝑧R ∈ ( R ‘𝑧) → 𝑧R No )
196195adantr 481 . . . . . . . . . . . . . . 15 ((𝑧R ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧)) → 𝑧R No )
197196adantl 482 . . . . . . . . . . . . . 14 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧R ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧))) → 𝑧R No )
198193, 197addscld 34316 . . . . . . . . . . . . 13 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧R ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧))) → (𝑦 +s 𝑧R) ∈ No )
199 simpll1 1212 . . . . . . . . . . . . . 14 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧R ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧))) → 𝑥 No )
200 simpll3 1214 . . . . . . . . . . . . . 14 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧R ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧))) → 𝑧 No )
201199, 200addscld 34316 . . . . . . . . . . . . 13 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧R ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧))) → (𝑥 +s 𝑧) ∈ No )
202199, 197addscld 34316 . . . . . . . . . . . . 13 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧R ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧))) → (𝑥 +s 𝑧R) ∈ No )
203 simprr 771 . . . . . . . . . . . . 13 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧R ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧))) → (𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧))
204200, 197, 1993jca 1128 . . . . . . . . . . . . . 14 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧R ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧))) → (𝑧 No 𝑧R No 𝑥 No ))
205 rightval 27190 . . . . . . . . . . . . . . . . . 18 ( R ‘𝑧) = {𝑧R ∈ ( O ‘( bday 𝑧)) ∣ 𝑧 <s 𝑧R}
206205rabeq2i 3428 . . . . . . . . . . . . . . . . 17 (𝑧R ∈ ( R ‘𝑧) ↔ (𝑧R ∈ ( O ‘( bday 𝑧)) ∧ 𝑧 <s 𝑧R))
207206simprbi 497 . . . . . . . . . . . . . . . 16 (𝑧R ∈ ( R ‘𝑧) → 𝑧 <s 𝑧R)
208207adantr 481 . . . . . . . . . . . . . . 15 ((𝑧R ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧)) → 𝑧 <s 𝑧R)
209208adantl 482 . . . . . . . . . . . . . 14 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧R ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧))) → 𝑧 <s 𝑧R)
210 sltadd2im 34321 . . . . . . . . . . . . . 14 ((𝑧 No 𝑧R No 𝑥 No ) → (𝑧 <s 𝑧R → (𝑥 +s 𝑧) <s (𝑥 +s 𝑧R)))
211204, 209, 210sylc 65 . . . . . . . . . . . . 13 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧R ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧))) → (𝑥 +s 𝑧) <s (𝑥 +s 𝑧R))
212198, 201, 202, 203, 211slelttrd 27105 . . . . . . . . . . . 12 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧R ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧))) → (𝑦 +s 𝑧R) <s (𝑥 +s 𝑧R))
213 oveq2 7362 . . . . . . . . . . . . . . 15 (𝑧O = 𝑧R → (𝑦 +s 𝑧O) = (𝑦 +s 𝑧R))
214 oveq2 7362 . . . . . . . . . . . . . . 15 (𝑧O = 𝑧R → (𝑥 +s 𝑧O) = (𝑥 +s 𝑧R))
215213, 214breq12d 5117 . . . . . . . . . . . . . 14 (𝑧O = 𝑧R → ((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) ↔ (𝑦 +s 𝑧R) <s (𝑥 +s 𝑧R)))
216215imbi1d 341 . . . . . . . . . . . . 13 (𝑧O = 𝑧R → (((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥) ↔ ((𝑦 +s 𝑧R) <s (𝑥 +s 𝑧R) → 𝑦 <s 𝑥)))
217 simplr3 1217 . . . . . . . . . . . . 13 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧R ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧))) → ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))
218 simprl 769 . . . . . . . . . . . . . 14 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧R ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧))) → 𝑧R ∈ ( R ‘𝑧))
219 elun2 4136 . . . . . . . . . . . . . 14 (𝑧R ∈ ( R ‘𝑧) → 𝑧R ∈ (( L ‘𝑧) ∪ ( R ‘𝑧)))
220218, 219syl 17 . . . . . . . . . . . . 13 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧R ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧))) → 𝑧R ∈ (( L ‘𝑧) ∪ ( R ‘𝑧)))
221216, 217, 220rspcdva 3581 . . . . . . . . . . . 12 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧R ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧))) → ((𝑦 +s 𝑧R) <s (𝑥 +s 𝑧R) → 𝑦 <s 𝑥))
222212, 221mpd 15 . . . . . . . . . . 11 ((((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) ∧ (𝑧R ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧))) → 𝑦 <s 𝑥)
223222rexlimdvaa 3152 . . . . . . . . . 10 (((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) → (∃𝑧R ∈ ( R ‘𝑧)(𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧) → 𝑦 <s 𝑥))
224192, 223jaod 857 . . . . . . . . 9 (((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) → ((∃𝑦R ∈ ( R ‘𝑦)(𝑦R +s 𝑧) ≤s (𝑥 +s 𝑧) ∨ ∃𝑧R ∈ ( R ‘𝑧)(𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧)) → 𝑦 <s 𝑥))
225174, 224biimtrid 241 . . . . . . . 8 (((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) → (∃𝑞 ∈ ({𝑐 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑐 = (𝑦R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧R)})𝑞 ≤s (𝑥 +s 𝑧) → 𝑦 <s 𝑥))
226145, 225jaod 857 . . . . . . 7 (((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) → ((∃𝑝 ∈ ({𝑎 ∣ ∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧L)})(𝑦 +s 𝑧) ≤s 𝑝 ∨ ∃𝑞 ∈ ({𝑐 ∣ ∃𝑦R ∈ ( R ‘𝑦)𝑐 = (𝑦R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧R)})𝑞 ≤s (𝑥 +s 𝑧)) → 𝑦 <s 𝑥))
22765, 226sylbid 239 . . . . . 6 (((𝑥 No 𝑦 No 𝑧 No ) ∧ ((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥))) → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦 <s 𝑥))
228227ex 413 . . . . 5 ((𝑥 No 𝑦 No 𝑧 No ) → (((∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦O <s 𝑥O) ∧ ∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) → 𝑦 <s 𝑥O)) ∧ (∀𝑥O ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥) ∧ ∀𝑦O ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥)) ∧ ∀𝑧O ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥)) → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦 <s 𝑥)))
2294, 8, 12, 16, 20, 22, 25, 29, 33, 37, 228no3inds 27266 . . . 4 ((𝐴 No 𝐵 No 𝐶 No ) → ((𝐵 +s 𝐶) <s (𝐴 +s 𝐶) → 𝐵 <s 𝐴))
230 addscl 34317 . . . . . 6 ((𝐵 No 𝐶 No ) → (𝐵 +s 𝐶) ∈ No )
2312303adant1 1130 . . . . 5 ((𝐴 No 𝐵 No 𝐶 No ) → (𝐵 +s 𝐶) ∈ No )
232 addscl 34317 . . . . . 6 ((𝐴 No 𝐶 No ) → (𝐴 +s 𝐶) ∈ No )
2332323adant2 1131 . . . . 5 ((𝐴 No 𝐵 No 𝐶 No ) → (𝐴 +s 𝐶) ∈ No )
234 sltnle 27097 . . . . 5 (((𝐵 +s 𝐶) ∈ No ∧ (𝐴 +s 𝐶) ∈ No ) → ((𝐵 +s 𝐶) <s (𝐴 +s 𝐶) ↔ ¬ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶)))
235231, 233, 234syl2anc 584 . . . 4 ((𝐴 No 𝐵 No 𝐶 No ) → ((𝐵 +s 𝐶) <s (𝐴 +s 𝐶) ↔ ¬ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶)))
236 sltnle 27097 . . . . . 6 ((𝐵 No 𝐴 No ) → (𝐵 <s 𝐴 ↔ ¬ 𝐴 ≤s 𝐵))
237236ancoms 459 . . . . 5 ((𝐴 No 𝐵 No ) → (𝐵 <s 𝐴 ↔ ¬ 𝐴 ≤s 𝐵))
2382373adant3 1132 . . . 4 ((𝐴 No 𝐵 No 𝐶 No ) → (𝐵 <s 𝐴 ↔ ¬ 𝐴 ≤s 𝐵))
239229, 235, 2383imtr3d 292 . . 3 ((𝐴 No 𝐵 No 𝐶 No ) → (¬ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶) → ¬ 𝐴 ≤s 𝐵))
240239con4d 115 . 2 ((𝐴 No 𝐵 No 𝐶 No ) → (𝐴 ≤s 𝐵 → (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶)))
241 sleadd1im 34322 . 2 ((𝐴 No 𝐵 No 𝐶 No ) → ((𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶) → 𝐴 ≤s 𝐵))
242240, 241impbid 211 1 ((𝐴 No 𝐵 No 𝐶 No ) → (𝐴 ≤s 𝐵 ↔ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3a 1087   = wceq 1541  wex 1781  wcel 2106  {cab 2713  wne 2942  wral 3063  wrex 3072  cun 3907  c0 4281  {csn 4585   class class class wbr 5104  cfv 6494  (class class class)co 7354   No csur 26984   <s cslt 26985   bday cbday 26986   ≤s csle 27088   <<s csslt 27116   |s cscut 27118   O cold 27169   L cleft 27171   R cright 27172   +s cadds 34297
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5241  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7669
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2888  df-ne 2943  df-ral 3064  df-rex 3073  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-pss 3928  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-ot 4594  df-uni 4865  df-int 4907  df-iun 4955  df-br 5105  df-opab 5167  df-mpt 5188  df-tr 5222  df-id 5530  df-eprel 5536  df-po 5544  df-so 5545  df-fr 5587  df-se 5588  df-we 5589  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6252  df-ord 6319  df-on 6320  df-suc 6322  df-iota 6446  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-riota 7310  df-ov 7357  df-oprab 7358  df-mpo 7359  df-1st 7918  df-2nd 7919  df-frecs 8209  df-wrecs 8240  df-recs 8314  df-1o 8409  df-2o 8410  df-nadd 8609  df-no 26987  df-slt 26988  df-bday 26989  df-sle 27089  df-sslt 27117  df-scut 27119  df-0s 27159  df-made 27173  df-old 27174  df-left 27176  df-right 27177  df-norec2 27257  df-adds 34298
This theorem is referenced by:  sleadd2  34325  addscan2  34328  sleadd1d  34330
  Copyright terms: Public domain W3C validator