Step | Hyp | Ref
| Expression |
1 | | oveq1 7361 |
. . . . . . 7
⊢ (𝑥 = 𝑥O → (𝑥 +s 𝑧) = (𝑥O +s 𝑧)) |
2 | 1 | breq2d 5116 |
. . . . . 6
⊢ (𝑥 = 𝑥O → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (𝑦 +s 𝑧) <s (𝑥O +s 𝑧))) |
3 | | breq2 5108 |
. . . . . 6
⊢ (𝑥 = 𝑥O → (𝑦 <s 𝑥 ↔ 𝑦 <s 𝑥O)) |
4 | 2, 3 | imbi12d 344 |
. . . . 5
⊢ (𝑥 = 𝑥O → (((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦 <s 𝑥) ↔ ((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) → 𝑦 <s 𝑥O))) |
5 | | oveq1 7361 |
. . . . . . 7
⊢ (𝑦 = 𝑦O → (𝑦 +s 𝑧) = (𝑦O +s 𝑧)) |
6 | 5 | breq1d 5114 |
. . . . . 6
⊢ (𝑦 = 𝑦O → ((𝑦 +s 𝑧) <s (𝑥O +s 𝑧) ↔ (𝑦O +s 𝑧) <s (𝑥O +s 𝑧))) |
7 | | breq1 5107 |
. . . . . 6
⊢ (𝑦 = 𝑦O → (𝑦 <s 𝑥O ↔ 𝑦O <s 𝑥O)) |
8 | 6, 7 | imbi12d 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)) |
11 | 9, 10 | breq12d 5117 |
. . . . . 6
⊢ (𝑧 = 𝑧O → ((𝑦O +s 𝑧) <s (𝑥O +s 𝑧) ↔ (𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O))) |
12 | 11 | imbi1d 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)) |
14 | 13 | breq2d 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)) |
16 | 14, 15 | imbi12d 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)) |
18 | 17 | breq1d 5114 |
. . . . . 6
⊢ (𝑦 = 𝑦O → ((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) ↔ (𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O))) |
19 | | breq1 5107 |
. . . . . 6
⊢ (𝑦 = 𝑦O → (𝑦 <s 𝑥 ↔ 𝑦O <s 𝑥)) |
20 | 18, 19 | imbi12d 344 |
. . . . 5
⊢ (𝑦 = 𝑦O → (((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦 <s 𝑥) ↔ ((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥))) |
21 | 17 | breq1d 5114 |
. . . . . 6
⊢ (𝑦 = 𝑦O → ((𝑦 +s 𝑧O) <s (𝑥O +s 𝑧O) ↔ (𝑦O +s 𝑧O) <s (𝑥O +s 𝑧O))) |
22 | 21, 7 | imbi12d 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)) |
24 | 9, 23 | breq12d 5117 |
. . . . . 6
⊢ (𝑧 = 𝑧O → ((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) ↔ (𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O))) |
25 | 24 | imbi1d 341 |
. . . . 5
⊢ (𝑧 = 𝑧O → (((𝑦O +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦O <s 𝑥) ↔ ((𝑦O +s 𝑧O) <s (𝑥 +s 𝑧O) → 𝑦O <s 𝑥))) |
26 | | oveq1 7361 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑥 +s 𝑧) = (𝐴 +s 𝑧)) |
27 | 26 | breq2d 5116 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) ↔ (𝑦 +s 𝑧) <s (𝐴 +s 𝑧))) |
28 | | breq2 5108 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝑦 <s 𝑥 ↔ 𝑦 <s 𝐴)) |
29 | 27, 28 | imbi12d 344 |
. . . . 5
⊢ (𝑥 = 𝐴 → (((𝑦 +s 𝑧) <s (𝑥 +s 𝑧) → 𝑦 <s 𝑥) ↔ ((𝑦 +s 𝑧) <s (𝐴 +s 𝑧) → 𝑦 <s 𝐴))) |
30 | | oveq1 7361 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (𝑦 +s 𝑧) = (𝐵 +s 𝑧)) |
31 | 30 | breq1d 5114 |
. . . . . 6
⊢ (𝑦 = 𝐵 → ((𝑦 +s 𝑧) <s (𝐴 +s 𝑧) ↔ (𝐵 +s 𝑧) <s (𝐴 +s 𝑧))) |
32 | | breq1 5107 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (𝑦 <s 𝐴 ↔ 𝐵 <s 𝐴)) |
33 | 31, 32 | imbi12d 344 |
. . . . 5
⊢ (𝑦 = 𝐵 → (((𝑦 +s 𝑧) <s (𝐴 +s 𝑧) → 𝑦 <s 𝐴) ↔ ((𝐵 +s 𝑧) <s (𝐴 +s 𝑧) → 𝐵 <s 𝐴))) |
34 | | oveq2 7362 |
. . . . . . 7
⊢ (𝑧 = 𝐶 → (𝐵 +s 𝑧) = (𝐵 +s 𝐶)) |
35 | | oveq2 7362 |
. . . . . . 7
⊢ (𝑧 = 𝐶 → (𝐴 +s 𝑧) = (𝐴 +s 𝐶)) |
36 | 34, 35 | breq12d 5117 |
. . . . . 6
⊢ (𝑧 = 𝐶 → ((𝐵 +s 𝑧) <s (𝐴 +s 𝑧) ↔ (𝐵 +s 𝐶) <s (𝐴 +s 𝐶))) |
37 | 36 | imbi1d 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 ) |
40 | 38, 39 | addscut 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 𝑧)}) |
42 | 40, 41 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
→ ({𝑎 ∣
∃𝑦L ∈
( L ‘𝑦)𝑎 = (𝑦L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑦 +s 𝑧L)}) <<s {(𝑦 +s 𝑧)}) |
43 | 40 | simp3d 1144 |
. . . . . . . . . 10
⊢ ((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
→ {(𝑦 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑦R ∈ ( R
‘𝑦)𝑐 = (𝑦R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧R)})) |
44 | | ovex 7387 |
. . . . . . . . . . . 12
⊢ (𝑦 +s 𝑧) ∈ V |
45 | 44 | snnz 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)})) |
47 | 45, 46 | mp3an3 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)})) |
48 | 42, 43, 47 | syl2anc 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 ) |
50 | 49, 39 | addscut 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 𝑧)}) |
52 | 50, 51 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
→ ({𝑎 ∣
∃𝑥L ∈
( L ‘𝑥)𝑎 = (𝑥L +s 𝑧)} ∪ {𝑏 ∣ ∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧L)}) <<s {(𝑥 +s 𝑧)}) |
53 | 50 | simp3d 1144 |
. . . . . . . . . 10
⊢ ((𝑥 ∈
No ∧ 𝑦 ∈
No ∧ 𝑧 ∈ No )
→ {(𝑥 +s 𝑧)} <<s ({𝑐 ∣ ∃𝑥R ∈ ( R
‘𝑥)𝑐 = (𝑥R +s 𝑧)} ∪ {𝑑 ∣ ∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑥 +s 𝑧R)})) |
54 | | ovex 7387 |
. . . . . . . . . . . 12
⊢ (𝑥 +s 𝑧) ∈ V |
55 | 54 | snnz 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)})) |
57 | 55, 56 | mp3an3 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)})) |
58 | 52, 53, 57 | syl2anc 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)}))) |
60 | 59 | 3adant1 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)}))) |
62 | 61 | 3adant2 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 𝑧)))) |
64 | 48, 58, 60, 62, 63 | syl22anc 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 𝑧)))) |
65 | 64 | adantr 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 𝑧))) |
68 | 67 | rexbidv 3174 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑝 → (∃𝑥L ∈ ( L ‘𝑥)𝑎 = (𝑥L +s 𝑧) ↔ ∃𝑥L ∈ ( L ‘𝑥)𝑝 = (𝑥L +s 𝑧))) |
69 | 68 | rexab 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 𝑝)) |
72 | 71 | exbii 1850 |
. . . . . . . . . . . . . 14
⊢
(∃𝑝∃𝑥L ∈ ( L ‘𝑥)(𝑝 = (𝑥L +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝(∃𝑥L ∈ ( L ‘𝑥)𝑝 = (𝑥L +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝)) |
73 | 70, 72 | bitri 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 𝑧))) |
76 | 74, 75 | ceqsexv 3493 |
. . . . . . . . . . . . . 14
⊢
(∃𝑝(𝑝 = (𝑥L +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ (𝑦 +s 𝑧) ≤s (𝑥L +s 𝑧)) |
77 | 76 | rexbii 3096 |
. . . . . . . . . . . . 13
⊢
(∃𝑥L ∈ ( L ‘𝑥)∃𝑝(𝑝 = (𝑥L +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑥L ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥L +s 𝑧)) |
78 | 73, 77 | bitr3i 276 |
. . . . . . . . . . . 12
⊢
(∃𝑝(∃𝑥L ∈ ( L ‘𝑥)𝑝 = (𝑥L +s 𝑧) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑥L ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥L +s 𝑧)) |
79 | 69, 78 | bitri 274 |
. . . . . . . . . . 11
⊢
(∃𝑝 ∈
{𝑎 ∣ ∃𝑥L ∈ ( L
‘𝑥)𝑎 = (𝑥L +s 𝑧)} (𝑦 +s 𝑧) ≤s 𝑝 ↔ ∃𝑥L ∈ ( L ‘𝑥)(𝑦 +s 𝑧) ≤s (𝑥L +s 𝑧)) |
80 | | eqeq1 2740 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑝 → (𝑏 = (𝑥 +s 𝑧L) ↔ 𝑝 = (𝑥 +s 𝑧L))) |
81 | 80 | rexbidv 3174 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑝 → (∃𝑧L ∈ ( L ‘𝑧)𝑏 = (𝑥 +s 𝑧L) ↔ ∃𝑧L ∈ ( L
‘𝑧)𝑝 = (𝑥 +s 𝑧L))) |
82 | 81 | rexab 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 𝑝)) |
85 | 84 | exbii 1850 |
. . . . . . . . . . . . . 14
⊢
(∃𝑝∃𝑧L ∈ ( L ‘𝑧)(𝑝 = (𝑥 +s 𝑧L) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑝(∃𝑧L ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧L) ∧ (𝑦 +s 𝑧) ≤s 𝑝)) |
86 | 83, 85 | bitri 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))) |
89 | 87, 88 | ceqsexv 3493 |
. . . . . . . . . . . . . 14
⊢
(∃𝑝(𝑝 = (𝑥 +s 𝑧L) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L)) |
90 | 89 | rexbii 3096 |
. . . . . . . . . . . . 13
⊢
(∃𝑧L ∈ ( L ‘𝑧)∃𝑝(𝑝 = (𝑥 +s 𝑧L) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑧L ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L)) |
91 | 86, 90 | bitr3i 276 |
. . . . . . . . . . . 12
⊢
(∃𝑝(∃𝑧L ∈ ( L ‘𝑧)𝑝 = (𝑥 +s 𝑧L) ∧ (𝑦 +s 𝑧) ≤s 𝑝) ↔ ∃𝑧L ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L)) |
92 | 82, 91 | bitri 274 |
. . . . . . . . . . 11
⊢
(∃𝑝 ∈
{𝑏 ∣ ∃𝑧L ∈ ( L
‘𝑧)𝑏 = (𝑥 +s 𝑧L)} (𝑦 +s 𝑧) ≤s 𝑝 ↔ ∃𝑧L ∈ ( L ‘𝑧)(𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L)) |
93 | 79, 92 | orbi12i 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))) |
94 | 66, 93 | bitri 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 |
97 | 96 | sseli 3939 |
. . . . . . . . . . . . . 14
⊢ (𝑥L ∈ ( L
‘𝑥) → 𝑥L ∈ No ) |
98 | 97 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑥L ∈ ( L
‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥L +s 𝑧)) → 𝑥L ∈ No
) |
99 | 98 | adantl 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)) |
104 | 95, 99, 102, 103 | syl3anc 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)) |
105 | 101, 104 | mpd 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 𝑥} |
107 | 106 | rabeq2i 3428 |
. . . . . . . . . . . . . . 15
⊢ (𝑥L ∈ ( L
‘𝑥) ↔ (𝑥L ∈ ( O
‘( bday ‘𝑥)) ∧ 𝑥L <s 𝑥)) |
108 | 107 | simprbi 497 |
. . . . . . . . . . . . . 14
⊢ (𝑥L ∈ ( L
‘𝑥) → 𝑥L <s 𝑥) |
109 | 108 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑥L ∈ ( L
‘𝑥) ∧ (𝑦 +s 𝑧) ≤s (𝑥L +s 𝑧)) → 𝑥L <s 𝑥) |
110 | 109 | adantl 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 𝑥) |
111 | 95, 99, 100, 105, 110 | slelttrd 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 𝑥) |
112 | 111 | rexlimdvaa 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 |
115 | 114 | sseli 3939 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧L ∈ ( L
‘𝑧) → 𝑧L ∈ No ) |
116 | 115 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧L ∈ ( L
‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L)) → 𝑧L ∈ No
) |
117 | 116 | adantl 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
) |
118 | 113, 117 | addscld 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
) |
120 | 113, 119 | addscld 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
) |
122 | 121, 117 | addscld 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 𝑧} |
124 | 123 | rabeq2i 3428 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧L ∈ ( L
‘𝑧) ↔ (𝑧L ∈ ( O
‘( bday ‘𝑧)) ∧ 𝑧L <s 𝑧)) |
125 | 124 | simprbi 497 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧L ∈ ( L
‘𝑧) → 𝑧L <s 𝑧) |
126 | 125 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧L ∈ ( L
‘𝑧) ∧ (𝑦 +s 𝑧) ≤s (𝑥 +s 𝑧L)) → 𝑧L <s 𝑧) |
127 | 126 | adantl 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 𝑧))) |
129 | 117, 119,
113, 128 | syl3anc 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 𝑧))) |
130 | 127, 129 | mpd 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)) |
132 | 118, 120,
122, 130, 131 | sltletrd 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)) |
135 | 133, 134 | breq12d 5117 |
. . . . . . . . . . . . . 14
⊢ (𝑧O = 𝑧L → ((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) ↔ (𝑦 +s 𝑧L) <s (𝑥 +s 𝑧L))) |
136 | 135 | imbi1d 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
‘𝑧))) |
140 | 138, 139 | syl 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 ‘𝑧))) |
141 | 136, 137,
140 | rspcdva 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 𝑥)) |
142 | 132, 141 | mpd 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 𝑥) |
143 | 142 | rexlimdvaa 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 𝑥)) |
144 | 112, 143 | jaod 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 𝑥)) |
145 | 94, 144 | biimtrid 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 𝑧))) |
148 | 147 | rexbidv 3174 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 𝑞 → (∃𝑦R ∈ ( R ‘𝑦)𝑐 = (𝑦R +s 𝑧) ↔ ∃𝑦R ∈ ( R ‘𝑦)𝑞 = (𝑦R +s 𝑧))) |
149 | 148 | rexab 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 𝑧))) |
152 | 151 | exbii 1850 |
. . . . . . . . . . . . . 14
⊢
(∃𝑞∃𝑦R ∈ ( R ‘𝑦)(𝑞 = (𝑦R +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞(∃𝑦R ∈ ( R ‘𝑦)𝑞 = (𝑦R +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧))) |
153 | 150, 152 | bitri 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 𝑧))) |
156 | 154, 155 | ceqsexv 3493 |
. . . . . . . . . . . . . 14
⊢
(∃𝑞(𝑞 = (𝑦R +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ (𝑦R +s 𝑧) ≤s (𝑥 +s 𝑧)) |
157 | 156 | rexbii 3096 |
. . . . . . . . . . . . 13
⊢
(∃𝑦R ∈ ( R ‘𝑦)∃𝑞(𝑞 = (𝑦R +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑦R ∈ ( R ‘𝑦)(𝑦R +s 𝑧) ≤s (𝑥 +s 𝑧)) |
158 | 153, 157 | bitr3i 276 |
. . . . . . . . . . . 12
⊢
(∃𝑞(∃𝑦R ∈ ( R ‘𝑦)𝑞 = (𝑦R +s 𝑧) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑦R ∈ ( R ‘𝑦)(𝑦R +s 𝑧) ≤s (𝑥 +s 𝑧)) |
159 | 149, 158 | bitri 274 |
. . . . . . . . . . 11
⊢
(∃𝑞 ∈
{𝑐 ∣ ∃𝑦R ∈ ( R
‘𝑦)𝑐 = (𝑦R +s 𝑧)}𝑞 ≤s (𝑥 +s 𝑧) ↔ ∃𝑦R ∈ ( R ‘𝑦)(𝑦R +s 𝑧) ≤s (𝑥 +s 𝑧)) |
160 | | eqeq1 2740 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = 𝑞 → (𝑑 = (𝑦 +s 𝑧R) ↔ 𝑞 = (𝑦 +s 𝑧R))) |
161 | 160 | rexbidv 3174 |
. . . . . . . . . . . . 13
⊢ (𝑑 = 𝑞 → (∃𝑧R ∈ ( R ‘𝑧)𝑑 = (𝑦 +s 𝑧R) ↔ ∃𝑧R ∈ ( R
‘𝑧)𝑞 = (𝑦 +s 𝑧R))) |
162 | 161 | rexab 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 𝑧))) |
165 | 164 | exbii 1850 |
. . . . . . . . . . . . . 14
⊢
(∃𝑞∃𝑧R ∈ ( R ‘𝑧)(𝑞 = (𝑦 +s 𝑧R) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑞(∃𝑧R ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧R) ∧ 𝑞 ≤s (𝑥 +s 𝑧))) |
166 | 163, 165 | bitri 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 𝑧))) |
169 | 167, 168 | ceqsexv 3493 |
. . . . . . . . . . . . . 14
⊢
(∃𝑞(𝑞 = (𝑦 +s 𝑧R) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ (𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧)) |
170 | 169 | rexbii 3096 |
. . . . . . . . . . . . 13
⊢
(∃𝑧R ∈ ( R ‘𝑧)∃𝑞(𝑞 = (𝑦 +s 𝑧R) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑧R ∈ ( R ‘𝑧)(𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧)) |
171 | 166, 170 | bitr3i 276 |
. . . . . . . . . . . 12
⊢
(∃𝑞(∃𝑧R ∈ ( R ‘𝑧)𝑞 = (𝑦 +s 𝑧R) ∧ 𝑞 ≤s (𝑥 +s 𝑧)) ↔ ∃𝑧R ∈ ( R ‘𝑧)(𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧)) |
172 | 162, 171 | bitri 274 |
. . . . . . . . . . 11
⊢
(∃𝑞 ∈
{𝑑 ∣ ∃𝑧R ∈ ( R
‘𝑧)𝑑 = (𝑦 +s 𝑧R)}𝑞 ≤s (𝑥 +s 𝑧) ↔ ∃𝑧R ∈ ( R ‘𝑧)(𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧)) |
173 | 159, 172 | orbi12i 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 𝑧))) |
174 | 146, 173 | bitri 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 |
177 | 176 | sseli 3939 |
. . . . . . . . . . . . . 14
⊢ (𝑦R ∈ ( R
‘𝑦) → 𝑦R ∈ No ) |
178 | 177 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑦R ∈ ( R
‘𝑦) ∧ (𝑦R +s 𝑧) ≤s (𝑥 +s 𝑧)) → 𝑦R ∈ No
) |
179 | 178 | adantl 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} |
182 | 181 | rabeq2i 3428 |
. . . . . . . . . . . . . . 15
⊢ (𝑦R ∈ ( R
‘𝑦) ↔ (𝑦R ∈ ( O
‘( bday ‘𝑦)) ∧ 𝑦 <s 𝑦R)) |
183 | 182 | simprbi 497 |
. . . . . . . . . . . . . 14
⊢ (𝑦R ∈ ( R
‘𝑦) → 𝑦 <s 𝑦R) |
184 | 183 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑦R ∈ ( R
‘𝑦) ∧ (𝑦R +s 𝑧) ≤s (𝑥 +s 𝑧)) → 𝑦 <s 𝑦R) |
185 | 184 | adantl 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 𝑥)) |
189 | 179, 180,
187, 188 | syl3anc 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 𝑥)) |
190 | 186, 189 | mpd 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 𝑥) |
191 | 175, 179,
180, 185, 190 | sltletrd 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 𝑥) |
192 | 191 | rexlimdvaa 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 |
195 | 194 | sseli 3939 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧R ∈ ( R
‘𝑧) → 𝑧R ∈ No ) |
196 | 195 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧R ∈ ( R
‘𝑧) ∧ (𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧)) → 𝑧R ∈ No
) |
197 | 196 | adantl 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
) |
198 | 193, 197 | addscld 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
) |
201 | 199, 200 | addscld 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
) |
202 | 199, 197 | addscld 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 𝑧)) |
204 | 200, 197,
199 | 3jca 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} |
206 | 205 | rabeq2i 3428 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧R ∈ ( R
‘𝑧) ↔ (𝑧R ∈ ( O
‘( bday ‘𝑧)) ∧ 𝑧 <s 𝑧R)) |
207 | 206 | simprbi 497 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧R ∈ ( R
‘𝑧) → 𝑧 <s 𝑧R) |
208 | 207 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧R ∈ ( R
‘𝑧) ∧ (𝑦 +s 𝑧R) ≤s (𝑥 +s 𝑧)) → 𝑧 <s 𝑧R) |
209 | 208 | adantl 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))) |
211 | 204, 209,
210 | sylc 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)) |
212 | 198, 201,
202, 203, 211 | slelttrd 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)) |
215 | 213, 214 | breq12d 5117 |
. . . . . . . . . . . . . 14
⊢ (𝑧O = 𝑧R → ((𝑦 +s 𝑧O) <s (𝑥 +s 𝑧O) ↔ (𝑦 +s 𝑧R) <s (𝑥 +s 𝑧R))) |
216 | 215 | imbi1d 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
‘𝑧))) |
220 | 218, 219 | syl 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 ‘𝑧))) |
221 | 216, 217,
220 | rspcdva 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 𝑥)) |
222 | 212, 221 | mpd 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 𝑥) |
223 | 222 | rexlimdvaa 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 𝑥)) |
224 | 192, 223 | jaod 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 𝑥)) |
225 | 174, 224 | biimtrid 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 𝑥)) |
226 | 145, 225 | jaod 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 𝑥)) |
227 | 65, 226 | sylbid 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 𝑥)) |
228 | 227 | ex 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 𝑥))) |
229 | 4, 8, 12, 16, 20, 22, 25, 29, 33, 37, 228 | no3inds 27266 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝐶 ∈ No )
→ ((𝐵 +s 𝐶) <s (𝐴 +s 𝐶) → 𝐵 <s 𝐴)) |
230 | | addscl 34317 |
. . . . . 6
⊢ ((𝐵 ∈
No ∧ 𝐶 ∈
No ) → (𝐵 +s 𝐶) ∈ No
) |
231 | 230 | 3adant1 1130 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝐶 ∈ No )
→ (𝐵 +s 𝐶) ∈
No ) |
232 | | addscl 34317 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ 𝐶 ∈
No ) → (𝐴 +s 𝐶) ∈ No
) |
233 | 232 | 3adant2 1131 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝐶 ∈ No )
→ (𝐴 +s 𝐶) ∈
No ) |
234 | | sltnle 27097 |
. . . . 5
⊢ (((𝐵 +s 𝐶) ∈ No
∧ (𝐴 +s 𝐶) ∈
No ) → ((𝐵 +s
𝐶) <s (𝐴 +s 𝐶) ↔ ¬ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶))) |
235 | 231, 233,
234 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝐶 ∈ No )
→ ((𝐵 +s 𝐶) <s (𝐴 +s 𝐶) ↔ ¬ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶))) |
236 | | sltnle 27097 |
. . . . . 6
⊢ ((𝐵 ∈
No ∧ 𝐴 ∈
No ) → (𝐵 <s 𝐴 ↔ ¬ 𝐴 ≤s 𝐵)) |
237 | 236 | ancoms 459 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐵 <s 𝐴 ↔ ¬ 𝐴 ≤s 𝐵)) |
238 | 237 | 3adant3 1132 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝐶 ∈ No )
→ (𝐵 <s 𝐴 ↔ ¬ 𝐴 ≤s 𝐵)) |
239 | 229, 235,
238 | 3imtr3d 292 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝐶 ∈ No )
→ (¬ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶) → ¬ 𝐴 ≤s 𝐵)) |
240 | 239 | con4d 115 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝐶 ∈ No )
→ (𝐴 ≤s 𝐵 → (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶))) |
241 | | sleadd1im 34322 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝐶 ∈ No )
→ ((𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶) → 𝐴 ≤s 𝐵)) |
242 | 240, 241 | impbid 211 |
1
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝐶 ∈ No )
→ (𝐴 ≤s 𝐵 ↔ (𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶))) |