| Step | Hyp | Ref
| Expression |
| 1 | | df-nr 11096 |
. . 3
⊢
R = ((P × P) /
~R ) |
| 2 | | breq1 5146 |
. . . 4
⊢
([〈𝑥, 𝑦〉]
~R = 𝑓 → ([〈𝑥, 𝑦〉] ~R
<R [〈𝑧, 𝑤〉] ~R ↔
𝑓
<R [〈𝑧, 𝑤〉] ~R
)) |
| 3 | | eqeq1 2741 |
. . . . . 6
⊢
([〈𝑥, 𝑦〉]
~R = 𝑓 → ([〈𝑥, 𝑦〉] ~R =
[〈𝑧, 𝑤〉]
~R ↔ 𝑓 = [〈𝑧, 𝑤〉] ~R
)) |
| 4 | | breq2 5147 |
. . . . . 6
⊢
([〈𝑥, 𝑦〉]
~R = 𝑓 → ([〈𝑧, 𝑤〉] ~R
<R [〈𝑥, 𝑦〉] ~R ↔
[〈𝑧, 𝑤〉]
~R <R 𝑓)) |
| 5 | 3, 4 | orbi12d 919 |
. . . . 5
⊢
([〈𝑥, 𝑦〉]
~R = 𝑓 → (([〈𝑥, 𝑦〉] ~R =
[〈𝑧, 𝑤〉]
~R ∨ [〈𝑧, 𝑤〉] ~R
<R [〈𝑥, 𝑦〉] ~R ) ↔
(𝑓 = [〈𝑧, 𝑤〉] ~R ∨
[〈𝑧, 𝑤〉]
~R <R 𝑓))) |
| 6 | 5 | notbid 318 |
. . . 4
⊢
([〈𝑥, 𝑦〉]
~R = 𝑓 → (¬ ([〈𝑥, 𝑦〉] ~R =
[〈𝑧, 𝑤〉]
~R ∨ [〈𝑧, 𝑤〉] ~R
<R [〈𝑥, 𝑦〉] ~R ) ↔
¬ (𝑓 = [〈𝑧, 𝑤〉] ~R ∨
[〈𝑧, 𝑤〉]
~R <R 𝑓))) |
| 7 | 2, 6 | bibi12d 345 |
. . 3
⊢
([〈𝑥, 𝑦〉]
~R = 𝑓 → (([〈𝑥, 𝑦〉] ~R
<R [〈𝑧, 𝑤〉] ~R ↔
¬ ([〈𝑥, 𝑦〉]
~R = [〈𝑧, 𝑤〉] ~R ∨
[〈𝑧, 𝑤〉]
~R <R [〈𝑥, 𝑦〉] ~R )) ↔
(𝑓
<R [〈𝑧, 𝑤〉] ~R ↔
¬ (𝑓 = [〈𝑧, 𝑤〉] ~R ∨
[〈𝑧, 𝑤〉]
~R <R 𝑓)))) |
| 8 | | breq2 5147 |
. . . 4
⊢
([〈𝑧, 𝑤〉]
~R = 𝑔 → (𝑓 <R [〈𝑧, 𝑤〉] ~R ↔
𝑓
<R 𝑔)) |
| 9 | | eqeq2 2749 |
. . . . . 6
⊢
([〈𝑧, 𝑤〉]
~R = 𝑔 → (𝑓 = [〈𝑧, 𝑤〉] ~R ↔
𝑓 = 𝑔)) |
| 10 | | breq1 5146 |
. . . . . 6
⊢
([〈𝑧, 𝑤〉]
~R = 𝑔 → ([〈𝑧, 𝑤〉] ~R
<R 𝑓 ↔ 𝑔 <R 𝑓)) |
| 11 | 9, 10 | orbi12d 919 |
. . . . 5
⊢
([〈𝑧, 𝑤〉]
~R = 𝑔 → ((𝑓 = [〈𝑧, 𝑤〉] ~R ∨
[〈𝑧, 𝑤〉]
~R <R 𝑓) ↔ (𝑓 = 𝑔 ∨ 𝑔 <R 𝑓))) |
| 12 | 11 | notbid 318 |
. . . 4
⊢
([〈𝑧, 𝑤〉]
~R = 𝑔 → (¬ (𝑓 = [〈𝑧, 𝑤〉] ~R ∨
[〈𝑧, 𝑤〉]
~R <R 𝑓) ↔ ¬ (𝑓 = 𝑔 ∨ 𝑔 <R 𝑓))) |
| 13 | 8, 12 | bibi12d 345 |
. . 3
⊢
([〈𝑧, 𝑤〉]
~R = 𝑔 → ((𝑓 <R [〈𝑧, 𝑤〉] ~R ↔
¬ (𝑓 = [〈𝑧, 𝑤〉] ~R ∨
[〈𝑧, 𝑤〉]
~R <R 𝑓)) ↔ (𝑓 <R 𝑔 ↔ ¬ (𝑓 = 𝑔 ∨ 𝑔 <R 𝑓)))) |
| 14 | | ltsrpr 11117 |
. . . 4
⊢
([〈𝑥, 𝑦〉]
~R <R [〈𝑧, 𝑤〉] ~R ↔
(𝑥
+P 𝑤)<P (𝑦 +P
𝑧)) |
| 15 | | addclpr 11058 |
. . . . . . 7
⊢ ((𝑥 ∈ P ∧
𝑤 ∈ P)
→ (𝑥
+P 𝑤) ∈ P) |
| 16 | | addclpr 11058 |
. . . . . . 7
⊢ ((𝑦 ∈ P ∧
𝑧 ∈ P)
→ (𝑦
+P 𝑧) ∈ P) |
| 17 | | ltsopr 11072 |
. . . . . . . 8
⊢
<P Or P |
| 18 | | sotric 5622 |
. . . . . . . 8
⊢
((<P Or P ∧ ((𝑥 +P
𝑤) ∈ P
∧ (𝑦
+P 𝑧) ∈ P)) → ((𝑥 +P
𝑤)<P (𝑦 +P
𝑧) ↔ ¬ ((𝑥 +P
𝑤) = (𝑦 +P 𝑧) ∨ (𝑦 +P 𝑧)<P
(𝑥
+P 𝑤)))) |
| 19 | 17, 18 | mpan 690 |
. . . . . . 7
⊢ (((𝑥 +P
𝑤) ∈ P
∧ (𝑦
+P 𝑧) ∈ P) → ((𝑥 +P
𝑤)<P (𝑦 +P
𝑧) ↔ ¬ ((𝑥 +P
𝑤) = (𝑦 +P 𝑧) ∨ (𝑦 +P 𝑧)<P
(𝑥
+P 𝑤)))) |
| 20 | 15, 16, 19 | syl2an 596 |
. . . . . 6
⊢ (((𝑥 ∈ P ∧
𝑤 ∈ P)
∧ (𝑦 ∈
P ∧ 𝑧
∈ P)) → ((𝑥 +P 𝑤)<P
(𝑦
+P 𝑧) ↔ ¬ ((𝑥 +P 𝑤) = (𝑦 +P 𝑧) ∨ (𝑦 +P 𝑧)<P
(𝑥
+P 𝑤)))) |
| 21 | 20 | an42s 661 |
. . . . 5
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → ((𝑥 +P 𝑤)<P
(𝑦
+P 𝑧) ↔ ¬ ((𝑥 +P 𝑤) = (𝑦 +P 𝑧) ∨ (𝑦 +P 𝑧)<P
(𝑥
+P 𝑤)))) |
| 22 | | enreceq 11106 |
. . . . . . 7
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → ([〈𝑥, 𝑦〉] ~R =
[〈𝑧, 𝑤〉]
~R ↔ (𝑥 +P 𝑤) = (𝑦 +P 𝑧))) |
| 23 | | ltsrpr 11117 |
. . . . . . . . 9
⊢
([〈𝑧, 𝑤〉]
~R <R [〈𝑥, 𝑦〉] ~R ↔
(𝑧
+P 𝑦)<P (𝑤 +P
𝑥)) |
| 24 | | addcompr 11061 |
. . . . . . . . . 10
⊢ (𝑧 +P
𝑦) = (𝑦 +P 𝑧) |
| 25 | | addcompr 11061 |
. . . . . . . . . 10
⊢ (𝑤 +P
𝑥) = (𝑥 +P 𝑤) |
| 26 | 24, 25 | breq12i 5152 |
. . . . . . . . 9
⊢ ((𝑧 +P
𝑦)<P (𝑤 +P
𝑥) ↔ (𝑦 +P
𝑧)<P (𝑥 +P
𝑤)) |
| 27 | 23, 26 | bitri 275 |
. . . . . . . 8
⊢
([〈𝑧, 𝑤〉]
~R <R [〈𝑥, 𝑦〉] ~R ↔
(𝑦
+P 𝑧)<P (𝑥 +P
𝑤)) |
| 28 | 27 | a1i 11 |
. . . . . . 7
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → ([〈𝑧, 𝑤〉] ~R
<R [〈𝑥, 𝑦〉] ~R ↔
(𝑦
+P 𝑧)<P (𝑥 +P
𝑤))) |
| 29 | 22, 28 | orbi12d 919 |
. . . . . 6
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → (([〈𝑥, 𝑦〉] ~R =
[〈𝑧, 𝑤〉]
~R ∨ [〈𝑧, 𝑤〉] ~R
<R [〈𝑥, 𝑦〉] ~R ) ↔
((𝑥
+P 𝑤) = (𝑦 +P 𝑧) ∨ (𝑦 +P 𝑧)<P
(𝑥
+P 𝑤)))) |
| 30 | 29 | notbid 318 |
. . . . 5
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → (¬ ([〈𝑥, 𝑦〉] ~R =
[〈𝑧, 𝑤〉]
~R ∨ [〈𝑧, 𝑤〉] ~R
<R [〈𝑥, 𝑦〉] ~R ) ↔
¬ ((𝑥
+P 𝑤) = (𝑦 +P 𝑧) ∨ (𝑦 +P 𝑧)<P
(𝑥
+P 𝑤)))) |
| 31 | 21, 30 | bitr4d 282 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → ((𝑥 +P 𝑤)<P
(𝑦
+P 𝑧) ↔ ¬ ([〈𝑥, 𝑦〉] ~R =
[〈𝑧, 𝑤〉]
~R ∨ [〈𝑧, 𝑤〉] ~R
<R [〈𝑥, 𝑦〉] ~R
))) |
| 32 | 14, 31 | bitrid 283 |
. . 3
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → ([〈𝑥, 𝑦〉] ~R
<R [〈𝑧, 𝑤〉] ~R ↔
¬ ([〈𝑥, 𝑦〉]
~R = [〈𝑧, 𝑤〉] ~R ∨
[〈𝑧, 𝑤〉]
~R <R [〈𝑥, 𝑦〉] ~R
))) |
| 33 | 1, 7, 13, 32 | 2ecoptocl 8848 |
. 2
⊢ ((𝑓 ∈ R ∧
𝑔 ∈ R)
→ (𝑓
<R 𝑔 ↔ ¬ (𝑓 = 𝑔 ∨ 𝑔 <R 𝑓))) |
| 34 | 2 | anbi1d 631 |
. . . 4
⊢
([〈𝑥, 𝑦〉]
~R = 𝑓 → (([〈𝑥, 𝑦〉] ~R
<R [〈𝑧, 𝑤〉] ~R ∧
[〈𝑧, 𝑤〉]
~R <R [〈𝑣, 𝑢〉] ~R ) ↔
(𝑓
<R [〈𝑧, 𝑤〉] ~R ∧
[〈𝑧, 𝑤〉]
~R <R [〈𝑣, 𝑢〉] ~R
))) |
| 35 | | breq1 5146 |
. . . 4
⊢
([〈𝑥, 𝑦〉]
~R = 𝑓 → ([〈𝑥, 𝑦〉] ~R
<R [〈𝑣, 𝑢〉] ~R ↔
𝑓
<R [〈𝑣, 𝑢〉] ~R
)) |
| 36 | 34, 35 | imbi12d 344 |
. . 3
⊢
([〈𝑥, 𝑦〉]
~R = 𝑓 → ((([〈𝑥, 𝑦〉] ~R
<R [〈𝑧, 𝑤〉] ~R ∧
[〈𝑧, 𝑤〉]
~R <R [〈𝑣, 𝑢〉] ~R ) →
[〈𝑥, 𝑦〉]
~R <R [〈𝑣, 𝑢〉] ~R ) ↔
((𝑓
<R [〈𝑧, 𝑤〉] ~R ∧
[〈𝑧, 𝑤〉]
~R <R [〈𝑣, 𝑢〉] ~R ) →
𝑓
<R [〈𝑣, 𝑢〉] ~R
))) |
| 37 | | breq1 5146 |
. . . . 5
⊢
([〈𝑧, 𝑤〉]
~R = 𝑔 → ([〈𝑧, 𝑤〉] ~R
<R [〈𝑣, 𝑢〉] ~R ↔
𝑔
<R [〈𝑣, 𝑢〉] ~R
)) |
| 38 | 8, 37 | anbi12d 632 |
. . . 4
⊢
([〈𝑧, 𝑤〉]
~R = 𝑔 → ((𝑓 <R [〈𝑧, 𝑤〉] ~R ∧
[〈𝑧, 𝑤〉]
~R <R [〈𝑣, 𝑢〉] ~R ) ↔
(𝑓
<R 𝑔 ∧ 𝑔 <R [〈𝑣, 𝑢〉] ~R
))) |
| 39 | 38 | imbi1d 341 |
. . 3
⊢
([〈𝑧, 𝑤〉]
~R = 𝑔 → (((𝑓 <R [〈𝑧, 𝑤〉] ~R ∧
[〈𝑧, 𝑤〉]
~R <R [〈𝑣, 𝑢〉] ~R ) →
𝑓
<R [〈𝑣, 𝑢〉] ~R ) ↔
((𝑓
<R 𝑔 ∧ 𝑔 <R [〈𝑣, 𝑢〉] ~R ) →
𝑓
<R [〈𝑣, 𝑢〉] ~R
))) |
| 40 | | breq2 5147 |
. . . . 5
⊢
([〈𝑣, 𝑢〉]
~R = ℎ → (𝑔 <R [〈𝑣, 𝑢〉] ~R ↔
𝑔
<R ℎ)) |
| 41 | 40 | anbi2d 630 |
. . . 4
⊢
([〈𝑣, 𝑢〉]
~R = ℎ → ((𝑓 <R 𝑔 ∧ 𝑔 <R [〈𝑣, 𝑢〉] ~R ) ↔
(𝑓
<R 𝑔 ∧ 𝑔 <R ℎ))) |
| 42 | | breq2 5147 |
. . . 4
⊢
([〈𝑣, 𝑢〉]
~R = ℎ → (𝑓 <R [〈𝑣, 𝑢〉] ~R ↔
𝑓
<R ℎ)) |
| 43 | 41, 42 | imbi12d 344 |
. . 3
⊢
([〈𝑣, 𝑢〉]
~R = ℎ → (((𝑓 <R 𝑔 ∧ 𝑔 <R [〈𝑣, 𝑢〉] ~R ) →
𝑓
<R [〈𝑣, 𝑢〉] ~R ) ↔
((𝑓
<R 𝑔 ∧ 𝑔 <R ℎ) → 𝑓 <R ℎ))) |
| 44 | | ovex 7464 |
. . . . . . . . . 10
⊢ (𝑥 +P
𝑤) ∈
V |
| 45 | | ovex 7464 |
. . . . . . . . . 10
⊢ (𝑦 +P
𝑧) ∈
V |
| 46 | | ltapr 11085 |
. . . . . . . . . 10
⊢ (ℎ ∈ P →
(𝑓<P 𝑔 ↔ (ℎ +P 𝑓)<P
(ℎ
+P 𝑔))) |
| 47 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑢 ∈ V |
| 48 | | addcompr 11061 |
. . . . . . . . . 10
⊢ (𝑓 +P
𝑔) = (𝑔 +P 𝑓) |
| 49 | 44, 45, 46, 47, 48 | caovord2 7645 |
. . . . . . . . 9
⊢ (𝑢 ∈ P →
((𝑥
+P 𝑤)<P (𝑦 +P
𝑧) ↔ ((𝑥 +P
𝑤)
+P 𝑢)<P ((𝑦 +P
𝑧)
+P 𝑢))) |
| 50 | | addasspr 11062 |
. . . . . . . . . 10
⊢ ((𝑥 +P
𝑤)
+P 𝑢) = (𝑥 +P (𝑤 +P
𝑢)) |
| 51 | | addasspr 11062 |
. . . . . . . . . 10
⊢ ((𝑦 +P
𝑧)
+P 𝑢) = (𝑦 +P (𝑧 +P
𝑢)) |
| 52 | 50, 51 | breq12i 5152 |
. . . . . . . . 9
⊢ (((𝑥 +P
𝑤)
+P 𝑢)<P ((𝑦 +P
𝑧)
+P 𝑢) ↔ (𝑥 +P (𝑤 +P
𝑢))<P (𝑦 +P
(𝑧
+P 𝑢))) |
| 53 | 49, 52 | bitrdi 287 |
. . . . . . . 8
⊢ (𝑢 ∈ P →
((𝑥
+P 𝑤)<P (𝑦 +P
𝑧) ↔ (𝑥 +P
(𝑤
+P 𝑢))<P (𝑦 +P
(𝑧
+P 𝑢)))) |
| 54 | 14, 53 | bitrid 283 |
. . . . . . 7
⊢ (𝑢 ∈ P →
([〈𝑥, 𝑦〉]
~R <R [〈𝑧, 𝑤〉] ~R ↔
(𝑥
+P (𝑤 +P 𝑢))<P
(𝑦
+P (𝑧 +P 𝑢)))) |
| 55 | | ltsrpr 11117 |
. . . . . . . 8
⊢
([〈𝑧, 𝑤〉]
~R <R [〈𝑣, 𝑢〉] ~R ↔
(𝑧
+P 𝑢)<P (𝑤 +P
𝑣)) |
| 56 | | ltapr 11085 |
. . . . . . . 8
⊢ (𝑦 ∈ P →
((𝑧
+P 𝑢)<P (𝑤 +P
𝑣) ↔ (𝑦 +P
(𝑧
+P 𝑢))<P (𝑦 +P
(𝑤
+P 𝑣)))) |
| 57 | 55, 56 | bitrid 283 |
. . . . . . 7
⊢ (𝑦 ∈ P →
([〈𝑧, 𝑤〉]
~R <R [〈𝑣, 𝑢〉] ~R ↔
(𝑦
+P (𝑧 +P 𝑢))<P
(𝑦
+P (𝑤 +P 𝑣)))) |
| 58 | 54, 57 | bi2anan9r 639 |
. . . . . 6
⊢ ((𝑦 ∈ P ∧
𝑢 ∈ P)
→ (([〈𝑥, 𝑦〉]
~R <R [〈𝑧, 𝑤〉] ~R ∧
[〈𝑧, 𝑤〉]
~R <R [〈𝑣, 𝑢〉] ~R ) ↔
((𝑥
+P (𝑤 +P 𝑢))<P
(𝑦
+P (𝑧 +P 𝑢)) ∧ (𝑦 +P (𝑧 +P
𝑢))<P (𝑦 +P
(𝑤
+P 𝑣))))) |
| 59 | | ltrelpr 11038 |
. . . . . . . 8
⊢
<P ⊆ (P ×
P) |
| 60 | 17, 59 | sotri 6147 |
. . . . . . 7
⊢ (((𝑥 +P
(𝑤
+P 𝑢))<P (𝑦 +P
(𝑧
+P 𝑢)) ∧ (𝑦 +P (𝑧 +P
𝑢))<P (𝑦 +P
(𝑤
+P 𝑣))) → (𝑥 +P (𝑤 +P
𝑢))<P (𝑦 +P
(𝑤
+P 𝑣))) |
| 61 | | dmplp 11052 |
. . . . . . . . 9
⊢ dom
+P = (P ×
P) |
| 62 | | 0npr 11032 |
. . . . . . . . 9
⊢ ¬
∅ ∈ P |
| 63 | | ltapr 11085 |
. . . . . . . . 9
⊢ (𝑤 ∈ P →
((𝑥
+P 𝑢)<P (𝑦 +P
𝑣) ↔ (𝑤 +P
(𝑥
+P 𝑢))<P (𝑤 +P
(𝑦
+P 𝑣)))) |
| 64 | 61, 59, 62, 63 | ndmovordi 7624 |
. . . . . . . 8
⊢ ((𝑤 +P
(𝑥
+P 𝑢))<P (𝑤 +P
(𝑦
+P 𝑣)) → (𝑥 +P 𝑢)<P
(𝑦
+P 𝑣)) |
| 65 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
| 66 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑤 ∈ V |
| 67 | | addasspr 11062 |
. . . . . . . . . 10
⊢ ((𝑓 +P
𝑔)
+P ℎ) = (𝑓 +P (𝑔 +P
ℎ)) |
| 68 | 65, 66, 47, 48, 67 | caov12 7661 |
. . . . . . . . 9
⊢ (𝑥 +P
(𝑤
+P 𝑢)) = (𝑤 +P (𝑥 +P
𝑢)) |
| 69 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
| 70 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑣 ∈ V |
| 71 | 69, 66, 70, 48, 67 | caov12 7661 |
. . . . . . . . 9
⊢ (𝑦 +P
(𝑤
+P 𝑣)) = (𝑤 +P (𝑦 +P
𝑣)) |
| 72 | 68, 71 | breq12i 5152 |
. . . . . . . 8
⊢ ((𝑥 +P
(𝑤
+P 𝑢))<P (𝑦 +P
(𝑤
+P 𝑣)) ↔ (𝑤 +P (𝑥 +P
𝑢))<P (𝑤 +P
(𝑦
+P 𝑣))) |
| 73 | | ltsrpr 11117 |
. . . . . . . 8
⊢
([〈𝑥, 𝑦〉]
~R <R [〈𝑣, 𝑢〉] ~R ↔
(𝑥
+P 𝑢)<P (𝑦 +P
𝑣)) |
| 74 | 64, 72, 73 | 3imtr4i 292 |
. . . . . . 7
⊢ ((𝑥 +P
(𝑤
+P 𝑢))<P (𝑦 +P
(𝑤
+P 𝑣)) → [〈𝑥, 𝑦〉] ~R
<R [〈𝑣, 𝑢〉] ~R
) |
| 75 | 60, 74 | syl 17 |
. . . . . 6
⊢ (((𝑥 +P
(𝑤
+P 𝑢))<P (𝑦 +P
(𝑧
+P 𝑢)) ∧ (𝑦 +P (𝑧 +P
𝑢))<P (𝑦 +P
(𝑤
+P 𝑣))) → [〈𝑥, 𝑦〉] ~R
<R [〈𝑣, 𝑢〉] ~R
) |
| 76 | 58, 75 | biimtrdi 253 |
. . . . 5
⊢ ((𝑦 ∈ P ∧
𝑢 ∈ P)
→ (([〈𝑥, 𝑦〉]
~R <R [〈𝑧, 𝑤〉] ~R ∧
[〈𝑧, 𝑤〉]
~R <R [〈𝑣, 𝑢〉] ~R ) →
[〈𝑥, 𝑦〉]
~R <R [〈𝑣, 𝑢〉] ~R
)) |
| 77 | 76 | ad2ant2l 746 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑣 ∈
P ∧ 𝑢
∈ P)) → (([〈𝑥, 𝑦〉] ~R
<R [〈𝑧, 𝑤〉] ~R ∧
[〈𝑧, 𝑤〉]
~R <R [〈𝑣, 𝑢〉] ~R ) →
[〈𝑥, 𝑦〉]
~R <R [〈𝑣, 𝑢〉] ~R
)) |
| 78 | 77 | 3adant2 1132 |
. . 3
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P) ∧ (𝑣 ∈ P ∧ 𝑢 ∈ P)) →
(([〈𝑥, 𝑦〉]
~R <R [〈𝑧, 𝑤〉] ~R ∧
[〈𝑧, 𝑤〉]
~R <R [〈𝑣, 𝑢〉] ~R ) →
[〈𝑥, 𝑦〉]
~R <R [〈𝑣, 𝑢〉] ~R
)) |
| 79 | 1, 36, 39, 43, 78 | 3ecoptocl 8849 |
. 2
⊢ ((𝑓 ∈ R ∧
𝑔 ∈ R
∧ ℎ ∈
R) → ((𝑓
<R 𝑔 ∧ 𝑔 <R ℎ) → 𝑓 <R ℎ)) |
| 80 | 33, 79 | isso2i 5629 |
1
⊢
<R Or R |