Step | Hyp | Ref
| Expression |
1 | | ltposr 6848 |
. 2
⊢
<R Po R |
2 | | df-nr 6812 |
. . . 4
⊢
R = ((P × P) /
~R ) |
3 | | breq1 3767 |
. . . . 5
⊢
([〈𝑎, 𝑏〉]
~R = 𝑥 → ([〈𝑎, 𝑏〉] ~R
<R [〈𝑐, 𝑑〉] ~R ↔
𝑥
<R [〈𝑐, 𝑑〉] ~R
)) |
4 | | breq1 3767 |
. . . . . 6
⊢
([〈𝑎, 𝑏〉]
~R = 𝑥 → ([〈𝑎, 𝑏〉] ~R
<R [〈𝑒, 𝑓〉] ~R ↔
𝑥
<R [〈𝑒, 𝑓〉] ~R
)) |
5 | 4 | orbi1d 705 |
. . . . 5
⊢
([〈𝑎, 𝑏〉]
~R = 𝑥 → (([〈𝑎, 𝑏〉] ~R
<R [〈𝑒, 𝑓〉] ~R ∨
[〈𝑒, 𝑓〉]
~R <R [〈𝑐, 𝑑〉] ~R ) ↔
(𝑥
<R [〈𝑒, 𝑓〉] ~R ∨
[〈𝑒, 𝑓〉]
~R <R [〈𝑐, 𝑑〉] ~R
))) |
6 | 3, 5 | imbi12d 223 |
. . . 4
⊢
([〈𝑎, 𝑏〉]
~R = 𝑥 → (([〈𝑎, 𝑏〉] ~R
<R [〈𝑐, 𝑑〉] ~R →
([〈𝑎, 𝑏〉]
~R <R [〈𝑒, 𝑓〉] ~R ∨
[〈𝑒, 𝑓〉]
~R <R [〈𝑐, 𝑑〉] ~R )) ↔
(𝑥
<R [〈𝑐, 𝑑〉] ~R →
(𝑥
<R [〈𝑒, 𝑓〉] ~R ∨
[〈𝑒, 𝑓〉]
~R <R [〈𝑐, 𝑑〉] ~R
)))) |
7 | | breq2 3768 |
. . . . 5
⊢
([〈𝑐, 𝑑〉]
~R = 𝑦 → (𝑥 <R [〈𝑐, 𝑑〉] ~R ↔
𝑥
<R 𝑦)) |
8 | | breq2 3768 |
. . . . . 6
⊢
([〈𝑐, 𝑑〉]
~R = 𝑦 → ([〈𝑒, 𝑓〉] ~R
<R [〈𝑐, 𝑑〉] ~R ↔
[〈𝑒, 𝑓〉]
~R <R 𝑦)) |
9 | 8 | orbi2d 704 |
. . . . 5
⊢
([〈𝑐, 𝑑〉]
~R = 𝑦 → ((𝑥 <R [〈𝑒, 𝑓〉] ~R ∨
[〈𝑒, 𝑓〉]
~R <R [〈𝑐, 𝑑〉] ~R ) ↔
(𝑥
<R [〈𝑒, 𝑓〉] ~R ∨
[〈𝑒, 𝑓〉]
~R <R 𝑦))) |
10 | 7, 9 | imbi12d 223 |
. . . 4
⊢
([〈𝑐, 𝑑〉]
~R = 𝑦 → ((𝑥 <R [〈𝑐, 𝑑〉] ~R →
(𝑥
<R [〈𝑒, 𝑓〉] ~R ∨
[〈𝑒, 𝑓〉]
~R <R [〈𝑐, 𝑑〉] ~R )) ↔
(𝑥
<R 𝑦 → (𝑥 <R [〈𝑒, 𝑓〉] ~R ∨
[〈𝑒, 𝑓〉]
~R <R 𝑦)))) |
11 | | breq2 3768 |
. . . . . 6
⊢
([〈𝑒, 𝑓〉]
~R = 𝑧 → (𝑥 <R [〈𝑒, 𝑓〉] ~R ↔
𝑥
<R 𝑧)) |
12 | | breq1 3767 |
. . . . . 6
⊢
([〈𝑒, 𝑓〉]
~R = 𝑧 → ([〈𝑒, 𝑓〉] ~R
<R 𝑦 ↔ 𝑧 <R 𝑦)) |
13 | 11, 12 | orbi12d 707 |
. . . . 5
⊢
([〈𝑒, 𝑓〉]
~R = 𝑧 → ((𝑥 <R [〈𝑒, 𝑓〉] ~R ∨
[〈𝑒, 𝑓〉]
~R <R 𝑦) ↔ (𝑥 <R 𝑧 ∨ 𝑧 <R 𝑦))) |
14 | 13 | imbi2d 219 |
. . . 4
⊢
([〈𝑒, 𝑓〉]
~R = 𝑧 → ((𝑥 <R 𝑦 → (𝑥 <R [〈𝑒, 𝑓〉] ~R ∨
[〈𝑒, 𝑓〉]
~R <R 𝑦)) ↔ (𝑥 <R 𝑦 → (𝑥 <R 𝑧 ∨ 𝑧 <R 𝑦)))) |
15 | | simp1l 928 |
. . . . . . . . 9
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
𝑎 ∈
P) |
16 | | simp3r 933 |
. . . . . . . . 9
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
𝑓 ∈
P) |
17 | | addclpr 6635 |
. . . . . . . . 9
⊢ ((𝑎 ∈ P ∧
𝑓 ∈ P)
→ (𝑎
+P 𝑓) ∈ P) |
18 | 15, 16, 17 | syl2anc 391 |
. . . . . . . 8
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
(𝑎
+P 𝑓) ∈ P) |
19 | | simp2r 931 |
. . . . . . . 8
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
𝑑 ∈
P) |
20 | | addclpr 6635 |
. . . . . . . 8
⊢ (((𝑎 +P
𝑓) ∈ P
∧ 𝑑 ∈
P) → ((𝑎
+P 𝑓) +P 𝑑) ∈
P) |
21 | 18, 19, 20 | syl2anc 391 |
. . . . . . 7
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
((𝑎
+P 𝑓) +P 𝑑) ∈
P) |
22 | | simp2l 930 |
. . . . . . . . 9
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
𝑐 ∈
P) |
23 | | addclpr 6635 |
. . . . . . . . 9
⊢ ((𝑓 ∈ P ∧
𝑐 ∈ P)
→ (𝑓
+P 𝑐) ∈ P) |
24 | 16, 22, 23 | syl2anc 391 |
. . . . . . . 8
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
(𝑓
+P 𝑐) ∈ P) |
25 | | simp1r 929 |
. . . . . . . 8
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
𝑏 ∈
P) |
26 | | addclpr 6635 |
. . . . . . . 8
⊢ (((𝑓 +P
𝑐) ∈ P
∧ 𝑏 ∈
P) → ((𝑓
+P 𝑐) +P 𝑏) ∈
P) |
27 | 24, 25, 26 | syl2anc 391 |
. . . . . . 7
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
((𝑓
+P 𝑐) +P 𝑏) ∈
P) |
28 | | simp3l 932 |
. . . . . . . . 9
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
𝑒 ∈
P) |
29 | | addclpr 6635 |
. . . . . . . . 9
⊢ ((𝑏 ∈ P ∧
𝑒 ∈ P)
→ (𝑏
+P 𝑒) ∈ P) |
30 | 25, 28, 29 | syl2anc 391 |
. . . . . . . 8
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
(𝑏
+P 𝑒) ∈ P) |
31 | | addclpr 6635 |
. . . . . . . 8
⊢ (((𝑏 +P
𝑒) ∈ P
∧ 𝑑 ∈
P) → ((𝑏
+P 𝑒) +P 𝑑) ∈
P) |
32 | 30, 19, 31 | syl2anc 391 |
. . . . . . 7
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
((𝑏
+P 𝑒) +P 𝑑) ∈
P) |
33 | | ltsopr 6694 |
. . . . . . . 8
⊢
<P Or P |
34 | | sowlin 4057 |
. . . . . . . 8
⊢
((<P Or P ∧ (((𝑎 +P
𝑓)
+P 𝑑) ∈ P ∧ ((𝑓 +P
𝑐)
+P 𝑏) ∈ P ∧ ((𝑏 +P
𝑒)
+P 𝑑) ∈ P)) → (((𝑎 +P
𝑓)
+P 𝑑)<P ((𝑓 +P
𝑐)
+P 𝑏) → (((𝑎 +P 𝑓) +P
𝑑)<P ((𝑏 +P
𝑒)
+P 𝑑) ∨ ((𝑏 +P 𝑒) +P
𝑑)<P ((𝑓 +P
𝑐)
+P 𝑏)))) |
35 | 33, 34 | mpan 400 |
. . . . . . 7
⊢ ((((𝑎 +P
𝑓)
+P 𝑑) ∈ P ∧ ((𝑓 +P
𝑐)
+P 𝑏) ∈ P ∧ ((𝑏 +P
𝑒)
+P 𝑑) ∈ P) → (((𝑎 +P
𝑓)
+P 𝑑)<P ((𝑓 +P
𝑐)
+P 𝑏) → (((𝑎 +P 𝑓) +P
𝑑)<P ((𝑏 +P
𝑒)
+P 𝑑) ∨ ((𝑏 +P 𝑒) +P
𝑑)<P ((𝑓 +P
𝑐)
+P 𝑏)))) |
36 | 21, 27, 32, 35 | syl3anc 1135 |
. . . . . 6
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
(((𝑎
+P 𝑓) +P 𝑑)<P
((𝑓
+P 𝑐) +P 𝑏) → (((𝑎 +P 𝑓) +P
𝑑)<P ((𝑏 +P
𝑒)
+P 𝑑) ∨ ((𝑏 +P 𝑒) +P
𝑑)<P ((𝑓 +P
𝑐)
+P 𝑏)))) |
37 | | addclpr 6635 |
. . . . . . . . 9
⊢ ((𝑎 ∈ P ∧
𝑑 ∈ P)
→ (𝑎
+P 𝑑) ∈ P) |
38 | 15, 19, 37 | syl2anc 391 |
. . . . . . . 8
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
(𝑎
+P 𝑑) ∈ P) |
39 | | addclpr 6635 |
. . . . . . . . 9
⊢ ((𝑏 ∈ P ∧
𝑐 ∈ P)
→ (𝑏
+P 𝑐) ∈ P) |
40 | 25, 22, 39 | syl2anc 391 |
. . . . . . . 8
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
(𝑏
+P 𝑐) ∈ P) |
41 | | ltaprg 6717 |
. . . . . . . 8
⊢ (((𝑎 +P
𝑑) ∈ P
∧ (𝑏
+P 𝑐) ∈ P ∧ 𝑓 ∈ P) →
((𝑎
+P 𝑑)<P (𝑏 +P
𝑐) ↔ (𝑓 +P
(𝑎
+P 𝑑))<P (𝑓 +P
(𝑏
+P 𝑐)))) |
42 | 38, 40, 16, 41 | syl3anc 1135 |
. . . . . . 7
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
((𝑎
+P 𝑑)<P (𝑏 +P
𝑐) ↔ (𝑓 +P
(𝑎
+P 𝑑))<P (𝑓 +P
(𝑏
+P 𝑐)))) |
43 | | addcomprg 6676 |
. . . . . . . . . . 11
⊢ ((𝑟 ∈ P ∧
𝑠 ∈ P)
→ (𝑟
+P 𝑠) = (𝑠 +P 𝑟)) |
44 | 43 | adantl 262 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) ∧
(𝑟 ∈ P
∧ 𝑠 ∈
P)) → (𝑟
+P 𝑠) = (𝑠 +P 𝑟)) |
45 | | addassprg 6677 |
. . . . . . . . . . 11
⊢ ((𝑟 ∈ P ∧
𝑠 ∈ P
∧ 𝑡 ∈
P) → ((𝑟
+P 𝑠) +P 𝑡) = (𝑟 +P (𝑠 +P
𝑡))) |
46 | 45 | adantl 262 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) ∧
(𝑟 ∈ P
∧ 𝑠 ∈
P ∧ 𝑡
∈ P)) → ((𝑟 +P 𝑠) +P
𝑡) = (𝑟 +P (𝑠 +P
𝑡))) |
47 | 16, 15, 19, 44, 46 | caov12d 5682 |
. . . . . . . . 9
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
(𝑓
+P (𝑎 +P 𝑑)) = (𝑎 +P (𝑓 +P
𝑑))) |
48 | 46, 15, 16, 19 | caovassd 5660 |
. . . . . . . . 9
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
((𝑎
+P 𝑓) +P 𝑑) = (𝑎 +P (𝑓 +P
𝑑))) |
49 | 47, 48 | eqtr4d 2075 |
. . . . . . . 8
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
(𝑓
+P (𝑎 +P 𝑑)) = ((𝑎 +P 𝑓) +P
𝑑)) |
50 | 46, 16, 25, 22 | caovassd 5660 |
. . . . . . . . 9
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
((𝑓
+P 𝑏) +P 𝑐) = (𝑓 +P (𝑏 +P
𝑐))) |
51 | 16, 25, 22, 44, 46 | caov32d 5681 |
. . . . . . . . 9
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
((𝑓
+P 𝑏) +P 𝑐) = ((𝑓 +P 𝑐) +P
𝑏)) |
52 | 50, 51 | eqtr3d 2074 |
. . . . . . . 8
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
(𝑓
+P (𝑏 +P 𝑐)) = ((𝑓 +P 𝑐) +P
𝑏)) |
53 | 49, 52 | breq12d 3777 |
. . . . . . 7
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
((𝑓
+P (𝑎 +P 𝑑))<P
(𝑓
+P (𝑏 +P 𝑐)) ↔ ((𝑎 +P 𝑓) +P
𝑑)<P ((𝑓 +P
𝑐)
+P 𝑏))) |
54 | 42, 53 | bitrd 177 |
. . . . . 6
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
((𝑎
+P 𝑑)<P (𝑏 +P
𝑐) ↔ ((𝑎 +P
𝑓)
+P 𝑑)<P ((𝑓 +P
𝑐)
+P 𝑏))) |
55 | | ltaprg 6717 |
. . . . . . . . 9
⊢ ((𝑟 ∈ P ∧
𝑠 ∈ P
∧ 𝑡 ∈
P) → (𝑟<P 𝑠 ↔ (𝑡 +P 𝑟)<P
(𝑡
+P 𝑠))) |
56 | 55 | adantl 262 |
. . . . . . . 8
⊢ ((((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) ∧
(𝑟 ∈ P
∧ 𝑠 ∈
P ∧ 𝑡
∈ P)) → (𝑟<P 𝑠 ↔ (𝑡 +P 𝑟)<P
(𝑡
+P 𝑠))) |
57 | 56, 18, 30, 19, 44 | caovord2d 5670 |
. . . . . . 7
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
((𝑎
+P 𝑓)<P (𝑏 +P
𝑒) ↔ ((𝑎 +P
𝑓)
+P 𝑑)<P ((𝑏 +P
𝑒)
+P 𝑑))) |
58 | | addclpr 6635 |
. . . . . . . . . 10
⊢ ((𝑒 ∈ P ∧
𝑑 ∈ P)
→ (𝑒
+P 𝑑) ∈ P) |
59 | 28, 19, 58 | syl2anc 391 |
. . . . . . . . 9
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
(𝑒
+P 𝑑) ∈ P) |
60 | 56, 59, 24, 25, 44 | caovord2d 5670 |
. . . . . . . 8
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
((𝑒
+P 𝑑)<P (𝑓 +P
𝑐) ↔ ((𝑒 +P
𝑑)
+P 𝑏)<P ((𝑓 +P
𝑐)
+P 𝑏))) |
61 | 46, 25, 28, 19 | caovassd 5660 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
((𝑏
+P 𝑒) +P 𝑑) = (𝑏 +P (𝑒 +P
𝑑))) |
62 | 44, 25, 59 | caovcomd 5657 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
(𝑏
+P (𝑒 +P 𝑑)) = ((𝑒 +P 𝑑) +P
𝑏)) |
63 | 61, 62 | eqtrd 2072 |
. . . . . . . . 9
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
((𝑏
+P 𝑒) +P 𝑑) = ((𝑒 +P 𝑑) +P
𝑏)) |
64 | 63 | breq1d 3774 |
. . . . . . . 8
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
(((𝑏
+P 𝑒) +P 𝑑)<P
((𝑓
+P 𝑐) +P 𝑏) ↔ ((𝑒 +P 𝑑) +P
𝑏)<P ((𝑓 +P
𝑐)
+P 𝑏))) |
65 | 60, 64 | bitr4d 180 |
. . . . . . 7
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
((𝑒
+P 𝑑)<P (𝑓 +P
𝑐) ↔ ((𝑏 +P
𝑒)
+P 𝑑)<P ((𝑓 +P
𝑐)
+P 𝑏))) |
66 | 57, 65 | orbi12d 707 |
. . . . . 6
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
(((𝑎
+P 𝑓)<P (𝑏 +P
𝑒) ∨ (𝑒 +P 𝑑)<P
(𝑓
+P 𝑐)) ↔ (((𝑎 +P 𝑓) +P
𝑑)<P ((𝑏 +P
𝑒)
+P 𝑑) ∨ ((𝑏 +P 𝑒) +P
𝑑)<P ((𝑓 +P
𝑐)
+P 𝑏)))) |
67 | 36, 54, 66 | 3imtr4d 192 |
. . . . 5
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
((𝑎
+P 𝑑)<P (𝑏 +P
𝑐) → ((𝑎 +P
𝑓)<P (𝑏 +P
𝑒) ∨ (𝑒 +P 𝑑)<P
(𝑓
+P 𝑐)))) |
68 | | ltsrprg 6832 |
. . . . . 6
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P)) → ([〈𝑎, 𝑏〉] ~R
<R [〈𝑐, 𝑑〉] ~R ↔
(𝑎
+P 𝑑)<P (𝑏 +P
𝑐))) |
69 | 68 | 3adant3 924 |
. . . . 5
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
([〈𝑎, 𝑏〉]
~R <R [〈𝑐, 𝑑〉] ~R ↔
(𝑎
+P 𝑑)<P (𝑏 +P
𝑐))) |
70 | | ltsrprg 6832 |
. . . . . . 7
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑒 ∈
P ∧ 𝑓
∈ P)) → ([〈𝑎, 𝑏〉] ~R
<R [〈𝑒, 𝑓〉] ~R ↔
(𝑎
+P 𝑓)<P (𝑏 +P
𝑒))) |
71 | 70 | 3adant2 923 |
. . . . . 6
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
([〈𝑎, 𝑏〉]
~R <R [〈𝑒, 𝑓〉] ~R ↔
(𝑎
+P 𝑓)<P (𝑏 +P
𝑒))) |
72 | | ltsrprg 6832 |
. . . . . . . 8
⊢ (((𝑒 ∈ P ∧
𝑓 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P)) → ([〈𝑒, 𝑓〉] ~R
<R [〈𝑐, 𝑑〉] ~R ↔
(𝑒
+P 𝑑)<P (𝑓 +P
𝑐))) |
73 | 72 | ancoms 255 |
. . . . . . 7
⊢ (((𝑐 ∈ P ∧
𝑑 ∈ P)
∧ (𝑒 ∈
P ∧ 𝑓
∈ P)) → ([〈𝑒, 𝑓〉] ~R
<R [〈𝑐, 𝑑〉] ~R ↔
(𝑒
+P 𝑑)<P (𝑓 +P
𝑐))) |
74 | 73 | 3adant1 922 |
. . . . . 6
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
([〈𝑒, 𝑓〉]
~R <R [〈𝑐, 𝑑〉] ~R ↔
(𝑒
+P 𝑑)<P (𝑓 +P
𝑐))) |
75 | 71, 74 | orbi12d 707 |
. . . . 5
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
(([〈𝑎, 𝑏〉]
~R <R [〈𝑒, 𝑓〉] ~R ∨
[〈𝑒, 𝑓〉]
~R <R [〈𝑐, 𝑑〉] ~R ) ↔
((𝑎
+P 𝑓)<P (𝑏 +P
𝑒) ∨ (𝑒 +P 𝑑)<P
(𝑓
+P 𝑐)))) |
76 | 67, 69, 75 | 3imtr4d 192 |
. . . 4
⊢ (((𝑎 ∈ P ∧
𝑏 ∈ P)
∧ (𝑐 ∈
P ∧ 𝑑
∈ P) ∧ (𝑒 ∈ P ∧ 𝑓 ∈ P)) →
([〈𝑎, 𝑏〉]
~R <R [〈𝑐, 𝑑〉] ~R →
([〈𝑎, 𝑏〉]
~R <R [〈𝑒, 𝑓〉] ~R ∨
[〈𝑒, 𝑓〉]
~R <R [〈𝑐, 𝑑〉] ~R
))) |
77 | 2, 6, 10, 14, 76 | 3ecoptocl 6195 |
. . 3
⊢ ((𝑥 ∈ R ∧
𝑦 ∈ R
∧ 𝑧 ∈
R) → (𝑥
<R 𝑦 → (𝑥 <R 𝑧 ∨ 𝑧 <R 𝑦))) |
78 | 77 | rgen3 2406 |
. 2
⊢
∀𝑥 ∈
R ∀𝑦
∈ R ∀𝑧 ∈ R (𝑥 <R 𝑦 → (𝑥 <R 𝑧 ∨ 𝑧 <R 𝑦)) |
79 | | df-iso 4034 |
. 2
⊢ (
<R Or R ↔ (
<R Po R ∧ ∀𝑥 ∈ R
∀𝑦 ∈
R ∀𝑧
∈ R (𝑥
<R 𝑦 → (𝑥 <R 𝑧 ∨ 𝑧 <R 𝑦)))) |
80 | 1, 78, 79 | mpbir2an 849 |
1
⊢
<R Or R |