Step | Hyp | Ref
| Expression |
1 | | eleq1 2141 |
. . 3
⊢ (𝑦 = 𝑎 → (𝑦 ∈ 𝐴 ↔ 𝑎 ∈ 𝐴)) |
2 | 1 | cbvexv 1836 |
. 2
⊢
(∃𝑦 𝑦 ∈ 𝐴 ↔ ∃𝑎 𝑎 ∈ 𝐴) |
3 | | eleq1 2141 |
. . . 4
⊢ (𝑥 = 𝑎 → (𝑥 ∈ 𝐴 ↔ 𝑎 ∈ 𝐴)) |
4 | 3 | cbvexv 1836 |
. . 3
⊢
(∃𝑥 𝑥 ∈ 𝐴 ↔ ∃𝑎 𝑎 ∈ 𝐴) |
5 | | relcnv 4723 |
. . . 4
⊢ Rel ◡∩ 𝑥 ∈ 𝐴 𝐵 |
6 | | r19.2m 3329 |
. . . . . . . 8
⊢
((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ◡𝐵 ⊆ (V × V)) → ∃𝑥 ∈ 𝐴 ◡𝐵 ⊆ (V × V)) |
7 | 6 | expcom 114 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 ◡𝐵 ⊆ (V × V) → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 ◡𝐵 ⊆ (V × V))) |
8 | | relcnv 4723 |
. . . . . . . . 9
⊢ Rel ◡𝐵 |
9 | | df-rel 4370 |
. . . . . . . . 9
⊢ (Rel
◡𝐵 ↔ ◡𝐵 ⊆ (V × V)) |
10 | 8, 9 | mpbi 143 |
. . . . . . . 8
⊢ ◡𝐵 ⊆ (V × V) |
11 | 10 | a1i 9 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → ◡𝐵 ⊆ (V × V)) |
12 | 7, 11 | mprg 2420 |
. . . . . 6
⊢
(∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 ◡𝐵 ⊆ (V × V)) |
13 | | iinss 3729 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐴 ◡𝐵 ⊆ (V × V) → ∩ 𝑥 ∈ 𝐴 ◡𝐵 ⊆ (V × V)) |
14 | 12, 13 | syl 14 |
. . . . 5
⊢
(∃𝑥 𝑥 ∈ 𝐴 → ∩
𝑥 ∈ 𝐴 ◡𝐵 ⊆ (V × V)) |
15 | | df-rel 4370 |
. . . . 5
⊢ (Rel
∩ 𝑥 ∈ 𝐴 ◡𝐵 ↔ ∩
𝑥 ∈ 𝐴 ◡𝐵 ⊆ (V × V)) |
16 | 14, 15 | sylibr 132 |
. . . 4
⊢
(∃𝑥 𝑥 ∈ 𝐴 → Rel ∩ 𝑥 ∈ 𝐴 ◡𝐵) |
17 | | vex 2604 |
. . . . . . . 8
⊢ 𝑏 ∈ V |
18 | | vex 2604 |
. . . . . . . 8
⊢ 𝑎 ∈ V |
19 | 17, 18 | opex 3984 |
. . . . . . 7
⊢
〈𝑏, 𝑎〉 ∈ V |
20 | | eliin 3683 |
. . . . . . 7
⊢
(〈𝑏, 𝑎〉 ∈ V →
(〈𝑏, 𝑎〉 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 〈𝑏, 𝑎〉 ∈ 𝐵)) |
21 | 19, 20 | ax-mp 7 |
. . . . . 6
⊢
(〈𝑏, 𝑎〉 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 〈𝑏, 𝑎〉 ∈ 𝐵) |
22 | 18, 17 | opelcnv 4535 |
. . . . . 6
⊢
(〈𝑎, 𝑏〉 ∈ ◡∩ 𝑥 ∈ 𝐴 𝐵 ↔ 〈𝑏, 𝑎〉 ∈ ∩ 𝑥 ∈ 𝐴 𝐵) |
23 | 18, 17 | opex 3984 |
. . . . . . . 8
⊢
〈𝑎, 𝑏〉 ∈ V |
24 | | eliin 3683 |
. . . . . . . 8
⊢
(〈𝑎, 𝑏〉 ∈ V →
(〈𝑎, 𝑏〉 ∈ ∩ 𝑥 ∈ 𝐴 ◡𝐵 ↔ ∀𝑥 ∈ 𝐴 〈𝑎, 𝑏〉 ∈ ◡𝐵)) |
25 | 23, 24 | ax-mp 7 |
. . . . . . 7
⊢
(〈𝑎, 𝑏〉 ∈ ∩ 𝑥 ∈ 𝐴 ◡𝐵 ↔ ∀𝑥 ∈ 𝐴 〈𝑎, 𝑏〉 ∈ ◡𝐵) |
26 | 18, 17 | opelcnv 4535 |
. . . . . . . 8
⊢
(〈𝑎, 𝑏〉 ∈ ◡𝐵 ↔ 〈𝑏, 𝑎〉 ∈ 𝐵) |
27 | 26 | ralbii 2372 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 〈𝑎, 𝑏〉 ∈ ◡𝐵 ↔ ∀𝑥 ∈ 𝐴 〈𝑏, 𝑎〉 ∈ 𝐵) |
28 | 25, 27 | bitri 182 |
. . . . . 6
⊢
(〈𝑎, 𝑏〉 ∈ ∩ 𝑥 ∈ 𝐴 ◡𝐵 ↔ ∀𝑥 ∈ 𝐴 〈𝑏, 𝑎〉 ∈ 𝐵) |
29 | 21, 22, 28 | 3bitr4i 210 |
. . . . 5
⊢
(〈𝑎, 𝑏〉 ∈ ◡∩ 𝑥 ∈ 𝐴 𝐵 ↔ 〈𝑎, 𝑏〉 ∈ ∩ 𝑥 ∈ 𝐴 ◡𝐵) |
30 | 29 | eqrelriv 4451 |
. . . 4
⊢ ((Rel
◡∩
𝑥 ∈ 𝐴 𝐵 ∧ Rel ∩ 𝑥 ∈ 𝐴 ◡𝐵) → ◡∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 ◡𝐵) |
31 | 5, 16, 30 | sylancr 405 |
. . 3
⊢
(∃𝑥 𝑥 ∈ 𝐴 → ◡∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 ◡𝐵) |
32 | 4, 31 | sylbir 133 |
. 2
⊢
(∃𝑎 𝑎 ∈ 𝐴 → ◡∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 ◡𝐵) |
33 | 2, 32 | sylbi 119 |
1
⊢
(∃𝑦 𝑦 ∈ 𝐴 → ◡∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 ◡𝐵) |