Step | Hyp | Ref
| Expression |
1 | | relxp 5359 |
. . . . . 6
⊢ Rel
(𝐶 × 𝐵) |
2 | 1 | rgenw 3132 |
. . . . 5
⊢
∀𝑥 ∈
𝐴 Rel (𝐶 × 𝐵) |
3 | | r19.2z 4281 |
. . . . 5
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 Rel (𝐶 × 𝐵)) → ∃𝑥 ∈ 𝐴 Rel (𝐶 × 𝐵)) |
4 | 2, 3 | mpan2 684 |
. . . 4
⊢ (𝐴 ≠ ∅ →
∃𝑥 ∈ 𝐴 Rel (𝐶 × 𝐵)) |
5 | | reliin 5474 |
. . . 4
⊢
(∃𝑥 ∈
𝐴 Rel (𝐶 × 𝐵) → Rel ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵)) |
6 | 4, 5 | syl 17 |
. . 3
⊢ (𝐴 ≠ ∅ → Rel
∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵)) |
7 | | relxp 5359 |
. . 3
⊢ Rel
(𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵) |
8 | 6, 7 | jctil 517 |
. 2
⊢ (𝐴 ≠ ∅ → (Rel (𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵) ∧ Rel ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵))) |
9 | | r19.28zv 4287 |
. . . . . 6
⊢ (𝐴 ≠ ∅ →
(∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐵) ↔ (𝑦 ∈ 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵))) |
10 | 9 | bicomd 215 |
. . . . 5
⊢ (𝐴 ≠ ∅ → ((𝑦 ∈ 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵) ↔ ∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐵))) |
11 | | vex 3416 |
. . . . . . 7
⊢ 𝑧 ∈ V |
12 | | eliin 4744 |
. . . . . . 7
⊢ (𝑧 ∈ V → (𝑧 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵)) |
13 | 11, 12 | ax-mp 5 |
. . . . . 6
⊢ (𝑧 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵) |
14 | 13 | anbi2i 618 |
. . . . 5
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑧 ∈ ∩
𝑥 ∈ 𝐴 𝐵) ↔ (𝑦 ∈ 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵)) |
15 | | opelxp 5377 |
. . . . . 6
⊢
(〈𝑦, 𝑧〉 ∈ (𝐶 × 𝐵) ↔ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐵)) |
16 | 15 | ralbii 3188 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 〈𝑦, 𝑧〉 ∈ (𝐶 × 𝐵) ↔ ∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐵)) |
17 | 10, 14, 16 | 3bitr4g 306 |
. . . 4
⊢ (𝐴 ≠ ∅ → ((𝑦 ∈ 𝐶 ∧ 𝑧 ∈ ∩
𝑥 ∈ 𝐴 𝐵) ↔ ∀𝑥 ∈ 𝐴 〈𝑦, 𝑧〉 ∈ (𝐶 × 𝐵))) |
18 | | opelxp 5377 |
. . . 4
⊢
(〈𝑦, 𝑧〉 ∈ (𝐶 × ∩
𝑥 ∈ 𝐴 𝐵) ↔ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ ∩
𝑥 ∈ 𝐴 𝐵)) |
19 | | opex 5152 |
. . . . 5
⊢
〈𝑦, 𝑧〉 ∈ V |
20 | | eliin 4744 |
. . . . 5
⊢
(〈𝑦, 𝑧〉 ∈ V →
(〈𝑦, 𝑧〉 ∈ ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵) ↔ ∀𝑥 ∈ 𝐴 〈𝑦, 𝑧〉 ∈ (𝐶 × 𝐵))) |
21 | 19, 20 | ax-mp 5 |
. . . 4
⊢
(〈𝑦, 𝑧〉 ∈ ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵) ↔ ∀𝑥 ∈ 𝐴 〈𝑦, 𝑧〉 ∈ (𝐶 × 𝐵)) |
22 | 17, 18, 21 | 3bitr4g 306 |
. . 3
⊢ (𝐴 ≠ ∅ →
(〈𝑦, 𝑧〉 ∈ (𝐶 × ∩
𝑥 ∈ 𝐴 𝐵) ↔ 〈𝑦, 𝑧〉 ∈ ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵))) |
23 | 22 | eqrelrdv2 5452 |
. 2
⊢ (((Rel
(𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵) ∧ Rel ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵)) ∧ 𝐴 ≠ ∅) → (𝐶 × ∩
𝑥 ∈ 𝐴 𝐵) = ∩
𝑥 ∈ 𝐴 (𝐶 × 𝐵)) |
24 | 8, 23 | mpancom 681 |
1
⊢ (𝐴 ≠ ∅ → (𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵) = ∩
𝑥 ∈ 𝐴 (𝐶 × 𝐵)) |