Step | Hyp | Ref
| Expression |
1 | | df-nr 6655 |
. 2
⊢
R = ((P × P) /
~R ) |
2 | | breq1 3758 |
. . . 4
⊢
([〈x, y〉] ~R = f → ([〈x, y〉]
~R <R [〈z, w〉]
~R ↔ f
<R [〈z,
w〉] ~R
)) |
3 | 2 | anbi1d 438 |
. . 3
⊢
([〈x, y〉] ~R = f → (([〈x, y〉]
~R <R [〈z, w〉]
~R ∧ [〈z, w〉]
~R <R [〈v, u〉]
~R ) ↔ (f
<R [〈z,
w〉] ~R ∧ [〈z,
w〉] ~R
<R [〈v,
u〉] ~R
))) |
4 | | breq1 3758 |
. . 3
⊢
([〈x, y〉] ~R = f → ([〈x, y〉]
~R <R [〈v, u〉]
~R ↔ f
<R [〈v,
u〉] ~R
)) |
5 | 3, 4 | imbi12d 223 |
. 2
⊢
([〈x, y〉] ~R = f → ((([〈x, y〉]
~R <R [〈z, w〉]
~R ∧ [〈z, w〉]
~R <R [〈v, u〉]
~R ) → [〈x, y〉]
~R <R [〈v, u〉]
~R ) ↔ ((f
<R [〈z,
w〉] ~R ∧ [〈z,
w〉] ~R
<R [〈v,
u〉] ~R )
→ f <R
[〈v, u〉] ~R
))) |
6 | | breq2 3759 |
. . . 4
⊢
([〈z, w〉] ~R = g → (f
<R [〈z,
w〉] ~R ↔
f <R g)) |
7 | | breq1 3758 |
. . . 4
⊢
([〈z, w〉] ~R = g → ([〈z, w〉]
~R <R [〈v, u〉]
~R ↔ g
<R [〈v,
u〉] ~R
)) |
8 | 6, 7 | anbi12d 442 |
. . 3
⊢
([〈z, w〉] ~R = g → ((f
<R [〈z,
w〉] ~R ∧ [〈z,
w〉] ~R
<R [〈v,
u〉] ~R )
↔ (f <R
g ∧
g <R
[〈v, u〉] ~R
))) |
9 | 8 | imbi1d 220 |
. 2
⊢
([〈z, w〉] ~R = g → (((f
<R [〈z,
w〉] ~R ∧ [〈z,
w〉] ~R
<R [〈v,
u〉] ~R )
→ f <R
[〈v, u〉] ~R ) ↔
((f <R g ∧ g <R [〈v, u〉]
~R ) → f
<R [〈v,
u〉] ~R
))) |
10 | | breq2 3759 |
. . . 4
⊢
([〈v, u〉] ~R = ℎ → (g <R [〈v, u〉]
~R ↔ g
<R ℎ)) |
11 | 10 | anbi2d 437 |
. . 3
⊢
([〈v, u〉] ~R = ℎ → ((f <R g ∧ g <R [〈v, u〉]
~R ) ↔ (f
<R g ∧ g
<R ℎ))) |
12 | | breq2 3759 |
. . 3
⊢
([〈v, u〉] ~R = ℎ → (f <R [〈v, u〉]
~R ↔ f
<R ℎ)) |
13 | 11, 12 | imbi12d 223 |
. 2
⊢
([〈v, u〉] ~R = ℎ → (((f <R g ∧ g <R [〈v, u〉]
~R ) → f
<R [〈v,
u〉] ~R )
↔ ((f <R
g ∧
g <R ℎ) → f <R ℎ))) |
14 | | ltsrprg 6675 |
. . . . . 6
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) → ([〈x, y〉]
~R <R [〈z, w〉]
~R ↔ (x
+P w)<P (y +P z))) |
15 | 14 | 3adant3 923 |
. . . . 5
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → ([〈x, y〉]
~R <R [〈z, w〉]
~R ↔ (x
+P w)<P (y +P z))) |
16 | | ltaprg 6592 |
. . . . . . . 8
⊢ ((𝑟 ∈ P ∧ 𝑠
∈ P ∧ 𝑡
∈ P) → (𝑟<P 𝑠 ↔ (𝑡 +P 𝑟)<P (𝑡 +P 𝑠))) |
17 | 16 | adantl 262 |
. . . . . . 7
⊢
((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) ∧ (𝑟 ∈
P ∧ 𝑠 ∈
P ∧ 𝑡 ∈
P)) → (𝑟<P 𝑠 ↔ (𝑡 +P 𝑟)<P (𝑡 +P 𝑠))) |
18 | | simp1l 927 |
. . . . . . . 8
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → x ∈
P) |
19 | | simp2r 930 |
. . . . . . . 8
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → w ∈
P) |
20 | | addclpr 6520 |
. . . . . . . 8
⊢
((x ∈ P ∧ w ∈ P) → (x +P w) ∈
P) |
21 | 18, 19, 20 | syl2anc 391 |
. . . . . . 7
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (x +P w) ∈
P) |
22 | | simp1r 928 |
. . . . . . . 8
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → y ∈
P) |
23 | | simp2l 929 |
. . . . . . . 8
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → z ∈
P) |
24 | | addclpr 6520 |
. . . . . . . 8
⊢
((y ∈ P ∧ z ∈ P) → (y +P z) ∈
P) |
25 | 22, 23, 24 | syl2anc 391 |
. . . . . . 7
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (y +P z) ∈
P) |
26 | | simp3r 932 |
. . . . . . 7
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → u ∈
P) |
27 | | addcomprg 6554 |
. . . . . . . 8
⊢ ((𝑟 ∈ P ∧ 𝑠
∈ P) → (𝑟 +P 𝑠) = (𝑠 +P 𝑟)) |
28 | 27 | adantl 262 |
. . . . . . 7
⊢
((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) ∧ (𝑟 ∈
P ∧ 𝑠 ∈
P)) → (𝑟
+P 𝑠)
= (𝑠
+P 𝑟)) |
29 | 17, 21, 25, 26, 28 | caovord2d 5612 |
. . . . . 6
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → ((x +P w)<P (y +P z) ↔ ((x
+P w)
+P u)<P ((y +P z) +P u))) |
30 | | addassprg 6555 |
. . . . . . . 8
⊢
((x ∈ P ∧ w ∈ P ∧ u ∈ P) → ((x +P w) +P u) = (x
+P (w
+P u))) |
31 | 18, 19, 26, 30 | syl3anc 1134 |
. . . . . . 7
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → ((x +P w) +P u) = (x
+P (w
+P u))) |
32 | | addassprg 6555 |
. . . . . . . 8
⊢
((y ∈ P ∧ z ∈ P ∧ u ∈ P) → ((y +P z) +P u) = (y
+P (z
+P u))) |
33 | 22, 23, 26, 32 | syl3anc 1134 |
. . . . . . 7
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → ((y +P z) +P u) = (y
+P (z
+P u))) |
34 | 31, 33 | breq12d 3768 |
. . . . . 6
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (((x +P w) +P u)<P ((y +P z) +P u) ↔ (x
+P (w
+P u))<P (y +P (z +P u)))) |
35 | 29, 34 | bitrd 177 |
. . . . 5
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → ((x +P w)<P (y +P z) ↔ (x
+P (w
+P u))<P (y +P (z +P u)))) |
36 | 15, 35 | bitrd 177 |
. . . 4
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → ([〈x, y〉]
~R <R [〈z, w〉]
~R ↔ (x
+P (w
+P u))<P (y +P (z +P u)))) |
37 | | ltsrprg 6675 |
. . . . . 6
⊢
(((z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → ([〈z, w〉]
~R <R [〈v, u〉]
~R ↔ (z
+P u)<P (w +P v))) |
38 | 37 | 3adant1 921 |
. . . . 5
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → ([〈z, w〉]
~R <R [〈v, u〉]
~R ↔ (z
+P u)<P (w +P v))) |
39 | | addclpr 6520 |
. . . . . . 7
⊢
((z ∈ P ∧ u ∈ P) → (z +P u) ∈
P) |
40 | 23, 26, 39 | syl2anc 391 |
. . . . . 6
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (z +P u) ∈
P) |
41 | | simp3l 931 |
. . . . . . 7
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → v ∈
P) |
42 | | addclpr 6520 |
. . . . . . 7
⊢
((w ∈ P ∧ v ∈ P) → (w +P v) ∈
P) |
43 | 19, 41, 42 | syl2anc 391 |
. . . . . 6
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (w +P v) ∈
P) |
44 | | ltaprg 6592 |
. . . . . 6
⊢
(((z +P
u) ∈
P ∧ (w +P v) ∈
P ∧ y ∈
P) → ((z
+P u)<P (w +P v) ↔ (y
+P (z
+P u))<P (y +P (w +P v)))) |
45 | 40, 43, 22, 44 | syl3anc 1134 |
. . . . 5
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → ((z +P u)<P (w +P v) ↔ (y
+P (z
+P u))<P (y +P (w +P v)))) |
46 | 38, 45 | bitrd 177 |
. . . 4
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → ([〈z, w〉]
~R <R [〈v, u〉]
~R ↔ (y
+P (z
+P u))<P (y +P (w +P v)))) |
47 | 36, 46 | anbi12d 442 |
. . 3
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (([〈x, y〉]
~R <R [〈z, w〉]
~R ∧ [〈z, w〉]
~R <R [〈v, u〉]
~R ) ↔ ((x
+P (w
+P u))<P (y +P (z +P u)) ∧ (y +P (z +P u))<P (y +P (w +P v))))) |
48 | | ltsopr 6570 |
. . . . 5
⊢
<P Or P |
49 | | ltrelpr 6488 |
. . . . 5
⊢
<P ⊆ (P ×
P) |
50 | 48, 49 | sotri 4663 |
. . . 4
⊢
(((x +P
(w +P u))<P (y +P (z +P u)) ∧ (y +P (z +P u))<P (y +P (w +P v))) → (x
+P (w
+P u))<P (y +P (w +P v))) |
51 | | addclpr 6520 |
. . . . . . . 8
⊢
((x ∈ P ∧ u ∈ P) → (x +P u) ∈
P) |
52 | 18, 26, 51 | syl2anc 391 |
. . . . . . 7
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (x +P u) ∈
P) |
53 | | addclpr 6520 |
. . . . . . . 8
⊢
((y ∈ P ∧ v ∈ P) → (y +P v) ∈
P) |
54 | 22, 41, 53 | syl2anc 391 |
. . . . . . 7
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (y +P v) ∈
P) |
55 | | ltaprg 6592 |
. . . . . . 7
⊢
(((x +P
u) ∈
P ∧ (y +P v) ∈
P ∧ w ∈
P) → ((x
+P u)<P (y +P v) ↔ (w
+P (x
+P u))<P (w +P (y +P v)))) |
56 | 52, 54, 19, 55 | syl3anc 1134 |
. . . . . 6
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → ((x +P u)<P (y +P v) ↔ (w
+P (x
+P u))<P (w +P (y +P v)))) |
57 | 56 | biimprd 147 |
. . . . 5
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → ((w +P (x +P u))<P (w +P (y +P v)) → (x
+P u)<P (y +P v))) |
58 | | addassprg 6555 |
. . . . . . . 8
⊢ ((𝑟 ∈ P ∧ 𝑠
∈ P ∧ 𝑡
∈ P) → ((𝑟 +P 𝑠) +P 𝑡) = (𝑟 +P (𝑠 +P 𝑡))) |
59 | 58 | adantl 262 |
. . . . . . 7
⊢
((((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) ∧ (𝑟 ∈
P ∧ 𝑠 ∈
P ∧ 𝑡 ∈
P)) → ((𝑟
+P 𝑠)
+P 𝑡)
= (𝑟
+P (𝑠
+P 𝑡))) |
60 | 18, 19, 26, 28, 59 | caov12d 5624 |
. . . . . 6
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (x +P (w +P u)) = (w
+P (x
+P u))) |
61 | 22, 19, 41, 28, 59 | caov12d 5624 |
. . . . . 6
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (y +P (w +P v)) = (w
+P (y
+P v))) |
62 | 60, 61 | breq12d 3768 |
. . . . 5
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → ((x +P (w +P u))<P (y +P (w +P v)) ↔ (w
+P (x
+P u))<P (w +P (y +P v)))) |
63 | | ltsrprg 6675 |
. . . . . 6
⊢
(((x ∈ P ∧ y ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → ([〈x, y〉]
~R <R [〈v, u〉]
~R ↔ (x
+P u)<P (y +P v))) |
64 | 63 | 3adant2 922 |
. . . . 5
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → ([〈x, y〉]
~R <R [〈v, u〉]
~R ↔ (x
+P u)<P (y +P v))) |
65 | 57, 62, 64 | 3imtr4d 192 |
. . . 4
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → ((x +P (w +P u))<P (y +P (w +P v)) → [〈x, y〉]
~R <R [〈v, u〉]
~R )) |
66 | 50, 65 | syl5 28 |
. . 3
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (((x +P (w +P u))<P (y +P (z +P u)) ∧ (y +P (z +P u))<P (y +P (w +P v))) → [〈x, y〉]
~R <R [〈v, u〉]
~R )) |
67 | 47, 66 | sylbid 139 |
. 2
⊢
(((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (([〈x, y〉]
~R <R [〈z, w〉]
~R ∧ [〈z, w〉]
~R <R [〈v, u〉]
~R ) → [〈x, y〉]
~R <R [〈v, u〉]
~R )) |
68 | 1, 5, 9, 13, 67 | 3ecoptocl 6131 |
1
⊢
((f ∈ R ∧ g ∈ R ∧ ℎ
∈ R) → ((f <R g ∧ g <R ℎ) → f
<R ℎ)) |