Step | Hyp | Ref
| Expression |
1 | | df-nr 7650 |
. . 3
⊢
R = ((P × P) /
~R ) |
2 | | breq1 3970 |
. . . . . 6
⊢
([〈𝑥, 𝑦〉]
~R = 𝐴 → ([〈𝑥, 𝑦〉] ~R
<R [〈𝑧, 𝑤〉] ~R ↔
𝐴
<R [〈𝑧, 𝑤〉] ~R
)) |
3 | | breq2 3971 |
. . . . . 6
⊢
([〈𝑥, 𝑦〉]
~R = 𝐴 → ([〈𝑧, 𝑤〉] ~R
<R [〈𝑥, 𝑦〉] ~R ↔
[〈𝑧, 𝑤〉]
~R <R 𝐴)) |
4 | 2, 3 | orbi12d 783 |
. . . . 5
⊢
([〈𝑥, 𝑦〉]
~R = 𝐴 → (([〈𝑥, 𝑦〉] ~R
<R [〈𝑧, 𝑤〉] ~R ∨
[〈𝑧, 𝑤〉]
~R <R [〈𝑥, 𝑦〉] ~R ) ↔
(𝐴
<R [〈𝑧, 𝑤〉] ~R ∨
[〈𝑧, 𝑤〉]
~R <R 𝐴))) |
5 | 4 | notbid 657 |
. . . 4
⊢
([〈𝑥, 𝑦〉]
~R = 𝐴 → (¬ ([〈𝑥, 𝑦〉] ~R
<R [〈𝑧, 𝑤〉] ~R ∨
[〈𝑧, 𝑤〉]
~R <R [〈𝑥, 𝑦〉] ~R ) ↔
¬ (𝐴
<R [〈𝑧, 𝑤〉] ~R ∨
[〈𝑧, 𝑤〉]
~R <R 𝐴))) |
6 | | eqeq1 2164 |
. . . 4
⊢
([〈𝑥, 𝑦〉]
~R = 𝐴 → ([〈𝑥, 𝑦〉] ~R =
[〈𝑧, 𝑤〉]
~R ↔ 𝐴 = [〈𝑧, 𝑤〉] ~R
)) |
7 | 5, 6 | imbi12d 233 |
. . 3
⊢
([〈𝑥, 𝑦〉]
~R = 𝐴 → ((¬ ([〈𝑥, 𝑦〉] ~R
<R [〈𝑧, 𝑤〉] ~R ∨
[〈𝑧, 𝑤〉]
~R <R [〈𝑥, 𝑦〉] ~R ) →
[〈𝑥, 𝑦〉]
~R = [〈𝑧, 𝑤〉] ~R ) ↔
(¬ (𝐴
<R [〈𝑧, 𝑤〉] ~R ∨
[〈𝑧, 𝑤〉]
~R <R 𝐴) → 𝐴 = [〈𝑧, 𝑤〉] ~R
))) |
8 | | breq2 3971 |
. . . . . 6
⊢
([〈𝑧, 𝑤〉]
~R = 𝐵 → (𝐴 <R [〈𝑧, 𝑤〉] ~R ↔
𝐴
<R 𝐵)) |
9 | | breq1 3970 |
. . . . . 6
⊢
([〈𝑧, 𝑤〉]
~R = 𝐵 → ([〈𝑧, 𝑤〉] ~R
<R 𝐴 ↔ 𝐵 <R 𝐴)) |
10 | 8, 9 | orbi12d 783 |
. . . . 5
⊢
([〈𝑧, 𝑤〉]
~R = 𝐵 → ((𝐴 <R [〈𝑧, 𝑤〉] ~R ∨
[〈𝑧, 𝑤〉]
~R <R 𝐴) ↔ (𝐴 <R 𝐵 ∨ 𝐵 <R 𝐴))) |
11 | 10 | notbid 657 |
. . . 4
⊢
([〈𝑧, 𝑤〉]
~R = 𝐵 → (¬ (𝐴 <R [〈𝑧, 𝑤〉] ~R ∨
[〈𝑧, 𝑤〉]
~R <R 𝐴) ↔ ¬ (𝐴 <R 𝐵 ∨ 𝐵 <R 𝐴))) |
12 | | eqeq2 2167 |
. . . 4
⊢
([〈𝑧, 𝑤〉]
~R = 𝐵 → (𝐴 = [〈𝑧, 𝑤〉] ~R ↔
𝐴 = 𝐵)) |
13 | 11, 12 | imbi12d 233 |
. . 3
⊢
([〈𝑧, 𝑤〉]
~R = 𝐵 → ((¬ (𝐴 <R [〈𝑧, 𝑤〉] ~R ∨
[〈𝑧, 𝑤〉]
~R <R 𝐴) → 𝐴 = [〈𝑧, 𝑤〉] ~R ) ↔
(¬ (𝐴
<R 𝐵 ∨ 𝐵 <R 𝐴) → 𝐴 = 𝐵))) |
14 | | addcomprg 7501 |
. . . . . . . . 9
⊢ ((𝑦 ∈ P ∧
𝑧 ∈ P)
→ (𝑦
+P 𝑧) = (𝑧 +P 𝑦)) |
15 | 14 | ad2ant2lr 502 |
. . . . . . . 8
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → (𝑦 +P 𝑧) = (𝑧 +P 𝑦)) |
16 | | addcomprg 7501 |
. . . . . . . . 9
⊢ ((𝑥 ∈ P ∧
𝑤 ∈ P)
→ (𝑥
+P 𝑤) = (𝑤 +P 𝑥)) |
17 | 16 | ad2ant2rl 503 |
. . . . . . . 8
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → (𝑥 +P 𝑤) = (𝑤 +P 𝑥)) |
18 | 15, 17 | breq12d 3980 |
. . . . . . 7
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → ((𝑦 +P 𝑧)<P
(𝑥
+P 𝑤) ↔ (𝑧 +P 𝑦)<P
(𝑤
+P 𝑥))) |
19 | 18 | orbi2d 780 |
. . . . . 6
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → (((𝑥 +P 𝑤)<P
(𝑦
+P 𝑧) ∨ (𝑦 +P 𝑧)<P
(𝑥
+P 𝑤)) ↔ ((𝑥 +P 𝑤)<P
(𝑦
+P 𝑧) ∨ (𝑧 +P 𝑦)<P
(𝑤
+P 𝑥)))) |
20 | 19 | notbid 657 |
. . . . 5
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → (¬ ((𝑥 +P 𝑤)<P
(𝑦
+P 𝑧) ∨ (𝑦 +P 𝑧)<P
(𝑥
+P 𝑤)) ↔ ¬ ((𝑥 +P 𝑤)<P
(𝑦
+P 𝑧) ∨ (𝑧 +P 𝑦)<P
(𝑤
+P 𝑥)))) |
21 | | addclpr 7460 |
. . . . . . 7
⊢ ((𝑥 ∈ P ∧
𝑤 ∈ P)
→ (𝑥
+P 𝑤) ∈ P) |
22 | 21 | ad2ant2rl 503 |
. . . . . 6
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → (𝑥 +P 𝑤) ∈
P) |
23 | | addclpr 7460 |
. . . . . . 7
⊢ ((𝑦 ∈ P ∧
𝑧 ∈ P)
→ (𝑦
+P 𝑧) ∈ P) |
24 | 23 | ad2ant2lr 502 |
. . . . . 6
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → (𝑦 +P 𝑧) ∈
P) |
25 | | aptipr 7564 |
. . . . . . 7
⊢ (((𝑥 +P
𝑤) ∈ P
∧ (𝑦
+P 𝑧) ∈ P ∧ ¬ ((𝑥 +P
𝑤)<P (𝑦 +P
𝑧) ∨ (𝑦 +P 𝑧)<P
(𝑥
+P 𝑤))) → (𝑥 +P 𝑤) = (𝑦 +P 𝑧)) |
26 | 25 | 3expia 1187 |
. . . . . 6
⊢ (((𝑥 +P
𝑤) ∈ P
∧ (𝑦
+P 𝑧) ∈ P) → (¬
((𝑥
+P 𝑤)<P (𝑦 +P
𝑧) ∨ (𝑦 +P 𝑧)<P
(𝑥
+P 𝑤)) → (𝑥 +P 𝑤) = (𝑦 +P 𝑧))) |
27 | 22, 24, 26 | syl2anc 409 |
. . . . 5
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → (¬ ((𝑥 +P 𝑤)<P
(𝑦
+P 𝑧) ∨ (𝑦 +P 𝑧)<P
(𝑥
+P 𝑤)) → (𝑥 +P 𝑤) = (𝑦 +P 𝑧))) |
28 | 20, 27 | sylbird 169 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → (¬ ((𝑥 +P 𝑤)<P
(𝑦
+P 𝑧) ∨ (𝑧 +P 𝑦)<P
(𝑤
+P 𝑥)) → (𝑥 +P 𝑤) = (𝑦 +P 𝑧))) |
29 | | ltsrprg 7670 |
. . . . . 6
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → ([〈𝑥, 𝑦〉] ~R
<R [〈𝑧, 𝑤〉] ~R ↔
(𝑥
+P 𝑤)<P (𝑦 +P
𝑧))) |
30 | | ltsrprg 7670 |
. . . . . . 7
⊢ (((𝑧 ∈ P ∧
𝑤 ∈ P)
∧ (𝑥 ∈
P ∧ 𝑦
∈ P)) → ([〈𝑧, 𝑤〉] ~R
<R [〈𝑥, 𝑦〉] ~R ↔
(𝑧
+P 𝑦)<P (𝑤 +P
𝑥))) |
31 | 30 | ancoms 266 |
. . . . . 6
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → ([〈𝑧, 𝑤〉] ~R
<R [〈𝑥, 𝑦〉] ~R ↔
(𝑧
+P 𝑦)<P (𝑤 +P
𝑥))) |
32 | 29, 31 | orbi12d 783 |
. . . . 5
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → (([〈𝑥, 𝑦〉] ~R
<R [〈𝑧, 𝑤〉] ~R ∨
[〈𝑧, 𝑤〉]
~R <R [〈𝑥, 𝑦〉] ~R ) ↔
((𝑥
+P 𝑤)<P (𝑦 +P
𝑧) ∨ (𝑧 +P 𝑦)<P
(𝑤
+P 𝑥)))) |
33 | 32 | notbid 657 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → (¬ ([〈𝑥, 𝑦〉] ~R
<R [〈𝑧, 𝑤〉] ~R ∨
[〈𝑧, 𝑤〉]
~R <R [〈𝑥, 𝑦〉] ~R ) ↔
¬ ((𝑥
+P 𝑤)<P (𝑦 +P
𝑧) ∨ (𝑧 +P 𝑦)<P
(𝑤
+P 𝑥)))) |
34 | | enreceq 7659 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → ([〈𝑥, 𝑦〉] ~R =
[〈𝑧, 𝑤〉]
~R ↔ (𝑥 +P 𝑤) = (𝑦 +P 𝑧))) |
35 | 28, 33, 34 | 3imtr4d 202 |
. . 3
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → (¬ ([〈𝑥, 𝑦〉] ~R
<R [〈𝑧, 𝑤〉] ~R ∨
[〈𝑧, 𝑤〉]
~R <R [〈𝑥, 𝑦〉] ~R ) →
[〈𝑥, 𝑦〉]
~R = [〈𝑧, 𝑤〉] ~R
)) |
36 | 1, 7, 13, 35 | 2ecoptocl 6571 |
. 2
⊢ ((𝐴 ∈ R ∧
𝐵 ∈ R)
→ (¬ (𝐴
<R 𝐵 ∨ 𝐵 <R 𝐴) → 𝐴 = 𝐵)) |
37 | 36 | 3impia 1182 |
1
⊢ ((𝐴 ∈ R ∧
𝐵 ∈ R
∧ ¬ (𝐴
<R 𝐵 ∨ 𝐵 <R 𝐴)) → 𝐴 = 𝐵) |