Step | Hyp | Ref
| Expression |
1 | | ecopopr.1 |
. . . . 5
⊢ ∼ =
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} |
2 | | opabssxp 5640 |
. . . . 5
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} ⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆)) |
3 | 1, 2 | eqsstri 3935 |
. . . 4
⊢ ∼
⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆)) |
4 | 3 | brel 5614 |
. . 3
⊢ (𝐴 ∼ 𝐵 → (𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆))) |
5 | | eqid 2737 |
. . . 4
⊢ (𝑆 × 𝑆) = (𝑆 × 𝑆) |
6 | | breq1 5056 |
. . . . 5
⊢
(〈𝑓, 𝑔〉 = 𝐴 → (〈𝑓, 𝑔〉 ∼ 〈ℎ, 𝑡〉 ↔ 𝐴 ∼ 〈ℎ, 𝑡〉)) |
7 | | breq2 5057 |
. . . . 5
⊢
(〈𝑓, 𝑔〉 = 𝐴 → (〈ℎ, 𝑡〉 ∼ 〈𝑓, 𝑔〉 ↔ 〈ℎ, 𝑡〉 ∼ 𝐴)) |
8 | 6, 7 | bibi12d 349 |
. . . 4
⊢
(〈𝑓, 𝑔〉 = 𝐴 → ((〈𝑓, 𝑔〉 ∼ 〈ℎ, 𝑡〉 ↔ 〈ℎ, 𝑡〉 ∼ 〈𝑓, 𝑔〉) ↔ (𝐴 ∼ 〈ℎ, 𝑡〉 ↔ 〈ℎ, 𝑡〉 ∼ 𝐴))) |
9 | | breq2 5057 |
. . . . 5
⊢
(〈ℎ, 𝑡〉 = 𝐵 → (𝐴 ∼ 〈ℎ, 𝑡〉 ↔ 𝐴 ∼ 𝐵)) |
10 | | breq1 5056 |
. . . . 5
⊢
(〈ℎ, 𝑡〉 = 𝐵 → (〈ℎ, 𝑡〉 ∼ 𝐴 ↔ 𝐵 ∼ 𝐴)) |
11 | 9, 10 | bibi12d 349 |
. . . 4
⊢
(〈ℎ, 𝑡〉 = 𝐵 → ((𝐴 ∼ 〈ℎ, 𝑡〉 ↔ 〈ℎ, 𝑡〉 ∼ 𝐴) ↔ (𝐴 ∼ 𝐵 ↔ 𝐵 ∼ 𝐴))) |
12 | 1 | ecopoveq 8500 |
. . . . . 6
⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) → (〈𝑓, 𝑔〉 ∼ 〈ℎ, 𝑡〉 ↔ (𝑓 + 𝑡) = (𝑔 + ℎ))) |
13 | | vex 3412 |
. . . . . . . . 9
⊢ 𝑓 ∈ V |
14 | | vex 3412 |
. . . . . . . . 9
⊢ 𝑡 ∈ V |
15 | | ecopopr.com |
. . . . . . . . 9
⊢ (𝑥 + 𝑦) = (𝑦 + 𝑥) |
16 | 13, 14, 15 | caovcom 7405 |
. . . . . . . 8
⊢ (𝑓 + 𝑡) = (𝑡 + 𝑓) |
17 | | vex 3412 |
. . . . . . . . 9
⊢ 𝑔 ∈ V |
18 | | vex 3412 |
. . . . . . . . 9
⊢ ℎ ∈ V |
19 | 17, 18, 15 | caovcom 7405 |
. . . . . . . 8
⊢ (𝑔 + ℎ) = (ℎ + 𝑔) |
20 | 16, 19 | eqeq12i 2755 |
. . . . . . 7
⊢ ((𝑓 + 𝑡) = (𝑔 + ℎ) ↔ (𝑡 + 𝑓) = (ℎ + 𝑔)) |
21 | | eqcom 2744 |
. . . . . . 7
⊢ ((𝑡 + 𝑓) = (ℎ + 𝑔) ↔ (ℎ + 𝑔) = (𝑡 + 𝑓)) |
22 | 20, 21 | bitri 278 |
. . . . . 6
⊢ ((𝑓 + 𝑡) = (𝑔 + ℎ) ↔ (ℎ + 𝑔) = (𝑡 + 𝑓)) |
23 | 12, 22 | bitrdi 290 |
. . . . 5
⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) → (〈𝑓, 𝑔〉 ∼ 〈ℎ, 𝑡〉 ↔ (ℎ + 𝑔) = (𝑡 + 𝑓))) |
24 | 1 | ecopoveq 8500 |
. . . . . 6
⊢ (((ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆)) → (〈ℎ, 𝑡〉 ∼ 〈𝑓, 𝑔〉 ↔ (ℎ + 𝑔) = (𝑡 + 𝑓))) |
25 | 24 | ancoms 462 |
. . . . 5
⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) → (〈ℎ, 𝑡〉 ∼ 〈𝑓, 𝑔〉 ↔ (ℎ + 𝑔) = (𝑡 + 𝑓))) |
26 | 23, 25 | bitr4d 285 |
. . . 4
⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) → (〈𝑓, 𝑔〉 ∼ 〈ℎ, 𝑡〉 ↔ 〈ℎ, 𝑡〉 ∼ 〈𝑓, 𝑔〉)) |
27 | 5, 8, 11, 26 | 2optocl 5643 |
. . 3
⊢ ((𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆)) → (𝐴 ∼ 𝐵 ↔ 𝐵 ∼ 𝐴)) |
28 | 4, 27 | syl 17 |
. 2
⊢ (𝐴 ∼ 𝐵 → (𝐴 ∼ 𝐵 ↔ 𝐵 ∼ 𝐴)) |
29 | 28 | ibi 270 |
1
⊢ (𝐴 ∼ 𝐵 → 𝐵 ∼ 𝐴) |