Step | Hyp | Ref
| Expression |
1 | | enrer 10677 |
. . . . . 6
⊢
~R Er (P ×
P) |
2 | | erdm 8401 |
. . . . . 6
⊢ (
~R Er (P × P) →
dom ~R = (P ×
P)) |
3 | 1, 2 | ax-mp 5 |
. . . . 5
⊢ dom
~R = (P ×
P) |
4 | | simprll 779 |
. . . . . 6
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
𝐴 = [〈𝑤, 𝑣〉] ~R
) |
5 | | simpll 767 |
. . . . . 6
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
𝐴 ∈ ((P
× P) / ~R
)) |
6 | 4, 5 | eqeltrrd 2839 |
. . . . 5
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
[〈𝑤, 𝑣〉]
~R ∈ ((P × P)
/ ~R )) |
7 | | ecelqsdm 8469 |
. . . . 5
⊢ ((dom
~R = (P × P) ∧
[〈𝑤, 𝑣〉]
~R ∈ ((P × P)
/ ~R )) → 〈𝑤, 𝑣〉 ∈ (P ×
P)) |
8 | 3, 6, 7 | sylancr 590 |
. . . 4
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
〈𝑤, 𝑣〉 ∈ (P ×
P)) |
9 | | opelxp 5587 |
. . . 4
⊢
(〈𝑤, 𝑣〉 ∈ (P
× P) ↔ (𝑤 ∈ P ∧ 𝑣 ∈
P)) |
10 | 8, 9 | sylib 221 |
. . 3
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
(𝑤 ∈ P
∧ 𝑣 ∈
P)) |
11 | | simprrl 781 |
. . . . . 6
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
𝐴 = [〈𝑠, 𝑓〉] ~R
) |
12 | 11, 5 | eqeltrrd 2839 |
. . . . 5
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
[〈𝑠, 𝑓〉]
~R ∈ ((P × P)
/ ~R )) |
13 | | ecelqsdm 8469 |
. . . . 5
⊢ ((dom
~R = (P × P) ∧
[〈𝑠, 𝑓〉]
~R ∈ ((P × P)
/ ~R )) → 〈𝑠, 𝑓〉 ∈ (P ×
P)) |
14 | 3, 12, 13 | sylancr 590 |
. . . 4
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
〈𝑠, 𝑓〉 ∈ (P ×
P)) |
15 | | opelxp 5587 |
. . . 4
⊢
(〈𝑠, 𝑓〉 ∈ (P
× P) ↔ (𝑠 ∈ P ∧ 𝑓 ∈
P)) |
16 | 14, 15 | sylib 221 |
. . 3
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
(𝑠 ∈ P
∧ 𝑓 ∈
P)) |
17 | 10, 16 | jca 515 |
. 2
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
((𝑤 ∈ P
∧ 𝑣 ∈
P) ∧ (𝑠
∈ P ∧ 𝑓 ∈ P))) |
18 | | simprlr 780 |
. . . . . 6
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
𝐵 = [〈𝑢, 𝑡〉] ~R
) |
19 | | simplr 769 |
. . . . . 6
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
𝐵 ∈ ((P
× P) / ~R
)) |
20 | 18, 19 | eqeltrrd 2839 |
. . . . 5
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
[〈𝑢, 𝑡〉]
~R ∈ ((P × P)
/ ~R )) |
21 | | ecelqsdm 8469 |
. . . . 5
⊢ ((dom
~R = (P × P) ∧
[〈𝑢, 𝑡〉]
~R ∈ ((P × P)
/ ~R )) → 〈𝑢, 𝑡〉 ∈ (P ×
P)) |
22 | 3, 20, 21 | sylancr 590 |
. . . 4
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
〈𝑢, 𝑡〉 ∈ (P ×
P)) |
23 | | opelxp 5587 |
. . . 4
⊢
(〈𝑢, 𝑡〉 ∈ (P
× P) ↔ (𝑢 ∈ P ∧ 𝑡 ∈
P)) |
24 | 22, 23 | sylib 221 |
. . 3
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
(𝑢 ∈ P
∧ 𝑡 ∈
P)) |
25 | | simprrr 782 |
. . . . . 6
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
𝐵 = [〈𝑔, ℎ〉] ~R
) |
26 | 25, 19 | eqeltrrd 2839 |
. . . . 5
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
[〈𝑔, ℎ〉]
~R ∈ ((P × P)
/ ~R )) |
27 | | ecelqsdm 8469 |
. . . . 5
⊢ ((dom
~R = (P × P) ∧
[〈𝑔, ℎ〉]
~R ∈ ((P × P)
/ ~R )) → 〈𝑔, ℎ〉 ∈ (P ×
P)) |
28 | 3, 26, 27 | sylancr 590 |
. . . 4
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
〈𝑔, ℎ〉 ∈ (P ×
P)) |
29 | | opelxp 5587 |
. . . 4
⊢
(〈𝑔, ℎ〉 ∈ (P
× P) ↔ (𝑔 ∈ P ∧ ℎ ∈
P)) |
30 | 28, 29 | sylib 221 |
. . 3
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
(𝑔 ∈ P
∧ ℎ ∈
P)) |
31 | 24, 30 | jca 515 |
. 2
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
((𝑢 ∈ P
∧ 𝑡 ∈
P) ∧ (𝑔
∈ P ∧ ℎ ∈ P))) |
32 | 4, 11 | eqtr3d 2779 |
. . . . 5
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
[〈𝑤, 𝑣〉]
~R = [〈𝑠, 𝑓〉] ~R
) |
33 | 1 | a1i 11 |
. . . . . 6
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
~R Er (P ×
P)) |
34 | 33, 8 | erth 8440 |
. . . . 5
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
(〈𝑤, 𝑣〉
~R 〈𝑠, 𝑓〉 ↔ [〈𝑤, 𝑣〉] ~R =
[〈𝑠, 𝑓〉]
~R )) |
35 | 32, 34 | mpbird 260 |
. . . 4
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
〈𝑤, 𝑣〉 ~R
〈𝑠, 𝑓〉) |
36 | | df-enr 10669 |
. . . . . 6
⊢
~R = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (P ×
P) ∧ 𝑦
∈ (P × P)) ∧ ∃𝑎∃𝑏∃𝑐∃𝑑((𝑥 = 〈𝑎, 𝑏〉 ∧ 𝑦 = 〈𝑐, 𝑑〉) ∧ (𝑎 +P 𝑑) = (𝑏 +P 𝑐)))} |
37 | 36 | ecopoveq 8500 |
. . . . 5
⊢ (((𝑤 ∈ P ∧
𝑣 ∈ P)
∧ (𝑠 ∈
P ∧ 𝑓
∈ P)) → (〈𝑤, 𝑣〉 ~R
〈𝑠, 𝑓〉 ↔ (𝑤 +P 𝑓) = (𝑣 +P 𝑠))) |
38 | 10, 16, 37 | syl2anc 587 |
. . . 4
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
(〈𝑤, 𝑣〉
~R 〈𝑠, 𝑓〉 ↔ (𝑤 +P 𝑓) = (𝑣 +P 𝑠))) |
39 | 35, 38 | mpbid 235 |
. . 3
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
(𝑤
+P 𝑓) = (𝑣 +P 𝑠)) |
40 | 18, 25 | eqtr3d 2779 |
. . . . 5
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
[〈𝑢, 𝑡〉]
~R = [〈𝑔, ℎ〉] ~R
) |
41 | 33, 22 | erth 8440 |
. . . . 5
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
(〈𝑢, 𝑡〉
~R 〈𝑔, ℎ〉 ↔ [〈𝑢, 𝑡〉] ~R =
[〈𝑔, ℎ〉]
~R )) |
42 | 40, 41 | mpbird 260 |
. . . 4
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
〈𝑢, 𝑡〉 ~R
〈𝑔, ℎ〉) |
43 | 36 | ecopoveq 8500 |
. . . . 5
⊢ (((𝑢 ∈ P ∧
𝑡 ∈ P)
∧ (𝑔 ∈
P ∧ ℎ
∈ P)) → (〈𝑢, 𝑡〉 ~R
〈𝑔, ℎ〉 ↔ (𝑢 +P ℎ) = (𝑡 +P 𝑔))) |
44 | 24, 30, 43 | syl2anc 587 |
. . . 4
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
(〈𝑢, 𝑡〉
~R 〈𝑔, ℎ〉 ↔ (𝑢 +P ℎ) = (𝑡 +P 𝑔))) |
45 | 42, 44 | mpbid 235 |
. . 3
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
(𝑢
+P ℎ) = (𝑡 +P 𝑔)) |
46 | 39, 45 | jca 515 |
. 2
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
((𝑤
+P 𝑓) = (𝑣 +P 𝑠) ∧ (𝑢 +P ℎ) = (𝑡 +P 𝑔))) |
47 | 17, 31, 46 | jca31 518 |
1
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
((((𝑤 ∈
P ∧ 𝑣
∈ P) ∧ (𝑠 ∈ P ∧ 𝑓 ∈ P)) ∧
((𝑢 ∈ P
∧ 𝑡 ∈
P) ∧ (𝑔
∈ P ∧ ℎ ∈ P))) ∧ ((𝑤 +P
𝑓) = (𝑣 +P 𝑠) ∧ (𝑢 +P ℎ) = (𝑡 +P 𝑔)))) |