Step | Hyp | Ref
| Expression |
1 | | ecopopr.1 |
. . . . . . 7
⊢ ∼ =
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} |
2 | | opabssxp 5679 |
. . . . . . 7
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} ⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆)) |
3 | 1, 2 | eqsstri 3960 |
. . . . . 6
⊢ ∼
⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆)) |
4 | 3 | brel 5653 |
. . . . 5
⊢ (𝐴 ∼ 𝐵 → (𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆))) |
5 | 4 | simpld 495 |
. . . 4
⊢ (𝐴 ∼ 𝐵 → 𝐴 ∈ (𝑆 × 𝑆)) |
6 | 3 | brel 5653 |
. . . 4
⊢ (𝐵 ∼ 𝐶 → (𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆))) |
7 | 5, 6 | anim12i 613 |
. . 3
⊢ ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶) → (𝐴 ∈ (𝑆 × 𝑆) ∧ (𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)))) |
8 | | 3anass 1094 |
. . 3
⊢ ((𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)) ↔ (𝐴 ∈ (𝑆 × 𝑆) ∧ (𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)))) |
9 | 7, 8 | sylibr 233 |
. 2
⊢ ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶) → (𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆))) |
10 | | eqid 2740 |
. . 3
⊢ (𝑆 × 𝑆) = (𝑆 × 𝑆) |
11 | | breq1 5082 |
. . . . 5
⊢
(〈𝑓, 𝑔〉 = 𝐴 → (〈𝑓, 𝑔〉 ∼ 〈ℎ, 𝑡〉 ↔ 𝐴 ∼ 〈ℎ, 𝑡〉)) |
12 | 11 | anbi1d 630 |
. . . 4
⊢
(〈𝑓, 𝑔〉 = 𝐴 → ((〈𝑓, 𝑔〉 ∼ 〈ℎ, 𝑡〉 ∧ 〈ℎ, 𝑡〉 ∼ 〈𝑠, 𝑟〉) ↔ (𝐴 ∼ 〈ℎ, 𝑡〉 ∧ 〈ℎ, 𝑡〉 ∼ 〈𝑠, 𝑟〉))) |
13 | | breq1 5082 |
. . . 4
⊢
(〈𝑓, 𝑔〉 = 𝐴 → (〈𝑓, 𝑔〉 ∼ 〈𝑠, 𝑟〉 ↔ 𝐴 ∼ 〈𝑠, 𝑟〉)) |
14 | 12, 13 | imbi12d 345 |
. . 3
⊢
(〈𝑓, 𝑔〉 = 𝐴 → (((〈𝑓, 𝑔〉 ∼ 〈ℎ, 𝑡〉 ∧ 〈ℎ, 𝑡〉 ∼ 〈𝑠, 𝑟〉) → 〈𝑓, 𝑔〉 ∼ 〈𝑠, 𝑟〉) ↔ ((𝐴 ∼ 〈ℎ, 𝑡〉 ∧ 〈ℎ, 𝑡〉 ∼ 〈𝑠, 𝑟〉) → 𝐴 ∼ 〈𝑠, 𝑟〉))) |
15 | | breq2 5083 |
. . . . 5
⊢
(〈ℎ, 𝑡〉 = 𝐵 → (𝐴 ∼ 〈ℎ, 𝑡〉 ↔ 𝐴 ∼ 𝐵)) |
16 | | breq1 5082 |
. . . . 5
⊢
(〈ℎ, 𝑡〉 = 𝐵 → (〈ℎ, 𝑡〉 ∼ 〈𝑠, 𝑟〉 ↔ 𝐵 ∼ 〈𝑠, 𝑟〉)) |
17 | 15, 16 | anbi12d 631 |
. . . 4
⊢
(〈ℎ, 𝑡〉 = 𝐵 → ((𝐴 ∼ 〈ℎ, 𝑡〉 ∧ 〈ℎ, 𝑡〉 ∼ 〈𝑠, 𝑟〉) ↔ (𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 〈𝑠, 𝑟〉))) |
18 | 17 | imbi1d 342 |
. . 3
⊢
(〈ℎ, 𝑡〉 = 𝐵 → (((𝐴 ∼ 〈ℎ, 𝑡〉 ∧ 〈ℎ, 𝑡〉 ∼ 〈𝑠, 𝑟〉) → 𝐴 ∼ 〈𝑠, 𝑟〉) ↔ ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 〈𝑠, 𝑟〉) → 𝐴 ∼ 〈𝑠, 𝑟〉))) |
19 | | breq2 5083 |
. . . . 5
⊢
(〈𝑠, 𝑟〉 = 𝐶 → (𝐵 ∼ 〈𝑠, 𝑟〉 ↔ 𝐵 ∼ 𝐶)) |
20 | 19 | anbi2d 629 |
. . . 4
⊢
(〈𝑠, 𝑟〉 = 𝐶 → ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 〈𝑠, 𝑟〉) ↔ (𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶))) |
21 | | breq2 5083 |
. . . 4
⊢
(〈𝑠, 𝑟〉 = 𝐶 → (𝐴 ∼ 〈𝑠, 𝑟〉 ↔ 𝐴 ∼ 𝐶)) |
22 | 20, 21 | imbi12d 345 |
. . 3
⊢
(〈𝑠, 𝑟〉 = 𝐶 → (((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 〈𝑠, 𝑟〉) → 𝐴 ∼ 〈𝑠, 𝑟〉) ↔ ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶) → 𝐴 ∼ 𝐶))) |
23 | 1 | ecopoveq 8599 |
. . . . . . . 8
⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) → (〈𝑓, 𝑔〉 ∼ 〈ℎ, 𝑡〉 ↔ (𝑓 + 𝑡) = (𝑔 + ℎ))) |
24 | 23 | 3adant3 1131 |
. . . . . . 7
⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (〈𝑓, 𝑔〉 ∼ 〈ℎ, 𝑡〉 ↔ (𝑓 + 𝑡) = (𝑔 + ℎ))) |
25 | 1 | ecopoveq 8599 |
. . . . . . . 8
⊢ (((ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (〈ℎ, 𝑡〉 ∼ 〈𝑠, 𝑟〉 ↔ (ℎ + 𝑟) = (𝑡 + 𝑠))) |
26 | 25 | 3adant1 1129 |
. . . . . . 7
⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (〈ℎ, 𝑡〉 ∼ 〈𝑠, 𝑟〉 ↔ (ℎ + 𝑟) = (𝑡 + 𝑠))) |
27 | 24, 26 | anbi12d 631 |
. . . . . 6
⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((〈𝑓, 𝑔〉 ∼ 〈ℎ, 𝑡〉 ∧ 〈ℎ, 𝑡〉 ∼ 〈𝑠, 𝑟〉) ↔ ((𝑓 + 𝑡) = (𝑔 + ℎ) ∧ (ℎ + 𝑟) = (𝑡 + 𝑠)))) |
28 | | oveq12 7281 |
. . . . . . 7
⊢ (((𝑓 + 𝑡) = (𝑔 + ℎ) ∧ (ℎ + 𝑟) = (𝑡 + 𝑠)) → ((𝑓 + 𝑡) + (ℎ + 𝑟)) = ((𝑔 + ℎ) + (𝑡 + 𝑠))) |
29 | | vex 3435 |
. . . . . . . 8
⊢ ℎ ∈ V |
30 | | vex 3435 |
. . . . . . . 8
⊢ 𝑡 ∈ V |
31 | | vex 3435 |
. . . . . . . 8
⊢ 𝑓 ∈ V |
32 | | ecopopr.com |
. . . . . . . 8
⊢ (𝑥 + 𝑦) = (𝑦 + 𝑥) |
33 | | ecopopr.ass |
. . . . . . . 8
⊢ ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) |
34 | | vex 3435 |
. . . . . . . 8
⊢ 𝑟 ∈ V |
35 | 29, 30, 31, 32, 33, 34 | caov411 7499 |
. . . . . . 7
⊢ ((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((𝑓 + 𝑡) + (ℎ + 𝑟)) |
36 | | vex 3435 |
. . . . . . . . 9
⊢ 𝑔 ∈ V |
37 | | vex 3435 |
. . . . . . . . 9
⊢ 𝑠 ∈ V |
38 | 36, 30, 29, 32, 33, 37 | caov411 7499 |
. . . . . . . 8
⊢ ((𝑔 + 𝑡) + (ℎ + 𝑠)) = ((ℎ + 𝑡) + (𝑔 + 𝑠)) |
39 | 36, 30, 29, 32, 33, 37 | caov4 7498 |
. . . . . . . 8
⊢ ((𝑔 + 𝑡) + (ℎ + 𝑠)) = ((𝑔 + ℎ) + (𝑡 + 𝑠)) |
40 | 38, 39 | eqtr3i 2770 |
. . . . . . 7
⊢ ((ℎ + 𝑡) + (𝑔 + 𝑠)) = ((𝑔 + ℎ) + (𝑡 + 𝑠)) |
41 | 28, 35, 40 | 3eqtr4g 2805 |
. . . . . 6
⊢ (((𝑓 + 𝑡) = (𝑔 + ℎ) ∧ (ℎ + 𝑟) = (𝑡 + 𝑠)) → ((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((ℎ + 𝑡) + (𝑔 + 𝑠))) |
42 | 27, 41 | syl6bi 252 |
. . . . 5
⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((〈𝑓, 𝑔〉 ∼ 〈ℎ, 𝑡〉 ∧ 〈ℎ, 𝑡〉 ∼ 〈𝑠, 𝑟〉) → ((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((ℎ + 𝑡) + (𝑔 + 𝑠)))) |
43 | | ecopopr.cl |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆) |
44 | 43 | caovcl 7461 |
. . . . . . . . . 10
⊢ ((ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) → (ℎ + 𝑡) ∈ 𝑆) |
45 | 43 | caovcl 7461 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆) → (𝑓 + 𝑟) ∈ 𝑆) |
46 | | ovex 7305 |
. . . . . . . . . . 11
⊢ (𝑔 + 𝑠) ∈ V |
47 | | ecopopr.can |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥 + 𝑦) = (𝑥 + 𝑧) → 𝑦 = 𝑧)) |
48 | 46, 47 | caovcan 7471 |
. . . . . . . . . 10
⊢ (((ℎ + 𝑡) ∈ 𝑆 ∧ (𝑓 + 𝑟) ∈ 𝑆) → (((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((ℎ + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠))) |
49 | 44, 45, 48 | syl2an 596 |
. . . . . . . . 9
⊢ (((ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑓 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((ℎ + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠))) |
50 | 49 | 3impb 1114 |
. . . . . . . 8
⊢ (((ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ 𝑓 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆) → (((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((ℎ + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠))) |
51 | 50 | 3com12 1122 |
. . . . . . 7
⊢ ((𝑓 ∈ 𝑆 ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ 𝑟 ∈ 𝑆) → (((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((ℎ + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠))) |
52 | 51 | 3adant3l 1179 |
. . . . . 6
⊢ ((𝑓 ∈ 𝑆 ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((ℎ + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠))) |
53 | 52 | 3adant1r 1176 |
. . . . 5
⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (((ℎ + 𝑡) + (𝑓 + 𝑟)) = ((ℎ + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠))) |
54 | 42, 53 | syld 47 |
. . . 4
⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((〈𝑓, 𝑔〉 ∼ 〈ℎ, 𝑡〉 ∧ 〈ℎ, 𝑡〉 ∼ 〈𝑠, 𝑟〉) → (𝑓 + 𝑟) = (𝑔 + 𝑠))) |
55 | 1 | ecopoveq 8599 |
. . . . 5
⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (〈𝑓, 𝑔〉 ∼ 〈𝑠, 𝑟〉 ↔ (𝑓 + 𝑟) = (𝑔 + 𝑠))) |
56 | 55 | 3adant2 1130 |
. . . 4
⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (〈𝑓, 𝑔〉 ∼ 〈𝑠, 𝑟〉 ↔ (𝑓 + 𝑟) = (𝑔 + 𝑠))) |
57 | 54, 56 | sylibrd 258 |
. . 3
⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((〈𝑓, 𝑔〉 ∼ 〈ℎ, 𝑡〉 ∧ 〈ℎ, 𝑡〉 ∼ 〈𝑠, 𝑟〉) → 〈𝑓, 𝑔〉 ∼ 〈𝑠, 𝑟〉)) |
58 | 10, 14, 18, 22, 57 | 3optocl 5683 |
. 2
⊢ ((𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)) → ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶) → 𝐴 ∼ 𝐶)) |
59 | 9, 58 | mpcom 38 |
1
⊢ ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶) → 𝐴 ∼ 𝐶) |