MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sleadd1 Structured version   Visualization version   GIF version
Theorem sleadd1 28023
Description: Addition to both sides of surreal less-than or equal. Theorem 5 of [Conway] p. 18. (Contributed by Scott Fenton, 21-Jan-2025.)
Assertion
Ref Expression
sleadd1 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 ≤s 𝐵 ↔ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶)))
Proof of Theorem sleadd1
Dummy variables 𝑥 𝑦 𝑧 𝑎 𝑏 𝑐 𝑑 𝑝 𝑞 𝑥𝐿 𝑦𝐿 𝑧𝐿 𝑥𝑅 𝑦𝑅 𝑧𝑅 𝑥𝑂 𝑦𝑂 𝑧𝑂 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 7439 . . . . . . 7 (𝑥 = 𝑥𝑂 → (𝑥 +s 𝑧) = (𝑥𝑂 +s 𝑧))
21breq2d 5154 . . . . . 6 (𝑥 = 𝑥𝑂 → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧)))
3 breq2 5146 . . . . . 6 (𝑥 = 𝑥𝑂 → (𝑦 <s 𝑥 ↔ 𝑦 <s 𝑥𝑂))
42, 3imbi12d 344 . . . . 5 (𝑥 = 𝑥𝑂 → (((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦 <s 𝑥) ↔ ((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂)))
5 oveq1 7439 . . . . . . 7 (𝑦 = 𝑦𝑂 → (𝑦 +s 𝑧) = (𝑦𝑂 +s 𝑧))
65breq1d 5152 . . . . . 6 (𝑦 = 𝑦𝑂 → ((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) ↔ (𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧)))
7 breq1 5145 . . . . . 6 (𝑦 = 𝑦𝑂 → (𝑦 <s 𝑥𝑂 ↔ 𝑦𝑂 <s 𝑥𝑂))
86, 7imbi12d 344 . . . . 5 (𝑦 = 𝑦𝑂 → (((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ↔ ((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂)))
9 oveq2 7440 . . . . . . 7 (𝑧 = 𝑧𝑂 → (𝑦𝑂 +s 𝑧) = (𝑦𝑂 +s 𝑧𝑂))
10 oveq2 7440 . . . . . . 7 (𝑧 = 𝑧𝑂 → (𝑥𝑂 +s 𝑧) = (𝑥𝑂 +s 𝑧𝑂))
119, 10breq12d 5155 . . . . . 6 (𝑧 = 𝑧𝑂 → ((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) ↔ (𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂)))
1211imbi1d 341 . . . . 5 (𝑧 = 𝑧𝑂 → (((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ↔ ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂)))
13 oveq1 7439 . . . . . . 7 (𝑥 = 𝑥𝑂 → (𝑥 +s 𝑧𝑂) = (𝑥𝑂 +s 𝑧𝑂))
1413breq2d 5154 . . . . . 6 (𝑥 = 𝑥𝑂 → ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) ↔ (𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂)))
15 breq2 5146 . . . . . 6 (𝑥 = 𝑥𝑂 → (𝑦𝑂 <s 𝑥 ↔ 𝑦𝑂 <s 𝑥𝑂))
1614, 15imbi12d 344 . . . . 5 (𝑥 = 𝑥𝑂 → (((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ↔ ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂)))
17 oveq1 7439 . . . . . . 7 (𝑦 = 𝑦𝑂 → (𝑦 +s 𝑧𝑂) = (𝑦𝑂 +s 𝑧𝑂))
1817breq1d 5152 . . . . . 6 (𝑦 = 𝑦𝑂 → ((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) ↔ (𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂)))
19 breq1 5145 . . . . . 6 (𝑦 = 𝑦𝑂 → (𝑦 <s 𝑥 ↔ 𝑦𝑂 <s 𝑥))
2018, 19imbi12d 344 . . . . 5 (𝑦 = 𝑦𝑂 → (((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥) ↔ ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥)))
2117breq1d 5152 . . . . . 6 (𝑦 = 𝑦𝑂 → ((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) ↔ (𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂)))
2221, 7imbi12d 344 . . . . 5 (𝑦 = 𝑦𝑂 → (((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂) ↔ ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂)))
23 oveq2 7440 . . . . . . 7 (𝑧 = 𝑧𝑂 → (𝑥 +s 𝑧) = (𝑥 +s 𝑧𝑂))
249, 23breq12d 5155 . . . . . 6 (𝑧 = 𝑧𝑂 → ((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂)))
2524imbi1d 341 . . . . 5 (𝑧 = 𝑧𝑂 → (((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥) ↔ ((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥)))
26 oveq1 7439 . . . . . . 7 (𝑥 = 𝐴 → (𝑥 +s 𝑧) = (𝐴 +s 𝑧))
2726breq2d 5154 . . . . . 6 (𝑥 = 𝐴 → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (𝑦 +s 𝑧) <s (𝐴 +s 𝑧)))
28 breq2 5146 . . . . . 6 (𝑥 = 𝐴 → (𝑦 <s 𝑥 ↔ 𝑦 <s 𝐴))
2927, 28imbi12d 344 . . . . 5 (𝑥 = 𝐴 → (((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦 <s 𝑥) ↔ ((𝑦 +s 𝑧) <s (𝐴 +s 𝑧) → 𝑦 <s 𝐴)))
30 oveq1 7439 . . . . . . 7 (𝑦 = 𝐵 → (𝑦 +s 𝑧) = (𝐵 +s 𝑧))
3130breq1d 5152 . . . . . 6 (𝑦 = 𝐵 → ((𝑦 +s 𝑧) <s (𝐴 +s 𝑧) ↔ (𝐵 +s 𝑧) <s (𝐴 +s 𝑧)))
32 breq1 5145 . . . . . 6 (𝑦 = 𝐵 → (𝑦 <s 𝐴 ↔ 𝐵 <s 𝐴))
3331, 32imbi12d 344 . . . . 5 (𝑦 = 𝐵 → (((𝑦 +s 𝑧) <s (𝐴 +s 𝑧) → 𝑦 <s 𝐴) ↔ ((𝐵 +s 𝑧) <s (𝐴 +s 𝑧) → 𝐵 <s 𝐴)))
34 oveq2 7440 . . . . . . 7 (𝑧 = 𝐶 → (𝐵 +s 𝑧) = (𝐵 +s 𝐶))
35 oveq2 7440 . . . . . . 7 (𝑧 = 𝐶 → (𝐴 +s 𝑧) = (𝐴 +s 𝐶))
3634, 35breq12d 5155 . . . . . 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 28012 . . . . . . . . . . 11 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ((𝑦 +s 𝑧) ∈ No ∧ ({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) <<s {(𝑦 +s 𝑧)} ∧ {(𝑦 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})))
41 simp2 1137 . . . . . . . . . . 11 (((𝑦 +s 𝑧) ∈ No ∧ ({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) <<s {(𝑦 +s 𝑧)} ∧ {(𝑦 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})) → ({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) <<s {(𝑦 +s 𝑧)})
4240, 41syl 17 . . . . . . . . . 10 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) <<s {(𝑦 +s 𝑧)})
4340simp3d 1144 . . . . . . . . . 10 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → {(𝑦 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}))
44 ovex 7465 . . . . . . . . . . . 12 (𝑦 +s 𝑧) ∈ V
4544snnz 4775 . . . . . . . . . . 11 {(𝑦 +s 𝑧)} ≠ ∅
46 sslttr 27853 . . . . . . . . . . 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 1451 . . . . . . . . . 10 ((({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) <<s {(𝑦 +s 𝑧)} ∧ {(𝑦 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})) → ({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) <<s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}))
4842, 43, 47syl2anc 584 . . . . . . . . 9 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) <<s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}))
49 simp1 1136 . . . . . . . . . . . 12 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → 𝑥 ∈ No )
5049, 39addscut 28012 . . . . . . . . . . 11 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ((𝑥 +s 𝑧) ∈ No ∧ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) <<s {(𝑥 +s 𝑧)} ∧ {(𝑥 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)})))
51 simp2 1137 . . . . . . . . . . 11 (((𝑥 +s 𝑧) ∈ No ∧ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) <<s {(𝑥 +s 𝑧)} ∧ {(𝑥 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)})) → ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) <<s {(𝑥 +s 𝑧)})
5250, 51syl 17 . . . . . . . . . 10 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) <<s {(𝑥 +s 𝑧)})
5350simp3d 1144 . . . . . . . . . 10 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → {(𝑥 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)}))
54 ovex 7465 . . . . . . . . . . . 12 (𝑥 +s 𝑧) ∈ V
5554snnz 4775 . . . . . . . . . . 11 {(𝑥 +s 𝑧)} ≠ ∅
56 sslttr 27853 . . . . . . . . . . 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 1451 . . . . . . . . . 10 ((({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) <<s {(𝑥 +s 𝑧)} ∧ {(𝑥 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)})) → ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) <<s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)}))
5852, 53, 57syl2anc 584 . . . . . . . . 9 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) <<s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)}))
59 addsval2 27997 . . . . . . . . . 10 ((𝑦 ∈ No ∧ 𝑧 ∈ No ) → (𝑦 +s 𝑧) = (({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) |s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})))
60593adant1 1130 . . . . . . . . 9 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → (𝑦 +s 𝑧) = (({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) |s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})))
61 addsval2 27997 . . . . . . . . . 10 ((𝑥 ∈ No ∧ 𝑧 ∈ No ) → (𝑥 +s 𝑧) = (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) |s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)})))
62613adant2 1131 . . . . . . . . 9 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → (𝑥 +s 𝑧) = (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) |s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)})))
63 sltrec 27866 . . . . . . . . 9 (((({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) <<s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}) ∧ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) <<s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)})) ∧ ((𝑦 +s 𝑧) = (({𝑎 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑎 = (𝑦𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧𝐿)}) |s ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})) ∧ (𝑥 +s 𝑧) = (({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)}) |s ({𝑐 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑐 = (𝑥𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧𝑅)})))) → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (∃𝑝 ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)})(𝑦 +s 𝑧) ≤s 𝑝 ∨ ∃𝑞 ∈ ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})𝑞 ≤s (𝑥 +s 𝑧))))
6448, 58, 60, 62, 63syl22anc 838 . . . . . . . 8 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (∃𝑝 ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)})(𝑦 +s 𝑧) ≤s 𝑝 ∨ ∃𝑞 ∈ ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})𝑞 ≤s (𝑥 +s 𝑧))))
6564adantr 480 . . . . . . 7 (((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (∃𝑝 ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)})(𝑦 +s 𝑧) ≤s 𝑝 ∨ ∃𝑞 ∈ ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})𝑞 ≤s (𝑥 +s 𝑧))))
66 rexun 4195 . . . . . . . . . 10 (∃𝑝 ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)})(𝑦 +s 𝑧) ≤s 𝑝 ↔ (∃𝑝 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} (𝑦 +s 𝑧) ≤s 𝑝 ∨ ∃𝑝 ∈ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)} (𝑦 +s 𝑧) ≤s 𝑝))
67 eqeq1 2740 . . . . . . . . . . . . . 14 (𝑎 = 𝑝 → (𝑎 = (𝑥𝐿 +s 𝑧) ↔ 𝑝 = (𝑥𝐿 +s 𝑧)))
6867rexbidv 3178 . . . . . . . . . . . . 13 (𝑎 = 𝑝 → (∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧) ↔ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑝 = (𝑥𝐿 +s 𝑧)))
6968rexab 3699 . . . . . . . . . . . 12 (∃𝑝 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} (𝑦 +s 𝑧) ≤s 𝑝 ↔ ∃𝑝(∃𝑥𝐿 ∈ ( L ‘𝑥)𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
70 rexcom4 3287 . . . . . . . . . . . . . 14 (∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑝(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
71 r19.41v 3188 . . . . . . . . . . . . . . 15 (∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ (∃𝑥𝐿 ∈ ( L ‘𝑥)𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
7271exbii 1847 . . . . . . . . . . . . . 14 (∃𝑝∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝(∃𝑥𝐿 ∈ ( L ‘𝑥)𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
7370, 72bitri 275 . . . . . . . . . . . . 13 (∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑝(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝(∃𝑥𝐿 ∈ ( L ‘𝑥)𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
74 ovex 7465 . . . . . . . . . . . . . . 15 (𝑥𝐿 +s 𝑧) ∈ V
75 breq2 5146 . . . . . . . . . . . . . . 15 (𝑝 = (𝑥𝐿 +s 𝑧) → ((𝑦 +s 𝑧) ≤s 𝑝 ↔ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧)))
7674, 75ceqsexv 3531 . . . . . . . . . . . . . 14 (∃𝑝(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))
7776rexbii 3093 . . . . . . . . . . . . 13 (∃𝑥𝐿 ∈ ( L ‘𝑥)∃𝑝(𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))
7873, 77bitr3i 277 . . . . . . . . . . . 12 (∃𝑝(∃𝑥𝐿 ∈ ( L ‘𝑥)𝑝 = (𝑥𝐿 +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))
7969, 78bitri 275 . . . . . . . . . . 11 (∃𝑝 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} (𝑦 +s 𝑧) ≤s 𝑝 ↔ ∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))
80 eqeq1 2740 . . . . . . . . . . . . . 14 (𝑏 = 𝑝 → (𝑏 = (𝑥 +s 𝑧𝐿) ↔ 𝑝 = (𝑥 +s 𝑧𝐿)))
8180rexbidv 3178 . . . . . . . . . . . . 13 (𝑏 = 𝑝 → (∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿) ↔ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧𝐿)))
8281rexab 3699 . . . . . . . . . . . 12 (∃𝑝 ∈ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)} (𝑦 +s 𝑧) ≤s 𝑝 ↔ ∃𝑝(∃𝑧𝐿 ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
83 rexcom4 3287 . . . . . . . . . . . . . 14 (∃𝑧𝐿 ∈ ( L ‘𝑧)∃𝑝(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
84 r19.41v 3188 . . . . . . . . . . . . . . 15 (∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ (∃𝑧𝐿 ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
8584exbii 1847 . . . . . . . . . . . . . 14 (∃𝑝∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝(∃𝑧𝐿 ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
8683, 85bitri 275 . . . . . . . . . . . . 13 (∃𝑧𝐿 ∈ ( L ‘𝑧)∃𝑝(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝(∃𝑧𝐿 ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝))
87 ovex 7465 . . . . . . . . . . . . . . 15 (𝑥 +s 𝑧𝐿) ∈ V
88 breq2 5146 . . . . . . . . . . . . . . 15 (𝑝 = (𝑥 +s 𝑧𝐿) → ((𝑦 +s 𝑧) ≤s 𝑝 ↔ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿)))
8987, 88ceqsexv 3531 . . . . . . . . . . . . . 14 (∃𝑝(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))
9089rexbii 3093 . . . . . . . . . . . . 13 (∃𝑧𝐿 ∈ ( L ‘𝑧)∃𝑝(𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))
9186, 90bitr3i 277 . . . . . . . . . . . 12 (∃𝑝(∃𝑧𝐿 ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧𝐿) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))
9282, 91bitri 275 . . . . . . . . . . 11 (∃𝑝 ∈ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)} (𝑦 +s 𝑧) ≤s 𝑝 ↔ ∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))
9379, 92orbi12i 914 . . . . . . . . . 10 ((∃𝑝 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} (𝑦 +s 𝑧) ≤s 𝑝 ∨ ∃𝑝 ∈ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)} (𝑦 +s 𝑧) ≤s 𝑝) ↔ (∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧) ∨ ∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿)))
9466, 93bitri 275 . . . . . . . . 9 (∃𝑝 ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)})(𝑦 +s 𝑧) ≤s 𝑝 ↔ (∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧) ∨ ∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿)))
95 simpll2 1213 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))) → 𝑦 ∈ No )
96 leftssno 27920 . . . . . . . . . . . . . . 15 ( L ‘𝑥) ⊆ No
9796sseli 3978 . . . . . . . . . . . . . 14 (𝑥𝐿 ∈ ( L ‘𝑥) → 𝑥𝐿 ∈ No )
9897adantr 480 . . . . . . . . . . . . 13 ((𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧)) → 𝑥𝐿 ∈ No )
9998adantl 481 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))) → 𝑥𝐿 ∈ No )
100 simpll1 1212 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))) → 𝑥 ∈ No )
101 simprr 772 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))) → (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))
102 simpll3 1214 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))) → 𝑧 ∈ No )
103 sleadd1im 28021 . . . . . . . . . . . . . 14 ((𝑦 ∈ No ∧ 𝑥𝐿 ∈ No ∧ 𝑧 ∈ No ) → ((𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧) → 𝑦 ≤s 𝑥𝐿))
10495, 99, 102, 103syl3anc 1372 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))) → ((𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧) → 𝑦 ≤s 𝑥𝐿))
105101, 104mpd 15 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))) → 𝑦 ≤s 𝑥𝐿)
106 leftval 27903 . . . . . . . . . . . . . . . 16 ( L ‘𝑥) = {𝑥𝐿 ∈ ( O ‘( bday ‘𝑥)) ∣ 𝑥𝐿 <s 𝑥}
107106reqabi 3459 . . . . . . . . . . . . . . 15 (𝑥𝐿 ∈ ( L ‘𝑥) ↔ (𝑥𝐿 ∈ ( O ‘( bday ‘𝑥)) ∧ 𝑥𝐿 <s 𝑥))
108107simprbi 496 . . . . . . . . . . . . . 14 (𝑥𝐿 ∈ ( L ‘𝑥) → 𝑥𝐿 <s 𝑥)
109108adantr 480 . . . . . . . . . . . . 13 ((𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧)) → 𝑥𝐿 <s 𝑥)
110109adantl 481 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑥𝐿 ∈ ( L ‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧))) → 𝑥𝐿 <s 𝑥)
11195, 99, 100, 105, 110slelttrd 27807 . . . . . . . . . . 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 𝑥)
112111rexlimdvaa 3155 . . . . . . . . . 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 𝑥))
113 simpll2 1213 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → 𝑦 ∈ No )
114 leftssno 27920 . . . . . . . . . . . . . . . . 17 ( L ‘𝑧) ⊆ No
115114sseli 3978 . . . . . . . . . . . . . . . 16 (𝑧𝐿 ∈ ( L ‘𝑧) → 𝑧𝐿 ∈ No )
116115adantr 480 . . . . . . . . . . . . . . 15 ((𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿)) → 𝑧𝐿 ∈ No )
117116adantl 481 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → 𝑧𝐿 ∈ No )
118113, 117addscld 28014 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → (𝑦 +s 𝑧𝐿) ∈ No )
119 simpll3 1214 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → 𝑧 ∈ No )
120113, 119addscld 28014 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → (𝑦 +s 𝑧) ∈ No )
121 simpll1 1212 . . . . . . . . . . . . . 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 )
122121, 117addscld 28014 . . . . . . . . . . . . 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 )
123 leftval 27903 . . . . . . . . . . . . . . . . . 18 ( L ‘𝑧) = {𝑧𝐿 ∈ ( O ‘( bday ‘𝑧)) ∣ 𝑧𝐿 <s 𝑧}
124123reqabi 3459 . . . . . . . . . . . . . . . . 17 (𝑧𝐿 ∈ ( L ‘𝑧) ↔ (𝑧𝐿 ∈ ( O ‘( bday ‘𝑧)) ∧ 𝑧𝐿 <s 𝑧))
125124simprbi 496 . . . . . . . . . . . . . . . 16 (𝑧𝐿 ∈ ( L ‘𝑧) → 𝑧𝐿 <s 𝑧)
126125adantr 480 . . . . . . . . . . . . . . 15 ((𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿)) → 𝑧𝐿 <s 𝑧)
127126adantl 481 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → 𝑧𝐿 <s 𝑧)
128 sltadd2im 28020 . . . . . . . . . . . . . . 15 ((𝑧𝐿 ∈ No ∧ 𝑧 ∈ No ∧ 𝑦 ∈ No ) → (𝑧𝐿 <s 𝑧 → (𝑦 +s 𝑧𝐿) <s (𝑦 +s 𝑧)))
129117, 119, 113, 128syl3anc 1372 . . . . . . . . . . . . . 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 𝑧)))
130127, 129mpd 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 𝑧))
131 simprr 772 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))
132118, 120, 122, 130, 131sltletrd 27806 . . . . . . . . . . . 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 𝑧𝐿))
133 oveq2 7440 . . . . . . . . . . . . . . 15 (𝑧𝑂 = 𝑧𝐿 → (𝑦 +s 𝑧𝑂) = (𝑦 +s 𝑧𝐿))
134 oveq2 7440 . . . . . . . . . . . . . . 15 (𝑧𝑂 = 𝑧𝐿 → (𝑥 +s 𝑧𝑂) = (𝑥 +s 𝑧𝐿))
135133, 134breq12d 5155 . . . . . . . . . . . . . 14 (𝑧𝑂 = 𝑧𝐿 → ((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) ↔ (𝑦 +s 𝑧𝐿) <s (𝑥 +s 𝑧𝐿)))
136135imbi1d 341 . . . . . . . . . . . . 13 (𝑧𝑂 = 𝑧𝐿 → (((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥) ↔ ((𝑦 +s 𝑧𝐿) <s (𝑥 +s 𝑧𝐿) → 𝑦 <s 𝑥)))
137 simplr3 1217 . . . . . . . . . . . . 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 𝑥))
138 simprl 770 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝐿 ∈ ( L ‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿))) → 𝑧𝐿 ∈ ( L ‘𝑧))
139 elun1 4181 . . . . . . . . . . . . . 14 (𝑧𝐿 ∈ ( L ‘𝑧) → 𝑧𝐿 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧)))
140138, 139syl 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 ‘𝑧)))
141136, 137, 140rspcdva 3622 . . . . . . . . . . . 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 𝑥))
142132, 141mpd 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 𝑥)
143142rexlimdvaa 3155 . . . . . . . . . 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 𝑥))
144112, 143jaod 859 . . . . . . . . 9 (((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) → ((∃𝑥𝐿 ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥𝐿 +s 𝑧) ∨ ∃𝑧𝐿 ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧𝐿)) → 𝑦 <s 𝑥))
14594, 144biimtrid 242 . . . . . . . 8 (((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) → (∃𝑝 ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)})(𝑦 +s 𝑧) ≤s 𝑝 → 𝑦 <s 𝑥))
146 rexun 4195 . . . . . . . . . 10 (∃𝑞 ∈ ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})𝑞 ≤s (𝑥 +s 𝑧) ↔ (∃𝑞 ∈ {𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)}𝑞 ≤s (𝑥 +s 𝑧) ∨ ∃𝑞 ∈ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}𝑞 ≤s (𝑥 +s 𝑧)))
147 eqeq1 2740 . . . . . . . . . . . . . 14 (𝑐 = 𝑞 → (𝑐 = (𝑦𝑅 +s 𝑧) ↔ 𝑞 = (𝑦𝑅 +s 𝑧)))
148147rexbidv 3178 . . . . . . . . . . . . 13 (𝑐 = 𝑞 → (∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧) ↔ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧)))
149148rexab 3699 . . . . . . . . . . . 12 (∃𝑞 ∈ {𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)}𝑞 ≤s (𝑥 +s 𝑧) ↔ ∃𝑞(∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
150 rexcom4 3287 . . . . . . . . . . . . . 14 (∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑞(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
151 r19.41v 3188 . . . . . . . . . . . . . . 15 (∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ (∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
152151exbii 1847 . . . . . . . . . . . . . 14 (∃𝑞∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞(∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
153150, 152bitri 275 . . . . . . . . . . . . 13 (∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑞(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞(∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
154 ovex 7465 . . . . . . . . . . . . . . 15 (𝑦𝑅 +s 𝑧) ∈ V
155 breq1 5145 . . . . . . . . . . . . . . 15 (𝑞 = (𝑦𝑅 +s 𝑧) → (𝑞 ≤s (𝑥 +s 𝑧) ↔ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧)))
156154, 155ceqsexv 3531 . . . . . . . . . . . . . 14 (∃𝑞(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))
157156rexbii 3093 . . . . . . . . . . . . 13 (∃𝑦𝑅 ∈ ( R ‘𝑦)∃𝑞(𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))
158153, 157bitr3i 277 . . . . . . . . . . . 12 (∃𝑞(∃𝑦𝑅 ∈ ( R ‘𝑦)𝑞 = (𝑦𝑅 +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))
159149, 158bitri 275 . . . . . . . . . . 11 (∃𝑞 ∈ {𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)}𝑞 ≤s (𝑥 +s 𝑧) ↔ ∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))
160 eqeq1 2740 . . . . . . . . . . . . . 14 (𝑑 = 𝑞 → (𝑑 = (𝑦 +s 𝑧𝑅) ↔ 𝑞 = (𝑦 +s 𝑧𝑅)))
161160rexbidv 3178 . . . . . . . . . . . . 13 (𝑑 = 𝑞 → (∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅) ↔ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅)))
162161rexab 3699 . . . . . . . . . . . 12 (∃𝑞 ∈ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}𝑞 ≤s (𝑥 +s 𝑧) ↔ ∃𝑞(∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
163 rexcom4 3287 . . . . . . . . . . . . . 14 (∃𝑧𝑅 ∈ ( R ‘𝑧)∃𝑞(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
164 r19.41v 3188 . . . . . . . . . . . . . . 15 (∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ (∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
165164exbii 1847 . . . . . . . . . . . . . 14 (∃𝑞∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞(∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
166163, 165bitri 275 . . . . . . . . . . . . 13 (∃𝑧𝑅 ∈ ( R ‘𝑧)∃𝑞(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞(∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)))
167 ovex 7465 . . . . . . . . . . . . . . 15 (𝑦 +s 𝑧𝑅) ∈ V
168 breq1 5145 . . . . . . . . . . . . . . 15 (𝑞 = (𝑦 +s 𝑧𝑅) → (𝑞 ≤s (𝑥 +s 𝑧) ↔ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧)))
169167, 168ceqsexv 3531 . . . . . . . . . . . . . 14 (∃𝑞(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))
170169rexbii 3093 . . . . . . . . . . . . 13 (∃𝑧𝑅 ∈ ( R ‘𝑧)∃𝑞(𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))
171166, 170bitr3i 277 . . . . . . . . . . . 12 (∃𝑞(∃𝑧𝑅 ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧𝑅) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))
172162, 171bitri 275 . . . . . . . . . . 11 (∃𝑞 ∈ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}𝑞 ≤s (𝑥 +s 𝑧) ↔ ∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))
173159, 172orbi12i 914 . . . . . . . . . 10 ((∃𝑞 ∈ {𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)}𝑞 ≤s (𝑥 +s 𝑧) ∨ ∃𝑞 ∈ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)}𝑞 ≤s (𝑥 +s 𝑧)) ↔ (∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧) ∨ ∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧)))
174146, 173bitri 275 . . . . . . . . 9 (∃𝑞 ∈ ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})𝑞 ≤s (𝑥 +s 𝑧) ↔ (∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧) ∨ ∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧)))
175 simpll2 1213 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))) → 𝑦 ∈ No )
176 rightssno 27921 . . . . . . . . . . . . . . 15 ( R ‘𝑦) ⊆ No
177176sseli 3978 . . . . . . . . . . . . . 14 (𝑦𝑅 ∈ ( R ‘𝑦) → 𝑦𝑅 ∈ No )
178177adantr 480 . . . . . . . . . . . . 13 ((𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧)) → 𝑦𝑅 ∈ No )
179178adantl 481 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))) → 𝑦𝑅 ∈ No )
180 simpll1 1212 . . . . . . . . . . . 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 )
181 rightval 27904 . . . . . . . . . . . . . . . 16 ( R ‘𝑦) = {𝑦𝑅 ∈ ( O ‘( bday ‘𝑦)) ∣ 𝑦 <s 𝑦𝑅}
182181reqabi 3459 . . . . . . . . . . . . . . 15 (𝑦𝑅 ∈ ( R ‘𝑦) ↔ (𝑦𝑅 ∈ ( O ‘( bday ‘𝑦)) ∧ 𝑦 <s 𝑦𝑅))
183182simprbi 496 . . . . . . . . . . . . . 14 (𝑦𝑅 ∈ ( R ‘𝑦) → 𝑦 <s 𝑦𝑅)
184183adantr 480 . . . . . . . . . . . . 13 ((𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧)) → 𝑦 <s 𝑦𝑅)
185184adantl 481 . . . . . . . . . . . 12 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))) → 𝑦 <s 𝑦𝑅)
186 simprr 772 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))) → (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))
187 simpll3 1214 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑦𝑅 ∈ ( R ‘𝑦) ∧ (𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧))) → 𝑧 ∈ No )
188 sleadd1im 28021 . . . . . . . . . . . . . 14 ((𝑦𝑅 ∈ No ∧ 𝑥 ∈ No ∧ 𝑧 ∈ No ) → ((𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧) → 𝑦𝑅 ≤s 𝑥))
189179, 180, 187, 188syl3anc 1372 . . . . . . . . . . . . 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 𝑥))
190186, 189mpd 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 𝑥)
191175, 179, 180, 185, 190sltletrd 27806 . . . . . . . . . . 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 𝑥)
192191rexlimdvaa 3155 . . . . . . . . . 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 𝑥))
193 simpll2 1213 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → 𝑦 ∈ No )
194 rightssno 27921 . . . . . . . . . . . . . . . . 17 ( R ‘𝑧) ⊆ No
195194sseli 3978 . . . . . . . . . . . . . . . 16 (𝑧𝑅 ∈ ( R ‘𝑧) → 𝑧𝑅 ∈ No )
196195adantr 480 . . . . . . . . . . . . . . 15 ((𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧)) → 𝑧𝑅 ∈ No )
197196adantl 481 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → 𝑧𝑅 ∈ No )
198193, 197addscld 28014 . . . . . . . . . . . . 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 )
199 simpll1 1212 . . . . . . . . . . . . . 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 )
200 simpll3 1214 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → 𝑧 ∈ No )
201199, 200addscld 28014 . . . . . . . . . . . . 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 )
202199, 197addscld 28014 . . . . . . . . . . . . 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 )
203 simprr 772 . . . . . . . . . . . . 13 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))
204200, 197, 1993jca 1128 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → (𝑧 ∈ No ∧ 𝑧𝑅 ∈ No ∧ 𝑥 ∈ No ))
205 rightval 27904 . . . . . . . . . . . . . . . . . 18 ( R ‘𝑧) = {𝑧𝑅 ∈ ( O ‘( bday ‘𝑧)) ∣ 𝑧 <s 𝑧𝑅}
206205reqabi 3459 . . . . . . . . . . . . . . . . 17 (𝑧𝑅 ∈ ( R ‘𝑧) ↔ (𝑧𝑅 ∈ ( O ‘( bday ‘𝑧)) ∧ 𝑧 <s 𝑧𝑅))
207206simprbi 496 . . . . . . . . . . . . . . . 16 (𝑧𝑅 ∈ ( R ‘𝑧) → 𝑧 <s 𝑧𝑅)
208207adantr 480 . . . . . . . . . . . . . . 15 ((𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧)) → 𝑧 <s 𝑧𝑅)
209208adantl 481 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → 𝑧 <s 𝑧𝑅)
210 sltadd2im 28020 . . . . . . . . . . . . . 14 ((𝑧 ∈ No ∧ 𝑧𝑅 ∈ No ∧ 𝑥 ∈ No ) → (𝑧 <s 𝑧𝑅 → (𝑥 +s 𝑧) <s (𝑥 +s 𝑧𝑅)))
211204, 209, 210sylc 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 𝑧𝑅))
212198, 201, 202, 203, 211slelttrd 27807 . . . . . . . . . . . 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 𝑧𝑅))
213 oveq2 7440 . . . . . . . . . . . . . . 15 (𝑧𝑂 = 𝑧𝑅 → (𝑦 +s 𝑧𝑂) = (𝑦 +s 𝑧𝑅))
214 oveq2 7440 . . . . . . . . . . . . . . 15 (𝑧𝑂 = 𝑧𝑅 → (𝑥 +s 𝑧𝑂) = (𝑥 +s 𝑧𝑅))
215213, 214breq12d 5155 . . . . . . . . . . . . . 14 (𝑧𝑂 = 𝑧𝑅 → ((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) ↔ (𝑦 +s 𝑧𝑅) <s (𝑥 +s 𝑧𝑅)))
216215imbi1d 341 . . . . . . . . . . . . 13 (𝑧𝑂 = 𝑧𝑅 → (((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥) ↔ ((𝑦 +s 𝑧𝑅) <s (𝑥 +s 𝑧𝑅) → 𝑦 <s 𝑥)))
217 simplr3 1217 . . . . . . . . . . . . 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 𝑥))
218 simprl 770 . . . . . . . . . . . . . 14 ((((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) ∧ (𝑧𝑅 ∈ ( R ‘𝑧) ∧ (𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧))) → 𝑧𝑅 ∈ ( R ‘𝑧))
219 elun2 4182 . . . . . . . . . . . . . 14 (𝑧𝑅 ∈ ( R ‘𝑧) → 𝑧𝑅 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧)))
220218, 219syl 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 ‘𝑧)))
221216, 217, 220rspcdva 3622 . . . . . . . . . . . 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 𝑥))
222212, 221mpd 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 𝑥)
223222rexlimdvaa 3155 . . . . . . . . . 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 𝑥))
224192, 223jaod 859 . . . . . . . . 9 (((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) → ((∃𝑦𝑅 ∈ ( R ‘𝑦)(𝑦𝑅 +s 𝑧) ≤s (𝑥 +s 𝑧) ∨ ∃𝑧𝑅 ∈ ( R ‘𝑧)(𝑦 +s 𝑧𝑅) ≤s (𝑥 +s 𝑧)) → 𝑦 <s 𝑥))
225174, 224biimtrid 242 . . . . . . . 8 (((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) → (∃𝑞 ∈ ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})𝑞 ≤s (𝑥 +s 𝑧) → 𝑦 <s 𝑥))
226145, 225jaod 859 . . . . . . 7 (((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) → ((∃𝑝 ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑎 = (𝑥𝐿 +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧𝐿)})(𝑦 +s 𝑧) ≤s 𝑝 ∨ ∃𝑞 ∈ ({𝑐 ∣ ∃𝑦𝑅 ∈ ( R ‘𝑦)𝑐 = (𝑦𝑅 +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧𝑅 ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧𝑅)})𝑞 ≤s (𝑥 +s 𝑧)) → 𝑦 <s 𝑥))
22765, 226sylbid 240 . . . . . 6 (((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥))) → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦 <s 𝑥))
228227ex 412 . . . . 5 ((𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → (((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦𝑂 <s 𝑥𝑂) ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥𝑂 +s 𝑧𝑂) → 𝑦 <s 𝑥𝑂)) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))((𝑦 +s 𝑧) <s (𝑥𝑂 +s 𝑧) → 𝑦 <s 𝑥𝑂) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦𝑂 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦𝑂 <s 𝑥) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))((𝑦𝑂 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦𝑂 <s 𝑥)) ∧ ∀𝑧𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))((𝑦 +s 𝑧𝑂) <s (𝑥 +s 𝑧𝑂) → 𝑦 <s 𝑥)) → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦 <s 𝑥)))
2294, 8, 12, 16, 20, 22, 25, 29, 33, 37, 228no3inds 27992 . . . 4 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐵 +s 𝐶) <s (𝐴 +s 𝐶) → 𝐵 <s 𝐴))
230 addscl 28015 . . . . . 6 ((𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐵 +s 𝐶) ∈ No )
2312303adant1 1130 . . . . 5 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐵 +s 𝐶) ∈ No )
232 addscl 28015 . . . . . 6 ((𝐴 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 +s 𝐶) ∈ No )
2332323adant2 1131 . . . . 5 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 +s 𝐶) ∈ No )
234 sltnle 27799 . . . . 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 27799 . . . . . 6 ((𝐵 ∈ No ∧ 𝐴 ∈ No ) → (𝐵 <s 𝐴 ↔ ¬ 𝐴 ≤s 𝐵))
237236ancoms 458 . . . . 5 ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐵 <s 𝐴 ↔ ¬ 𝐴 ≤s 𝐵))
2382373adant3 1132 . . . 4 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐵 <s 𝐴 ↔ ¬ 𝐴 ≤s 𝐵))
239229, 235, 2383imtr3d 293 . . 3 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (¬ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶) → ¬ 𝐴 ≤s 𝐵))
240239con4d 115 . 2 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 ≤s 𝐵 → (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶)))
241 sleadd1im 28021 . 2 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶) → 𝐴 ≤s 𝐵))
242240, 241impbid 212 1 ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 ≤s 𝐵 ↔ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1539  ∃wex 1778   ∈ wcel 2107  {cab 2713   ≠ wne 2939  ∀wral 3060  ∃wrex 3069   ∪ cun 3948  ∅c0 4332  {csn 4625   class class class wbr 5142  ‘cfv 6560  (class class class)co 7432   No csur 27685   <s cslt 27686   bday cbday 27687   ≤s csle 27790   <<s csslt 27826   |s cscut 27828   O cold 27883   L cleft 27885   R cright 27886   +s cadds 27993
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-tp 4630  df-op 4632  df-ot 4634  df-uni 4907  df-int 4946  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-se 5637  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-1st 8015  df-2nd 8016  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-1o 8507  df-2o 8508  df-nadd 8705  df-no 27688  df-slt 27689  df-bday 27690  df-sle 27791  df-sslt 27827  df-scut 27829  df-0s 27870  df-made 27887  df-old 27888  df-left 27890  df-right 27891  df-norec2 27983  df-adds 27994
This theorem is referenced by:  sleadd2  28024  addscan2  28027  sleadd1d  28029  nnsge1  28347
  Copyright terms: Public domain W3C validator