Step | Hyp | Ref
| Expression |
1 | | ibar 285 |
. . . 4
⊢ (∃x x ∈ B → ((𝑎 ∈ A ∧ 𝑐 ∈ 𝐶) ↔ (∃x x ∈ B ∧ (𝑎 ∈ A ∧ 𝑐
∈ 𝐶)))) |
2 | | ancom 253 |
. . . . . . . 8
⊢ ((𝑎 ∈ A ∧ x ∈ B) ↔
(x ∈
B ∧ 𝑎 ∈ A)) |
3 | 2 | anbi1i 431 |
. . . . . . 7
⊢ (((𝑎 ∈ A ∧ x ∈ B) ∧ (x ∈ B ∧ 𝑐
∈ 𝐶)) ↔ ((x ∈ B ∧ 𝑎 ∈ A) ∧ (x ∈ B ∧ 𝑐 ∈ 𝐶))) |
4 | | brxp 4318 |
. . . . . . . 8
⊢ (𝑎(A × B)x ↔
(𝑎 ∈ A ∧ x ∈ B)) |
5 | | brxp 4318 |
. . . . . . . 8
⊢ (x(B ×
𝐶)𝑐 ↔ (x ∈ B ∧ 𝑐 ∈ 𝐶)) |
6 | 4, 5 | anbi12i 433 |
. . . . . . 7
⊢ ((𝑎(A × B)x ∧ x(B × 𝐶)𝑐) ↔ ((𝑎 ∈ A ∧ x ∈ B) ∧ (x ∈ B ∧ 𝑐 ∈ 𝐶))) |
7 | | anandi 524 |
. . . . . . 7
⊢
((x ∈ B ∧ (𝑎 ∈ A ∧ 𝑐 ∈ 𝐶)) ↔ ((x ∈ B ∧ 𝑎 ∈ A) ∧ (x ∈ B ∧ 𝑐 ∈ 𝐶))) |
8 | 3, 6, 7 | 3bitr4i 201 |
. . . . . 6
⊢ ((𝑎(A × B)x ∧ x(B × 𝐶)𝑐) ↔ (x ∈ B ∧ (𝑎 ∈ A ∧ 𝑐
∈ 𝐶))) |
9 | 8 | exbii 1493 |
. . . . 5
⊢ (∃x(𝑎(A × B)x ∧ x(B × 𝐶)𝑐) ↔ ∃x(x ∈ B ∧ (𝑎 ∈ A ∧ 𝑐
∈ 𝐶))) |
10 | | 19.41v 1779 |
. . . . 5
⊢ (∃x(x ∈ B ∧ (𝑎 ∈ A ∧ 𝑐
∈ 𝐶)) ↔ (∃x x ∈ B ∧ (𝑎 ∈ A ∧ 𝑐
∈ 𝐶))) |
11 | 9, 10 | bitr2i 174 |
. . . 4
⊢ ((∃x x ∈ B ∧ (𝑎 ∈ A ∧ 𝑐
∈ 𝐶)) ↔ ∃x(𝑎(A × B)x ∧ x(B × 𝐶)𝑐)) |
12 | 1, 11 | syl6rbb 186 |
. . 3
⊢ (∃x x ∈ B → (∃x(𝑎(A × B)x ∧ x(B × 𝐶)𝑐) ↔ (𝑎 ∈ A ∧ 𝑐 ∈ 𝐶))) |
13 | 12 | opabbidv 3814 |
. 2
⊢ (∃x x ∈ B → {〈𝑎, 𝑐〉 ∣ ∃x(𝑎(A × B)x ∧ x(B × 𝐶)𝑐)} = {〈𝑎, 𝑐〉 ∣ (𝑎 ∈ A ∧ 𝑐 ∈ 𝐶)}) |
14 | | df-co 4297 |
. 2
⊢
((B × 𝐶) ∘ (A × B)) =
{〈𝑎, 𝑐〉 ∣ ∃x(𝑎(A × B)x ∧ x(B × 𝐶)𝑐)} |
15 | | df-xp 4294 |
. 2
⊢ (A × 𝐶) = {〈𝑎, 𝑐〉 ∣ (𝑎 ∈ A ∧ 𝑐 ∈ 𝐶)} |
16 | 13, 14, 15 | 3eqtr4g 2094 |
1
⊢ (∃x x ∈ B → ((B
× 𝐶) ∘
(A × B)) = (A ×
𝐶)) |