Step | Hyp | Ref
| Expression |
1 | | relxp 5602 |
. . . . . 6
⊢ Rel
(𝐶 × 𝐵) |
2 | 1 | rgenw 3076 |
. . . . 5
⊢
∀𝑥 ∈
𝐴 Rel (𝐶 × 𝐵) |
3 | | r19.2z 4425 |
. . . . 5
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 Rel (𝐶 × 𝐵)) → ∃𝑥 ∈ 𝐴 Rel (𝐶 × 𝐵)) |
4 | 2, 3 | mpan2 688 |
. . . 4
⊢ (𝐴 ≠ ∅ →
∃𝑥 ∈ 𝐴 Rel (𝐶 × 𝐵)) |
5 | | reliin 5720 |
. . . 4
⊢
(∃𝑥 ∈
𝐴 Rel (𝐶 × 𝐵) → Rel ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵)) |
6 | 4, 5 | syl 17 |
. . 3
⊢ (𝐴 ≠ ∅ → Rel
∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵)) |
7 | | relxp 5602 |
. . 3
⊢ Rel
(𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵) |
8 | 6, 7 | jctil 520 |
. 2
⊢ (𝐴 ≠ ∅ → (Rel (𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵) ∧ Rel ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵))) |
9 | | r19.28zv 4431 |
. . . . . 6
⊢ (𝐴 ≠ ∅ →
(∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐵) ↔ (𝑦 ∈ 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵))) |
10 | 9 | bicomd 222 |
. . . . 5
⊢ (𝐴 ≠ ∅ → ((𝑦 ∈ 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵) ↔ ∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐵))) |
11 | | eliin 4929 |
. . . . . . 7
⊢ (𝑧 ∈ V → (𝑧 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵)) |
12 | 11 | elv 3435 |
. . . . . 6
⊢ (𝑧 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵) |
13 | 12 | anbi2i 623 |
. . . . 5
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑧 ∈ ∩
𝑥 ∈ 𝐴 𝐵) ↔ (𝑦 ∈ 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵)) |
14 | | opelxp 5620 |
. . . . . 6
⊢
(〈𝑦, 𝑧〉 ∈ (𝐶 × 𝐵) ↔ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐵)) |
15 | 14 | ralbii 3091 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 〈𝑦, 𝑧〉 ∈ (𝐶 × 𝐵) ↔ ∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐵)) |
16 | 10, 13, 15 | 3bitr4g 314 |
. . . 4
⊢ (𝐴 ≠ ∅ → ((𝑦 ∈ 𝐶 ∧ 𝑧 ∈ ∩
𝑥 ∈ 𝐴 𝐵) ↔ ∀𝑥 ∈ 𝐴 〈𝑦, 𝑧〉 ∈ (𝐶 × 𝐵))) |
17 | | opelxp 5620 |
. . . 4
⊢
(〈𝑦, 𝑧〉 ∈ (𝐶 × ∩
𝑥 ∈ 𝐴 𝐵) ↔ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ ∩
𝑥 ∈ 𝐴 𝐵)) |
18 | | opex 5377 |
. . . . 5
⊢
〈𝑦, 𝑧〉 ∈ V |
19 | | eliin 4929 |
. . . . 5
⊢
(〈𝑦, 𝑧〉 ∈ V →
(〈𝑦, 𝑧〉 ∈ ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵) ↔ ∀𝑥 ∈ 𝐴 〈𝑦, 𝑧〉 ∈ (𝐶 × 𝐵))) |
20 | 18, 19 | ax-mp 5 |
. . . 4
⊢
(〈𝑦, 𝑧〉 ∈ ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵) ↔ ∀𝑥 ∈ 𝐴 〈𝑦, 𝑧〉 ∈ (𝐶 × 𝐵)) |
21 | 16, 17, 20 | 3bitr4g 314 |
. . 3
⊢ (𝐴 ≠ ∅ →
(〈𝑦, 𝑧〉 ∈ (𝐶 × ∩
𝑥 ∈ 𝐴 𝐵) ↔ 〈𝑦, 𝑧〉 ∈ ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵))) |
22 | 21 | eqrelrdv2 5698 |
. 2
⊢ (((Rel
(𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵) ∧ Rel ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵)) ∧ 𝐴 ≠ ∅) → (𝐶 × ∩
𝑥 ∈ 𝐴 𝐵) = ∩
𝑥 ∈ 𝐴 (𝐶 × 𝐵)) |
23 | 8, 22 | mpancom 685 |
1
⊢ (𝐴 ≠ ∅ → (𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵) = ∩
𝑥 ∈ 𝐴 (𝐶 × 𝐵)) |