Step | Hyp | Ref
| Expression |
1 | | eleq1w 2218 |
. . 3
⊢ (𝑦 = 𝑎 → (𝑦 ∈ 𝐴 ↔ 𝑎 ∈ 𝐴)) |
2 | 1 | cbvexv 1898 |
. 2
⊢
(∃𝑦 𝑦 ∈ 𝐴 ↔ ∃𝑎 𝑎 ∈ 𝐴) |
3 | | eleq1w 2218 |
. . . 4
⊢ (𝑥 = 𝑎 → (𝑥 ∈ 𝐴 ↔ 𝑎 ∈ 𝐴)) |
4 | 3 | cbvexv 1898 |
. . 3
⊢
(∃𝑥 𝑥 ∈ 𝐴 ↔ ∃𝑎 𝑎 ∈ 𝐴) |
5 | | relcnv 4964 |
. . . 4
⊢ Rel ◡∩ 𝑥 ∈ 𝐴 𝐵 |
6 | | r19.2m 3480 |
. . . . . . . 8
⊢
((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ◡𝐵 ⊆ (V × V)) → ∃𝑥 ∈ 𝐴 ◡𝐵 ⊆ (V × V)) |
7 | 6 | expcom 115 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 ◡𝐵 ⊆ (V × V) → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 ◡𝐵 ⊆ (V × V))) |
8 | | relcnv 4964 |
. . . . . . . . 9
⊢ Rel ◡𝐵 |
9 | | df-rel 4593 |
. . . . . . . . 9
⊢ (Rel
◡𝐵 ↔ ◡𝐵 ⊆ (V × V)) |
10 | 8, 9 | mpbi 144 |
. . . . . . . 8
⊢ ◡𝐵 ⊆ (V × V) |
11 | 10 | a1i 9 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → ◡𝐵 ⊆ (V × V)) |
12 | 7, 11 | mprg 2514 |
. . . . . 6
⊢
(∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 ◡𝐵 ⊆ (V × V)) |
13 | | iinss 3900 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐴 ◡𝐵 ⊆ (V × V) → ∩ 𝑥 ∈ 𝐴 ◡𝐵 ⊆ (V × V)) |
14 | 12, 13 | syl 14 |
. . . . 5
⊢
(∃𝑥 𝑥 ∈ 𝐴 → ∩
𝑥 ∈ 𝐴 ◡𝐵 ⊆ (V × V)) |
15 | | df-rel 4593 |
. . . . 5
⊢ (Rel
∩ 𝑥 ∈ 𝐴 ◡𝐵 ↔ ∩
𝑥 ∈ 𝐴 ◡𝐵 ⊆ (V × V)) |
16 | 14, 15 | sylibr 133 |
. . . 4
⊢
(∃𝑥 𝑥 ∈ 𝐴 → Rel ∩ 𝑥 ∈ 𝐴 ◡𝐵) |
17 | | vex 2715 |
. . . . . . . 8
⊢ 𝑏 ∈ V |
18 | | vex 2715 |
. . . . . . . 8
⊢ 𝑎 ∈ V |
19 | 17, 18 | opex 4189 |
. . . . . . 7
⊢
〈𝑏, 𝑎〉 ∈ V |
20 | | eliin 3854 |
. . . . . . 7
⊢
(〈𝑏, 𝑎〉 ∈ V →
(〈𝑏, 𝑎〉 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 〈𝑏, 𝑎〉 ∈ 𝐵)) |
21 | 19, 20 | ax-mp 5 |
. . . . . 6
⊢
(〈𝑏, 𝑎〉 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 〈𝑏, 𝑎〉 ∈ 𝐵) |
22 | 18, 17 | opelcnv 4768 |
. . . . . 6
⊢
(〈𝑎, 𝑏〉 ∈ ◡∩ 𝑥 ∈ 𝐴 𝐵 ↔ 〈𝑏, 𝑎〉 ∈ ∩ 𝑥 ∈ 𝐴 𝐵) |
23 | 18, 17 | opex 4189 |
. . . . . . . 8
⊢
〈𝑎, 𝑏〉 ∈ V |
24 | | eliin 3854 |
. . . . . . . 8
⊢
(〈𝑎, 𝑏〉 ∈ V →
(〈𝑎, 𝑏〉 ∈ ∩ 𝑥 ∈ 𝐴 ◡𝐵 ↔ ∀𝑥 ∈ 𝐴 〈𝑎, 𝑏〉 ∈ ◡𝐵)) |
25 | 23, 24 | ax-mp 5 |
. . . . . . 7
⊢
(〈𝑎, 𝑏〉 ∈ ∩ 𝑥 ∈ 𝐴 ◡𝐵 ↔ ∀𝑥 ∈ 𝐴 〈𝑎, 𝑏〉 ∈ ◡𝐵) |
26 | 18, 17 | opelcnv 4768 |
. . . . . . . 8
⊢
(〈𝑎, 𝑏〉 ∈ ◡𝐵 ↔ 〈𝑏, 𝑎〉 ∈ 𝐵) |
27 | 26 | ralbii 2463 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 〈𝑎, 𝑏〉 ∈ ◡𝐵 ↔ ∀𝑥 ∈ 𝐴 〈𝑏, 𝑎〉 ∈ 𝐵) |
28 | 25, 27 | bitri 183 |
. . . . . 6
⊢
(〈𝑎, 𝑏〉 ∈ ∩ 𝑥 ∈ 𝐴 ◡𝐵 ↔ ∀𝑥 ∈ 𝐴 〈𝑏, 𝑎〉 ∈ 𝐵) |
29 | 21, 22, 28 | 3bitr4i 211 |
. . . . 5
⊢
(〈𝑎, 𝑏〉 ∈ ◡∩ 𝑥 ∈ 𝐴 𝐵 ↔ 〈𝑎, 𝑏〉 ∈ ∩ 𝑥 ∈ 𝐴 ◡𝐵) |
30 | 29 | eqrelriv 4679 |
. . . 4
⊢ ((Rel
◡∩
𝑥 ∈ 𝐴 𝐵 ∧ Rel ∩ 𝑥 ∈ 𝐴 ◡𝐵) → ◡∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 ◡𝐵) |
31 | 5, 16, 30 | sylancr 411 |
. . 3
⊢
(∃𝑥 𝑥 ∈ 𝐴 → ◡∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 ◡𝐵) |
32 | 4, 31 | sylbir 134 |
. 2
⊢
(∃𝑎 𝑎 ∈ 𝐴 → ◡∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 ◡𝐵) |
33 | 2, 32 | sylbi 120 |
1
⊢
(∃𝑦 𝑦 ∈ 𝐴 → ◡∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 ◡𝐵) |