Step | Hyp | Ref
| Expression |
1 | | eleq1 2097 |
. . 3
⊢ (y = 𝑎 → (y ∈ A ↔ 𝑎 ∈ A)) |
2 | 1 | cbvexv 1792 |
. 2
⊢ (∃y y ∈ A ↔ ∃𝑎 𝑎 ∈ A) |
3 | | eleq1 2097 |
. . . 4
⊢ (x = 𝑎 → (x ∈ A ↔ 𝑎 ∈ A)) |
4 | 3 | cbvexv 1792 |
. . 3
⊢ (∃x x ∈ A ↔ ∃𝑎 𝑎 ∈ A) |
5 | | relcnv 4646 |
. . . 4
⊢ Rel ◡∩ x ∈ A B |
6 | | r19.2m 3303 |
. . . . . . . 8
⊢ ((∃x x ∈ A ∧ ∀x ∈ A ◡B
⊆ (V × V)) → ∃x ∈ A ◡B ⊆ (V × V)) |
7 | 6 | expcom 109 |
. . . . . . 7
⊢ (∀x ∈ A ◡B
⊆ (V × V) → (∃x x ∈ A →
∃x ∈ A ◡B
⊆ (V × V))) |
8 | | relcnv 4646 |
. . . . . . . . 9
⊢ Rel ◡B |
9 | | df-rel 4295 |
. . . . . . . . 9
⊢ (Rel
◡B
↔ ◡B ⊆ (V × V)) |
10 | 8, 9 | mpbi 133 |
. . . . . . . 8
⊢ ◡B
⊆ (V × V) |
11 | 10 | a1i 9 |
. . . . . . 7
⊢ (x ∈ A → ◡B
⊆ (V × V)) |
12 | 7, 11 | mprg 2372 |
. . . . . 6
⊢ (∃x x ∈ A → ∃x ∈ A ◡B
⊆ (V × V)) |
13 | | iinss 3699 |
. . . . . 6
⊢ (∃x ∈ A ◡B
⊆ (V × V) → ∩ x ∈ A ◡B ⊆ (V × V)) |
14 | 12, 13 | syl 14 |
. . . . 5
⊢ (∃x x ∈ A → ∩
x ∈
A ◡B
⊆ (V × V)) |
15 | | df-rel 4295 |
. . . . 5
⊢ (Rel
∩ x ∈ A ◡B ↔
∩ x ∈ A ◡B
⊆ (V × V)) |
16 | 14, 15 | sylibr 137 |
. . . 4
⊢ (∃x x ∈ A → Rel ∩
x ∈
A ◡B) |
17 | | vex 2554 |
. . . . . . . 8
⊢ 𝑏 ∈ V |
18 | | vex 2554 |
. . . . . . . 8
⊢ 𝑎 ∈ V |
19 | 17, 18 | opex 3957 |
. . . . . . 7
⊢
〈𝑏, 𝑎〉 ∈ V |
20 | | eliin 3653 |
. . . . . . 7
⊢
(〈𝑏, 𝑎〉 ∈ V → (〈𝑏, 𝑎〉 ∈
∩ x ∈ A B ↔ ∀x ∈ A 〈𝑏, 𝑎〉 ∈
B)) |
21 | 19, 20 | ax-mp 7 |
. . . . . 6
⊢
(〈𝑏, 𝑎〉 ∈ ∩ x ∈ A B ↔ ∀x ∈ A 〈𝑏, 𝑎〉 ∈
B) |
22 | 18, 17 | opelcnv 4460 |
. . . . . 6
⊢
(〈𝑎, 𝑏〉 ∈ ◡∩ x ∈ A B ↔ 〈𝑏, 𝑎〉 ∈
∩ x ∈ A B) |
23 | 18, 17 | opex 3957 |
. . . . . . . 8
⊢
〈𝑎, 𝑏〉 ∈ V |
24 | | eliin 3653 |
. . . . . . . 8
⊢
(〈𝑎, 𝑏〉 ∈ V → (〈𝑎, 𝑏〉 ∈
∩ x ∈ A ◡B ↔
∀x
∈ A
〈𝑎, 𝑏〉 ∈
◡B)) |
25 | 23, 24 | ax-mp 7 |
. . . . . . 7
⊢
(〈𝑎, 𝑏〉 ∈ ∩ x ∈ A ◡B ↔ ∀x ∈ A 〈𝑎, 𝑏〉 ∈
◡B) |
26 | 18, 17 | opelcnv 4460 |
. . . . . . . 8
⊢
(〈𝑎, 𝑏〉 ∈ ◡B ↔ 〈𝑏, 𝑎〉 ∈
B) |
27 | 26 | ralbii 2324 |
. . . . . . 7
⊢ (∀x ∈ A 〈𝑎, 𝑏〉 ∈
◡B
↔ ∀x ∈ A 〈𝑏, 𝑎〉 ∈
B) |
28 | 25, 27 | bitri 173 |
. . . . . 6
⊢
(〈𝑎, 𝑏〉 ∈ ∩ x ∈ A ◡B ↔ ∀x ∈ A 〈𝑏, 𝑎〉 ∈
B) |
29 | 21, 22, 28 | 3bitr4i 201 |
. . . . 5
⊢
(〈𝑎, 𝑏〉 ∈ ◡∩ x ∈ A B ↔ 〈𝑎, 𝑏〉 ∈
∩ x ∈ A ◡B) |
30 | 29 | eqrelriv 4376 |
. . . 4
⊢ ((Rel
◡∩
x ∈
A B
∧ Rel ∩
x ∈
A ◡B)
→ ◡∩ x ∈ A B = ∩ x ∈ A ◡B) |
31 | 5, 16, 30 | sylancr 393 |
. . 3
⊢ (∃x x ∈ A → ◡∩ x ∈ A B = ∩ x ∈ A ◡B) |
32 | 4, 31 | sylbir 125 |
. 2
⊢ (∃𝑎 𝑎 ∈ A → ◡∩ x ∈ A B = ∩ x ∈ A ◡B) |
33 | 2, 32 | sylbi 114 |
1
⊢ (∃y y ∈ A → ◡∩ x ∈ A B = ∩ x ∈ A ◡B) |