Step | Hyp | Ref
| Expression |
1 | | df-nr 10670 |
. . 3
⊢
R = ((P × P) /
~R ) |
2 | | breq1 5056 |
. . . 4
⊢
([〈𝑥, 𝑦〉]
~R = 𝑓 → ([〈𝑥, 𝑦〉] ~R
<R [〈𝑧, 𝑤〉] ~R ↔
𝑓
<R [〈𝑧, 𝑤〉] ~R
)) |
3 | | eqeq1 2741 |
. . . . . 6
⊢
([〈𝑥, 𝑦〉]
~R = 𝑓 → ([〈𝑥, 𝑦〉] ~R =
[〈𝑧, 𝑤〉]
~R ↔ 𝑓 = [〈𝑧, 𝑤〉] ~R
)) |
4 | | breq2 5057 |
. . . . . 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 321 |
. . . 4
⊢
([〈𝑥, 𝑦〉]
~R = 𝑓 → (¬ ([〈𝑥, 𝑦〉] ~R =
[〈𝑧, 𝑤〉]
~R ∨ [〈𝑧, 𝑤〉] ~R
<R [〈𝑥, 𝑦〉] ~R ) ↔
¬ (𝑓 = [〈𝑧, 𝑤〉] ~R ∨
[〈𝑧, 𝑤〉]
~R <R 𝑓))) |
7 | 2, 6 | bibi12d 349 |
. . 3
⊢
([〈𝑥, 𝑦〉]
~R = 𝑓 → (([〈𝑥, 𝑦〉] ~R
<R [〈𝑧, 𝑤〉] ~R ↔
¬ ([〈𝑥, 𝑦〉]
~R = [〈𝑧, 𝑤〉] ~R ∨
[〈𝑧, 𝑤〉]
~R <R [〈𝑥, 𝑦〉] ~R )) ↔
(𝑓
<R [〈𝑧, 𝑤〉] ~R ↔
¬ (𝑓 = [〈𝑧, 𝑤〉] ~R ∨
[〈𝑧, 𝑤〉]
~R <R 𝑓)))) |
8 | | breq2 5057 |
. . . 4
⊢
([〈𝑧, 𝑤〉]
~R = 𝑔 → (𝑓 <R [〈𝑧, 𝑤〉] ~R ↔
𝑓
<R 𝑔)) |
9 | | eqeq2 2749 |
. . . . . 6
⊢
([〈𝑧, 𝑤〉]
~R = 𝑔 → (𝑓 = [〈𝑧, 𝑤〉] ~R ↔
𝑓 = 𝑔)) |
10 | | breq1 5056 |
. . . . . 6
⊢
([〈𝑧, 𝑤〉]
~R = 𝑔 → ([〈𝑧, 𝑤〉] ~R
<R 𝑓 ↔ 𝑔 <R 𝑓)) |
11 | 9, 10 | orbi12d 919 |
. . . . 5
⊢
([〈𝑧, 𝑤〉]
~R = 𝑔 → ((𝑓 = [〈𝑧, 𝑤〉] ~R ∨
[〈𝑧, 𝑤〉]
~R <R 𝑓) ↔ (𝑓 = 𝑔 ∨ 𝑔 <R 𝑓))) |
12 | 11 | notbid 321 |
. . . 4
⊢
([〈𝑧, 𝑤〉]
~R = 𝑔 → (¬ (𝑓 = [〈𝑧, 𝑤〉] ~R ∨
[〈𝑧, 𝑤〉]
~R <R 𝑓) ↔ ¬ (𝑓 = 𝑔 ∨ 𝑔 <R 𝑓))) |
13 | 8, 12 | bibi12d 349 |
. . 3
⊢
([〈𝑧, 𝑤〉]
~R = 𝑔 → ((𝑓 <R [〈𝑧, 𝑤〉] ~R ↔
¬ (𝑓 = [〈𝑧, 𝑤〉] ~R ∨
[〈𝑧, 𝑤〉]
~R <R 𝑓)) ↔ (𝑓 <R 𝑔 ↔ ¬ (𝑓 = 𝑔 ∨ 𝑔 <R 𝑓)))) |
14 | | ltsrpr 10691 |
. . . 4
⊢
([〈𝑥, 𝑦〉]
~R <R [〈𝑧, 𝑤〉] ~R ↔
(𝑥
+P 𝑤)<P (𝑦 +P
𝑧)) |
15 | | addclpr 10632 |
. . . . . . 7
⊢ ((𝑥 ∈ P ∧
𝑤 ∈ P)
→ (𝑥
+P 𝑤) ∈ P) |
16 | | addclpr 10632 |
. . . . . . 7
⊢ ((𝑦 ∈ P ∧
𝑧 ∈ P)
→ (𝑦
+P 𝑧) ∈ P) |
17 | | ltsopr 10646 |
. . . . . . . 8
⊢
<P Or P |
18 | | sotric 5496 |
. . . . . . . 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 599 |
. . . . . 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 10680 |
. . . . . . 7
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → ([〈𝑥, 𝑦〉] ~R =
[〈𝑧, 𝑤〉]
~R ↔ (𝑥 +P 𝑤) = (𝑦 +P 𝑧))) |
23 | | ltsrpr 10691 |
. . . . . . . . 9
⊢
([〈𝑧, 𝑤〉]
~R <R [〈𝑥, 𝑦〉] ~R ↔
(𝑧
+P 𝑦)<P (𝑤 +P
𝑥)) |
24 | | addcompr 10635 |
. . . . . . . . . 10
⊢ (𝑧 +P
𝑦) = (𝑦 +P 𝑧) |
25 | | addcompr 10635 |
. . . . . . . . . 10
⊢ (𝑤 +P
𝑥) = (𝑥 +P 𝑤) |
26 | 24, 25 | breq12i 5062 |
. . . . . . . . 9
⊢ ((𝑧 +P
𝑦)<P (𝑤 +P
𝑥) ↔ (𝑦 +P
𝑧)<P (𝑥 +P
𝑤)) |
27 | 23, 26 | bitri 278 |
. . . . . . . 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 321 |
. . . . 5
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → (¬ ([〈𝑥, 𝑦〉] ~R =
[〈𝑧, 𝑤〉]
~R ∨ [〈𝑧, 𝑤〉] ~R
<R [〈𝑥, 𝑦〉] ~R ) ↔
¬ ((𝑥
+P 𝑤) = (𝑦 +P 𝑧) ∨ (𝑦 +P 𝑧)<P
(𝑥
+P 𝑤)))) |
31 | 21, 30 | bitr4d 285 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → ((𝑥 +P 𝑤)<P
(𝑦
+P 𝑧) ↔ ¬ ([〈𝑥, 𝑦〉] ~R =
[〈𝑧, 𝑤〉]
~R ∨ [〈𝑧, 𝑤〉] ~R
<R [〈𝑥, 𝑦〉] ~R
))) |
32 | 14, 31 | syl5bb 286 |
. . 3
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → ([〈𝑥, 𝑦〉] ~R
<R [〈𝑧, 𝑤〉] ~R ↔
¬ ([〈𝑥, 𝑦〉]
~R = [〈𝑧, 𝑤〉] ~R ∨
[〈𝑧, 𝑤〉]
~R <R [〈𝑥, 𝑦〉] ~R
))) |
33 | 1, 7, 13, 32 | 2ecoptocl 8490 |
. 2
⊢ ((𝑓 ∈ R ∧
𝑔 ∈ R)
→ (𝑓
<R 𝑔 ↔ ¬ (𝑓 = 𝑔 ∨ 𝑔 <R 𝑓))) |
34 | 2 | anbi1d 633 |
. . . 4
⊢
([〈𝑥, 𝑦〉]
~R = 𝑓 → (([〈𝑥, 𝑦〉] ~R
<R [〈𝑧, 𝑤〉] ~R ∧
[〈𝑧, 𝑤〉]
~R <R [〈𝑣, 𝑢〉] ~R ) ↔
(𝑓
<R [〈𝑧, 𝑤〉] ~R ∧
[〈𝑧, 𝑤〉]
~R <R [〈𝑣, 𝑢〉] ~R
))) |
35 | | breq1 5056 |
. . . 4
⊢
([〈𝑥, 𝑦〉]
~R = 𝑓 → ([〈𝑥, 𝑦〉] ~R
<R [〈𝑣, 𝑢〉] ~R ↔
𝑓
<R [〈𝑣, 𝑢〉] ~R
)) |
36 | 34, 35 | imbi12d 348 |
. . 3
⊢
([〈𝑥, 𝑦〉]
~R = 𝑓 → ((([〈𝑥, 𝑦〉] ~R
<R [〈𝑧, 𝑤〉] ~R ∧
[〈𝑧, 𝑤〉]
~R <R [〈𝑣, 𝑢〉] ~R ) →
[〈𝑥, 𝑦〉]
~R <R [〈𝑣, 𝑢〉] ~R ) ↔
((𝑓
<R [〈𝑧, 𝑤〉] ~R ∧
[〈𝑧, 𝑤〉]
~R <R [〈𝑣, 𝑢〉] ~R ) →
𝑓
<R [〈𝑣, 𝑢〉] ~R
))) |
37 | | breq1 5056 |
. . . . 5
⊢
([〈𝑧, 𝑤〉]
~R = 𝑔 → ([〈𝑧, 𝑤〉] ~R
<R [〈𝑣, 𝑢〉] ~R ↔
𝑔
<R [〈𝑣, 𝑢〉] ~R
)) |
38 | 8, 37 | anbi12d 634 |
. . . 4
⊢
([〈𝑧, 𝑤〉]
~R = 𝑔 → ((𝑓 <R [〈𝑧, 𝑤〉] ~R ∧
[〈𝑧, 𝑤〉]
~R <R [〈𝑣, 𝑢〉] ~R ) ↔
(𝑓
<R 𝑔 ∧ 𝑔 <R [〈𝑣, 𝑢〉] ~R
))) |
39 | 38 | imbi1d 345 |
. . 3
⊢
([〈𝑧, 𝑤〉]
~R = 𝑔 → (((𝑓 <R [〈𝑧, 𝑤〉] ~R ∧
[〈𝑧, 𝑤〉]
~R <R [〈𝑣, 𝑢〉] ~R ) →
𝑓
<R [〈𝑣, 𝑢〉] ~R ) ↔
((𝑓
<R 𝑔 ∧ 𝑔 <R [〈𝑣, 𝑢〉] ~R ) →
𝑓
<R [〈𝑣, 𝑢〉] ~R
))) |
40 | | breq2 5057 |
. . . . 5
⊢
([〈𝑣, 𝑢〉]
~R = ℎ → (𝑔 <R [〈𝑣, 𝑢〉] ~R ↔
𝑔
<R ℎ)) |
41 | 40 | anbi2d 632 |
. . . 4
⊢
([〈𝑣, 𝑢〉]
~R = ℎ → ((𝑓 <R 𝑔 ∧ 𝑔 <R [〈𝑣, 𝑢〉] ~R ) ↔
(𝑓
<R 𝑔 ∧ 𝑔 <R ℎ))) |
42 | | breq2 5057 |
. . . 4
⊢
([〈𝑣, 𝑢〉]
~R = ℎ → (𝑓 <R [〈𝑣, 𝑢〉] ~R ↔
𝑓
<R ℎ)) |
43 | 41, 42 | imbi12d 348 |
. . 3
⊢
([〈𝑣, 𝑢〉]
~R = ℎ → (((𝑓 <R 𝑔 ∧ 𝑔 <R [〈𝑣, 𝑢〉] ~R ) →
𝑓
<R [〈𝑣, 𝑢〉] ~R ) ↔
((𝑓
<R 𝑔 ∧ 𝑔 <R ℎ) → 𝑓 <R ℎ))) |
44 | | ovex 7246 |
. . . . . . . . . 10
⊢ (𝑥 +P
𝑤) ∈
V |
45 | | ovex 7246 |
. . . . . . . . . 10
⊢ (𝑦 +P
𝑧) ∈
V |
46 | | ltapr 10659 |
. . . . . . . . . 10
⊢ (ℎ ∈ P →
(𝑓<P 𝑔 ↔ (ℎ +P 𝑓)<P
(ℎ
+P 𝑔))) |
47 | | vex 3412 |
. . . . . . . . . 10
⊢ 𝑢 ∈ V |
48 | | addcompr 10635 |
. . . . . . . . . 10
⊢ (𝑓 +P
𝑔) = (𝑔 +P 𝑓) |
49 | 44, 45, 46, 47, 48 | caovord2 7420 |
. . . . . . . . 9
⊢ (𝑢 ∈ P →
((𝑥
+P 𝑤)<P (𝑦 +P
𝑧) ↔ ((𝑥 +P
𝑤)
+P 𝑢)<P ((𝑦 +P
𝑧)
+P 𝑢))) |
50 | | addasspr 10636 |
. . . . . . . . . 10
⊢ ((𝑥 +P
𝑤)
+P 𝑢) = (𝑥 +P (𝑤 +P
𝑢)) |
51 | | addasspr 10636 |
. . . . . . . . . 10
⊢ ((𝑦 +P
𝑧)
+P 𝑢) = (𝑦 +P (𝑧 +P
𝑢)) |
52 | 50, 51 | breq12i 5062 |
. . . . . . . . 9
⊢ (((𝑥 +P
𝑤)
+P 𝑢)<P ((𝑦 +P
𝑧)
+P 𝑢) ↔ (𝑥 +P (𝑤 +P
𝑢))<P (𝑦 +P
(𝑧
+P 𝑢))) |
53 | 49, 52 | bitrdi 290 |
. . . . . . . 8
⊢ (𝑢 ∈ P →
((𝑥
+P 𝑤)<P (𝑦 +P
𝑧) ↔ (𝑥 +P
(𝑤
+P 𝑢))<P (𝑦 +P
(𝑧
+P 𝑢)))) |
54 | 14, 53 | syl5bb 286 |
. . . . . . 7
⊢ (𝑢 ∈ P →
([〈𝑥, 𝑦〉]
~R <R [〈𝑧, 𝑤〉] ~R ↔
(𝑥
+P (𝑤 +P 𝑢))<P
(𝑦
+P (𝑧 +P 𝑢)))) |
55 | | ltsrpr 10691 |
. . . . . . . 8
⊢
([〈𝑧, 𝑤〉]
~R <R [〈𝑣, 𝑢〉] ~R ↔
(𝑧
+P 𝑢)<P (𝑤 +P
𝑣)) |
56 | | ltapr 10659 |
. . . . . . . 8
⊢ (𝑦 ∈ P →
((𝑧
+P 𝑢)<P (𝑤 +P
𝑣) ↔ (𝑦 +P
(𝑧
+P 𝑢))<P (𝑦 +P
(𝑤
+P 𝑣)))) |
57 | 55, 56 | syl5bb 286 |
. . . . . . 7
⊢ (𝑦 ∈ P →
([〈𝑧, 𝑤〉]
~R <R [〈𝑣, 𝑢〉] ~R ↔
(𝑦
+P (𝑧 +P 𝑢))<P
(𝑦
+P (𝑤 +P 𝑣)))) |
58 | 54, 57 | bi2anan9r 640 |
. . . . . 6
⊢ ((𝑦 ∈ P ∧
𝑢 ∈ P)
→ (([〈𝑥, 𝑦〉]
~R <R [〈𝑧, 𝑤〉] ~R ∧
[〈𝑧, 𝑤〉]
~R <R [〈𝑣, 𝑢〉] ~R ) ↔
((𝑥
+P (𝑤 +P 𝑢))<P
(𝑦
+P (𝑧 +P 𝑢)) ∧ (𝑦 +P (𝑧 +P
𝑢))<P (𝑦 +P
(𝑤
+P 𝑣))))) |
59 | | ltrelpr 10612 |
. . . . . . . 8
⊢
<P ⊆ (P ×
P) |
60 | 17, 59 | sotri 5992 |
. . . . . . 7
⊢ (((𝑥 +P
(𝑤
+P 𝑢))<P (𝑦 +P
(𝑧
+P 𝑢)) ∧ (𝑦 +P (𝑧 +P
𝑢))<P (𝑦 +P
(𝑤
+P 𝑣))) → (𝑥 +P (𝑤 +P
𝑢))<P (𝑦 +P
(𝑤
+P 𝑣))) |
61 | | dmplp 10626 |
. . . . . . . . 9
⊢ dom
+P = (P ×
P) |
62 | | 0npr 10606 |
. . . . . . . . 9
⊢ ¬
∅ ∈ P |
63 | | ltapr 10659 |
. . . . . . . . 9
⊢ (𝑤 ∈ P →
((𝑥
+P 𝑢)<P (𝑦 +P
𝑣) ↔ (𝑤 +P
(𝑥
+P 𝑢))<P (𝑤 +P
(𝑦
+P 𝑣)))) |
64 | 61, 59, 62, 63 | ndmovordi 7399 |
. . . . . . . 8
⊢ ((𝑤 +P
(𝑥
+P 𝑢))<P (𝑤 +P
(𝑦
+P 𝑣)) → (𝑥 +P 𝑢)<P
(𝑦
+P 𝑣)) |
65 | | vex 3412 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
66 | | vex 3412 |
. . . . . . . . . 10
⊢ 𝑤 ∈ V |
67 | | addasspr 10636 |
. . . . . . . . . 10
⊢ ((𝑓 +P
𝑔)
+P ℎ) = (𝑓 +P (𝑔 +P
ℎ)) |
68 | 65, 66, 47, 48, 67 | caov12 7436 |
. . . . . . . . 9
⊢ (𝑥 +P
(𝑤
+P 𝑢)) = (𝑤 +P (𝑥 +P
𝑢)) |
69 | | vex 3412 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
70 | | vex 3412 |
. . . . . . . . . 10
⊢ 𝑣 ∈ V |
71 | 69, 66, 70, 48, 67 | caov12 7436 |
. . . . . . . . 9
⊢ (𝑦 +P
(𝑤
+P 𝑣)) = (𝑤 +P (𝑦 +P
𝑣)) |
72 | 68, 71 | breq12i 5062 |
. . . . . . . 8
⊢ ((𝑥 +P
(𝑤
+P 𝑢))<P (𝑦 +P
(𝑤
+P 𝑣)) ↔ (𝑤 +P (𝑥 +P
𝑢))<P (𝑤 +P
(𝑦
+P 𝑣))) |
73 | | ltsrpr 10691 |
. . . . . . . 8
⊢
([〈𝑥, 𝑦〉]
~R <R [〈𝑣, 𝑢〉] ~R ↔
(𝑥
+P 𝑢)<P (𝑦 +P
𝑣)) |
74 | 64, 72, 73 | 3imtr4i 295 |
. . . . . . 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 | syl6bi 256 |
. . . . 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 1133 |
. . 3
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P) ∧ (𝑣 ∈ P ∧ 𝑢 ∈ P)) →
(([〈𝑥, 𝑦〉]
~R <R [〈𝑧, 𝑤〉] ~R ∧
[〈𝑧, 𝑤〉]
~R <R [〈𝑣, 𝑢〉] ~R ) →
[〈𝑥, 𝑦〉]
~R <R [〈𝑣, 𝑢〉] ~R
)) |
79 | 1, 36, 39, 43, 78 | 3ecoptocl 8491 |
. 2
⊢ ((𝑓 ∈ R ∧
𝑔 ∈ R
∧ ℎ ∈
R) → ((𝑓
<R 𝑔 ∧ 𝑔 <R ℎ) → 𝑓 <R ℎ)) |
80 | 33, 79 | isso2i 5503 |
1
⊢
<R Or R |