Step | Hyp | Ref
| Expression |
1 | | xpcogend.1 |
. . . . . 6
⊢ (𝜑 → (𝐵 ∩ 𝐶) ≠ ∅) |
2 | | ndisj 4247 |
. . . . . 6
⊢ ((𝐵 ∩ 𝐶) ≠ ∅ ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) |
3 | 1, 2 | sylib 219 |
. . . . 5
⊢ (𝜑 → ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) |
4 | 3 | biantrud 532 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷) ∧ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))) |
5 | | brxp 5489 |
. . . . . . 7
⊢ (𝑥(𝐴 × 𝐵)𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
6 | | brxp 5489 |
. . . . . . . 8
⊢ (𝑦(𝐶 × 𝐷)𝑧 ↔ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐷)) |
7 | 6 | biancomi 463 |
. . . . . . 7
⊢ (𝑦(𝐶 × 𝐷)𝑧 ↔ (𝑧 ∈ 𝐷 ∧ 𝑦 ∈ 𝐶)) |
8 | 5, 7 | anbi12i 626 |
. . . . . 6
⊢ ((𝑥(𝐴 × 𝐵)𝑦 ∧ 𝑦(𝐶 × 𝐷)𝑧) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑦 ∈ 𝐶))) |
9 | 8 | exbii 1829 |
. . . . 5
⊢
(∃𝑦(𝑥(𝐴 × 𝐵)𝑦 ∧ 𝑦(𝐶 × 𝐷)𝑧) ↔ ∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑦 ∈ 𝐶))) |
10 | | an4 652 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑦 ∈ 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) |
11 | 10 | exbii 1829 |
. . . . 5
⊢
(∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) |
12 | | 19.42v 1931 |
. . . . 5
⊢
(∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷) ∧ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) |
13 | 9, 11, 12 | 3bitri 298 |
. . . 4
⊢
(∃𝑦(𝑥(𝐴 × 𝐵)𝑦 ∧ 𝑦(𝐶 × 𝐷)𝑧) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷) ∧ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) |
14 | 4, 13 | syl6rbbr 291 |
. . 3
⊢ (𝜑 → (∃𝑦(𝑥(𝐴 × 𝐵)𝑦 ∧ 𝑦(𝐶 × 𝐷)𝑧) ↔ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷))) |
15 | 14 | opabbidv 5028 |
. 2
⊢ (𝜑 → {〈𝑥, 𝑧〉 ∣ ∃𝑦(𝑥(𝐴 × 𝐵)𝑦 ∧ 𝑦(𝐶 × 𝐷)𝑧)} = {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷)}) |
16 | | df-co 5452 |
. 2
⊢ ((𝐶 × 𝐷) ∘ (𝐴 × 𝐵)) = {〈𝑥, 𝑧〉 ∣ ∃𝑦(𝑥(𝐴 × 𝐵)𝑦 ∧ 𝑦(𝐶 × 𝐷)𝑧)} |
17 | | df-xp 5449 |
. 2
⊢ (𝐴 × 𝐷) = {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷)} |
18 | 15, 16, 17 | 3eqtr4g 2856 |
1
⊢ (𝜑 → ((𝐶 × 𝐷) ∘ (𝐴 × 𝐵)) = (𝐴 × 𝐷)) |