Step | Hyp | Ref
| Expression |
1 | | ibar 299 |
. . . 4
⊢
(∃𝑥 𝑥 ∈ 𝐵 → ((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶) ↔ (∃𝑥 𝑥 ∈ 𝐵 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶)))) |
2 | | ancom 264 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐴)) |
3 | 2 | anbi1i 455 |
. . . . . . 7
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐴) ∧ (𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶))) |
4 | | brxp 4642 |
. . . . . . . 8
⊢ (𝑎(𝐴 × 𝐵)𝑥 ↔ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) |
5 | | brxp 4642 |
. . . . . . . 8
⊢ (𝑥(𝐵 × 𝐶)𝑐 ↔ (𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) |
6 | 4, 5 | anbi12i 457 |
. . . . . . 7
⊢ ((𝑎(𝐴 × 𝐵)𝑥 ∧ 𝑥(𝐵 × 𝐶)𝑐) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶))) |
7 | | anandi 585 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐵 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶)) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐴) ∧ (𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶))) |
8 | 3, 6, 7 | 3bitr4i 211 |
. . . . . 6
⊢ ((𝑎(𝐴 × 𝐵)𝑥 ∧ 𝑥(𝐵 × 𝐶)𝑐) ↔ (𝑥 ∈ 𝐵 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶))) |
9 | 8 | exbii 1598 |
. . . . 5
⊢
(∃𝑥(𝑎(𝐴 × 𝐵)𝑥 ∧ 𝑥(𝐵 × 𝐶)𝑐) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶))) |
10 | | 19.41v 1895 |
. . . . 5
⊢
(∃𝑥(𝑥 ∈ 𝐵 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶)) ↔ (∃𝑥 𝑥 ∈ 𝐵 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶))) |
11 | 9, 10 | bitr2i 184 |
. . . 4
⊢
((∃𝑥 𝑥 ∈ 𝐵 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶)) ↔ ∃𝑥(𝑎(𝐴 × 𝐵)𝑥 ∧ 𝑥(𝐵 × 𝐶)𝑐)) |
12 | 1, 11 | bitr2di 196 |
. . 3
⊢
(∃𝑥 𝑥 ∈ 𝐵 → (∃𝑥(𝑎(𝐴 × 𝐵)𝑥 ∧ 𝑥(𝐵 × 𝐶)𝑐) ↔ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶))) |
13 | 12 | opabbidv 4055 |
. 2
⊢
(∃𝑥 𝑥 ∈ 𝐵 → {〈𝑎, 𝑐〉 ∣ ∃𝑥(𝑎(𝐴 × 𝐵)𝑥 ∧ 𝑥(𝐵 × 𝐶)𝑐)} = {〈𝑎, 𝑐〉 ∣ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶)}) |
14 | | df-co 4620 |
. 2
⊢ ((𝐵 × 𝐶) ∘ (𝐴 × 𝐵)) = {〈𝑎, 𝑐〉 ∣ ∃𝑥(𝑎(𝐴 × 𝐵)𝑥 ∧ 𝑥(𝐵 × 𝐶)𝑐)} |
15 | | df-xp 4617 |
. 2
⊢ (𝐴 × 𝐶) = {〈𝑎, 𝑐〉 ∣ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐶)} |
16 | 13, 14, 15 | 3eqtr4g 2228 |
1
⊢
(∃𝑥 𝑥 ∈ 𝐵 → ((𝐵 × 𝐶) ∘ (𝐴 × 𝐵)) = (𝐴 × 𝐶)) |