Step | Hyp | Ref
| Expression |
1 | | relxp 4447 |
. . . . . 6
⊢ Rel
(𝐶 × 𝐵) |
2 | 1 | rgenw 2376 |
. . . . 5
⊢
∀𝑥 ∈
𝐴 Rel (𝐶 × 𝐵) |
3 | | eleq1 2100 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
4 | 3 | cbvexv 1795 |
. . . . . 6
⊢
(∃𝑥 𝑥 ∈ 𝐴 ↔ ∃𝑦 𝑦 ∈ 𝐴) |
5 | | r19.2m 3309 |
. . . . . 6
⊢
((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 Rel (𝐶 × 𝐵)) → ∃𝑥 ∈ 𝐴 Rel (𝐶 × 𝐵)) |
6 | 4, 5 | sylanbr 269 |
. . . . 5
⊢
((∃𝑦 𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 Rel (𝐶 × 𝐵)) → ∃𝑥 ∈ 𝐴 Rel (𝐶 × 𝐵)) |
7 | 2, 6 | mpan2 401 |
. . . 4
⊢
(∃𝑦 𝑦 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 Rel (𝐶 × 𝐵)) |
8 | | reliin 4459 |
. . . 4
⊢
(∃𝑥 ∈
𝐴 Rel (𝐶 × 𝐵) → Rel ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵)) |
9 | 7, 8 | syl 14 |
. . 3
⊢
(∃𝑦 𝑦 ∈ 𝐴 → Rel ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵)) |
10 | | relxp 4447 |
. . 3
⊢ Rel
(𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵) |
11 | 9, 10 | jctil 295 |
. 2
⊢
(∃𝑦 𝑦 ∈ 𝐴 → (Rel (𝐶 × ∩
𝑥 ∈ 𝐴 𝐵) ∧ Rel ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵))) |
12 | | r19.28mv 3314 |
. . . . . . 7
⊢
(∃𝑥 𝑥 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (𝑤 ∈ 𝐶 ∧ 𝑧 ∈ 𝐵) ↔ (𝑤 ∈ 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵))) |
13 | 4, 12 | sylbir 125 |
. . . . . 6
⊢
(∃𝑦 𝑦 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (𝑤 ∈ 𝐶 ∧ 𝑧 ∈ 𝐵) ↔ (𝑤 ∈ 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵))) |
14 | 13 | bicomd 129 |
. . . . 5
⊢
(∃𝑦 𝑦 ∈ 𝐴 → ((𝑤 ∈ 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵) ↔ ∀𝑥 ∈ 𝐴 (𝑤 ∈ 𝐶 ∧ 𝑧 ∈ 𝐵))) |
15 | | vex 2560 |
. . . . . . 7
⊢ 𝑧 ∈ V |
16 | | eliin 3662 |
. . . . . . 7
⊢ (𝑧 ∈ V → (𝑧 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵)) |
17 | 15, 16 | ax-mp 7 |
. . . . . 6
⊢ (𝑧 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵) |
18 | 17 | anbi2i 430 |
. . . . 5
⊢ ((𝑤 ∈ 𝐶 ∧ 𝑧 ∈ ∩
𝑥 ∈ 𝐴 𝐵) ↔ (𝑤 ∈ 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵)) |
19 | | opelxp 4374 |
. . . . . 6
⊢
(〈𝑤, 𝑧〉 ∈ (𝐶 × 𝐵) ↔ (𝑤 ∈ 𝐶 ∧ 𝑧 ∈ 𝐵)) |
20 | 19 | ralbii 2330 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 〈𝑤, 𝑧〉 ∈ (𝐶 × 𝐵) ↔ ∀𝑥 ∈ 𝐴 (𝑤 ∈ 𝐶 ∧ 𝑧 ∈ 𝐵)) |
21 | 14, 18, 20 | 3bitr4g 212 |
. . . 4
⊢
(∃𝑦 𝑦 ∈ 𝐴 → ((𝑤 ∈ 𝐶 ∧ 𝑧 ∈ ∩
𝑥 ∈ 𝐴 𝐵) ↔ ∀𝑥 ∈ 𝐴 〈𝑤, 𝑧〉 ∈ (𝐶 × 𝐵))) |
22 | | opelxp 4374 |
. . . 4
⊢
(〈𝑤, 𝑧〉 ∈ (𝐶 × ∩
𝑥 ∈ 𝐴 𝐵) ↔ (𝑤 ∈ 𝐶 ∧ 𝑧 ∈ ∩
𝑥 ∈ 𝐴 𝐵)) |
23 | | vex 2560 |
. . . . . 6
⊢ 𝑤 ∈ V |
24 | 23, 15 | opex 3966 |
. . . . 5
⊢
〈𝑤, 𝑧〉 ∈ V |
25 | | eliin 3662 |
. . . . 5
⊢
(〈𝑤, 𝑧〉 ∈ V →
(〈𝑤, 𝑧〉 ∈ ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵) ↔ ∀𝑥 ∈ 𝐴 〈𝑤, 𝑧〉 ∈ (𝐶 × 𝐵))) |
26 | 24, 25 | ax-mp 7 |
. . . 4
⊢
(〈𝑤, 𝑧〉 ∈ ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵) ↔ ∀𝑥 ∈ 𝐴 〈𝑤, 𝑧〉 ∈ (𝐶 × 𝐵)) |
27 | 21, 22, 26 | 3bitr4g 212 |
. . 3
⊢
(∃𝑦 𝑦 ∈ 𝐴 → (〈𝑤, 𝑧〉 ∈ (𝐶 × ∩
𝑥 ∈ 𝐴 𝐵) ↔ 〈𝑤, 𝑧〉 ∈ ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵))) |
28 | 27 | eqrelrdv2 4439 |
. 2
⊢ (((Rel
(𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵) ∧ Rel ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵)) ∧ ∃𝑦 𝑦 ∈ 𝐴) → (𝐶 × ∩
𝑥 ∈ 𝐴 𝐵) = ∩
𝑥 ∈ 𝐴 (𝐶 × 𝐵)) |
29 | 11, 28 | mpancom 399 |
1
⊢
(∃𝑦 𝑦 ∈ 𝐴 → (𝐶 × ∩
𝑥 ∈ 𝐴 𝐵) = ∩
𝑥 ∈ 𝐴 (𝐶 × 𝐵)) |