Step | Hyp | Ref
| Expression |
1 | | xpcogend.1 |
. . . . . 6
⊢ (𝜑 → (𝐵 ∩ 𝐶) ≠ ∅) |
2 | | n0 3931 |
. . . . . . 7
⊢ ((𝐵 ∩ 𝐶) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝐵 ∩ 𝐶)) |
3 | | elin 3796 |
. . . . . . . 8
⊢ (𝑦 ∈ (𝐵 ∩ 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) |
4 | 3 | exbii 1774 |
. . . . . . 7
⊢
(∃𝑦 𝑦 ∈ (𝐵 ∩ 𝐶) ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) |
5 | 2, 4 | bitri 264 |
. . . . . 6
⊢ ((𝐵 ∩ 𝐶) ≠ ∅ ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) |
6 | 1, 5 | sylib 208 |
. . . . 5
⊢ (𝜑 → ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) |
7 | 6 | biantrud 528 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷) ∧ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))) |
8 | | brxp 5147 |
. . . . . . 7
⊢ (𝑥(𝐴 × 𝐵)𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
9 | | brxp 5147 |
. . . . . . . 8
⊢ (𝑦(𝐶 × 𝐷)𝑧 ↔ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐷)) |
10 | | ancom 466 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐷) ↔ (𝑧 ∈ 𝐷 ∧ 𝑦 ∈ 𝐶)) |
11 | 9, 10 | bitri 264 |
. . . . . . 7
⊢ (𝑦(𝐶 × 𝐷)𝑧 ↔ (𝑧 ∈ 𝐷 ∧ 𝑦 ∈ 𝐶)) |
12 | 8, 11 | anbi12i 733 |
. . . . . 6
⊢ ((𝑥(𝐴 × 𝐵)𝑦 ∧ 𝑦(𝐶 × 𝐷)𝑧) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑦 ∈ 𝐶))) |
13 | 12 | exbii 1774 |
. . . . 5
⊢
(∃𝑦(𝑥(𝐴 × 𝐵)𝑦 ∧ 𝑦(𝐶 × 𝐷)𝑧) ↔ ∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑦 ∈ 𝐶))) |
14 | | an4 865 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑦 ∈ 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) |
15 | 14 | exbii 1774 |
. . . . 5
⊢
(∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) |
16 | | 19.42v 1918 |
. . . . 5
⊢
(∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷) ∧ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) |
17 | 13, 15, 16 | 3bitri 286 |
. . . 4
⊢
(∃𝑦(𝑥(𝐴 × 𝐵)𝑦 ∧ 𝑦(𝐶 × 𝐷)𝑧) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷) ∧ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) |
18 | 7, 17 | syl6rbbr 279 |
. . 3
⊢ (𝜑 → (∃𝑦(𝑥(𝐴 × 𝐵)𝑦 ∧ 𝑦(𝐶 × 𝐷)𝑧) ↔ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷))) |
19 | 18 | opabbidv 4716 |
. 2
⊢ (𝜑 → {〈𝑥, 𝑧〉 ∣ ∃𝑦(𝑥(𝐴 × 𝐵)𝑦 ∧ 𝑦(𝐶 × 𝐷)𝑧)} = {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷)}) |
20 | | df-co 5123 |
. 2
⊢ ((𝐶 × 𝐷) ∘ (𝐴 × 𝐵)) = {〈𝑥, 𝑧〉 ∣ ∃𝑦(𝑥(𝐴 × 𝐵)𝑦 ∧ 𝑦(𝐶 × 𝐷)𝑧)} |
21 | | df-xp 5120 |
. 2
⊢ (𝐴 × 𝐷) = {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐷)} |
22 | 19, 20, 21 | 3eqtr4g 2681 |
1
⊢ (𝜑 → ((𝐶 × 𝐷) ∘ (𝐴 × 𝐵)) = (𝐴 × 𝐷)) |