Step | Hyp | Ref
| Expression |
1 | | ecopopr.1 |
. . . . 5
⊢ ∼ =
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} |
2 | | opabssxp 4685 |
. . . . 5
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} ⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆)) |
3 | 1, 2 | eqsstri 3179 |
. . . 4
⊢ ∼
⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆)) |
4 | 3 | brel 4663 |
. . 3
⊢ (𝐴 ∼ 𝐵 → (𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆))) |
5 | | eqid 2170 |
. . . 4
⊢ (𝑆 × 𝑆) = (𝑆 × 𝑆) |
6 | | breq1 3992 |
. . . . 5
⊢
(〈𝑓, 𝑔〉 = 𝐴 → (〈𝑓, 𝑔〉 ∼ 〈ℎ, 𝑡〉 ↔ 𝐴 ∼ 〈ℎ, 𝑡〉)) |
7 | | breq2 3993 |
. . . . 5
⊢
(〈𝑓, 𝑔〉 = 𝐴 → (〈ℎ, 𝑡〉 ∼ 〈𝑓, 𝑔〉 ↔ 〈ℎ, 𝑡〉 ∼ 𝐴)) |
8 | 6, 7 | bibi12d 234 |
. . . 4
⊢
(〈𝑓, 𝑔〉 = 𝐴 → ((〈𝑓, 𝑔〉 ∼ 〈ℎ, 𝑡〉 ↔ 〈ℎ, 𝑡〉 ∼ 〈𝑓, 𝑔〉) ↔ (𝐴 ∼ 〈ℎ, 𝑡〉 ↔ 〈ℎ, 𝑡〉 ∼ 𝐴))) |
9 | | breq2 3993 |
. . . . 5
⊢
(〈ℎ, 𝑡〉 = 𝐵 → (𝐴 ∼ 〈ℎ, 𝑡〉 ↔ 𝐴 ∼ 𝐵)) |
10 | | breq1 3992 |
. . . . 5
⊢
(〈ℎ, 𝑡〉 = 𝐵 → (〈ℎ, 𝑡〉 ∼ 𝐴 ↔ 𝐵 ∼ 𝐴)) |
11 | 9, 10 | bibi12d 234 |
. . . 4
⊢
(〈ℎ, 𝑡〉 = 𝐵 → ((𝐴 ∼ 〈ℎ, 𝑡〉 ↔ 〈ℎ, 𝑡〉 ∼ 𝐴) ↔ (𝐴 ∼ 𝐵 ↔ 𝐵 ∼ 𝐴))) |
12 | | ecopoprg.com |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
13 | 12 | adantl 275 |
. . . . . . . 8
⊢ ((((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
14 | | simpll 524 |
. . . . . . . 8
⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) → 𝑓 ∈ 𝑆) |
15 | | simprr 527 |
. . . . . . . 8
⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) → 𝑡 ∈ 𝑆) |
16 | 13, 14, 15 | caovcomd 6009 |
. . . . . . 7
⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) → (𝑓 + 𝑡) = (𝑡 + 𝑓)) |
17 | | simplr 525 |
. . . . . . . 8
⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) → 𝑔 ∈ 𝑆) |
18 | | simprl 526 |
. . . . . . . 8
⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) → ℎ ∈ 𝑆) |
19 | 13, 17, 18 | caovcomd 6009 |
. . . . . . 7
⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) → (𝑔 + ℎ) = (ℎ + 𝑔)) |
20 | 16, 19 | eqeq12d 2185 |
. . . . . 6
⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) → ((𝑓 + 𝑡) = (𝑔 + ℎ) ↔ (𝑡 + 𝑓) = (ℎ + 𝑔))) |
21 | | eqcom 2172 |
. . . . . 6
⊢ ((𝑡 + 𝑓) = (ℎ + 𝑔) ↔ (ℎ + 𝑔) = (𝑡 + 𝑓)) |
22 | 20, 21 | bitrdi 195 |
. . . . 5
⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) → ((𝑓 + 𝑡) = (𝑔 + ℎ) ↔ (ℎ + 𝑔) = (𝑡 + 𝑓))) |
23 | 1 | ecopoveq 6608 |
. . . . 5
⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) → (〈𝑓, 𝑔〉 ∼ 〈ℎ, 𝑡〉 ↔ (𝑓 + 𝑡) = (𝑔 + ℎ))) |
24 | 1 | ecopoveq 6608 |
. . . . . 6
⊢ (((ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆)) → (〈ℎ, 𝑡〉 ∼ 〈𝑓, 𝑔〉 ↔ (ℎ + 𝑔) = (𝑡 + 𝑓))) |
25 | 24 | ancoms 266 |
. . . . 5
⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) → (〈ℎ, 𝑡〉 ∼ 〈𝑓, 𝑔〉 ↔ (ℎ + 𝑔) = (𝑡 + 𝑓))) |
26 | 22, 23, 25 | 3bitr4d 219 |
. . . 4
⊢ (((𝑓 ∈ 𝑆 ∧ 𝑔 ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) → (〈𝑓, 𝑔〉 ∼ 〈ℎ, 𝑡〉 ↔ 〈ℎ, 𝑡〉 ∼ 〈𝑓, 𝑔〉)) |
27 | 5, 8, 11, 26 | 2optocl 4688 |
. . 3
⊢ ((𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆)) → (𝐴 ∼ 𝐵 ↔ 𝐵 ∼ 𝐴)) |
28 | 4, 27 | syl 14 |
. 2
⊢ (𝐴 ∼ 𝐵 → (𝐴 ∼ 𝐵 ↔ 𝐵 ∼ 𝐴)) |
29 | 28 | ibi 175 |
1
⊢ (𝐴 ∼ 𝐵 → 𝐵 ∼ 𝐴) |