Step | Hyp | Ref
| Expression |
1 | | relcnv 6057 |
. 2
⊢ Rel ◡∩ 𝑥 ∈ 𝐴 𝐵 |
2 | | relcnv 6057 |
. . . . . . 7
⊢ Rel ◡𝐵 |
3 | | df-rel 5641 |
. . . . . . 7
⊢ (Rel
◡𝐵 ↔ ◡𝐵 ⊆ (V × V)) |
4 | 2, 3 | mpbi 229 |
. . . . . 6
⊢ ◡𝐵 ⊆ (V × V) |
5 | 4 | rgenw 3065 |
. . . . 5
⊢
∀𝑥 ∈
𝐴 ◡𝐵 ⊆ (V × V) |
6 | | r19.2z 4453 |
. . . . 5
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 ◡𝐵 ⊆ (V × V)) → ∃𝑥 ∈ 𝐴 ◡𝐵 ⊆ (V × V)) |
7 | 5, 6 | mpan2 690 |
. . . 4
⊢ (𝐴 ≠ ∅ →
∃𝑥 ∈ 𝐴 ◡𝐵 ⊆ (V × V)) |
8 | | iinss 5017 |
. . . 4
⊢
(∃𝑥 ∈
𝐴 ◡𝐵 ⊆ (V × V) → ∩ 𝑥 ∈ 𝐴 ◡𝐵 ⊆ (V × V)) |
9 | 7, 8 | syl 17 |
. . 3
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 ◡𝐵 ⊆ (V × V)) |
10 | | df-rel 5641 |
. . 3
⊢ (Rel
∩ 𝑥 ∈ 𝐴 ◡𝐵 ↔ ∩
𝑥 ∈ 𝐴 ◡𝐵 ⊆ (V × V)) |
11 | 9, 10 | sylibr 233 |
. 2
⊢ (𝐴 ≠ ∅ → Rel
∩ 𝑥 ∈ 𝐴 ◡𝐵) |
12 | | opex 5422 |
. . . . 5
⊢
⟨𝑏, 𝑎⟩ ∈ V |
13 | | eliin 4960 |
. . . . 5
⊢
(⟨𝑏, 𝑎⟩ ∈ V →
(⟨𝑏, 𝑎⟩ ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 ⟨𝑏, 𝑎⟩ ∈ 𝐵)) |
14 | 12, 13 | ax-mp 5 |
. . . 4
⊢
(⟨𝑏, 𝑎⟩ ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 ⟨𝑏, 𝑎⟩ ∈ 𝐵) |
15 | | vex 3448 |
. . . . 5
⊢ 𝑎 ∈ V |
16 | | vex 3448 |
. . . . 5
⊢ 𝑏 ∈ V |
17 | 15, 16 | opelcnv 5838 |
. . . 4
⊢
(⟨𝑎, 𝑏⟩ ∈ ◡∩ 𝑥 ∈ 𝐴 𝐵 ↔ ⟨𝑏, 𝑎⟩ ∈ ∩ 𝑥 ∈ 𝐴 𝐵) |
18 | | opex 5422 |
. . . . . 6
⊢
⟨𝑎, 𝑏⟩ ∈ V |
19 | | eliin 4960 |
. . . . . 6
⊢
(⟨𝑎, 𝑏⟩ ∈ V →
(⟨𝑎, 𝑏⟩ ∈ ∩ 𝑥 ∈ 𝐴 ◡𝐵 ↔ ∀𝑥 ∈ 𝐴 ⟨𝑎, 𝑏⟩ ∈ ◡𝐵)) |
20 | 18, 19 | ax-mp 5 |
. . . . 5
⊢
(⟨𝑎, 𝑏⟩ ∈ ∩ 𝑥 ∈ 𝐴 ◡𝐵 ↔ ∀𝑥 ∈ 𝐴 ⟨𝑎, 𝑏⟩ ∈ ◡𝐵) |
21 | 15, 16 | opelcnv 5838 |
. . . . . 6
⊢
(⟨𝑎, 𝑏⟩ ∈ ◡𝐵 ↔ ⟨𝑏, 𝑎⟩ ∈ 𝐵) |
22 | 21 | ralbii 3093 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ⟨𝑎, 𝑏⟩ ∈ ◡𝐵 ↔ ∀𝑥 ∈ 𝐴 ⟨𝑏, 𝑎⟩ ∈ 𝐵) |
23 | 20, 22 | bitri 275 |
. . . 4
⊢
(⟨𝑎, 𝑏⟩ ∈ ∩ 𝑥 ∈ 𝐴 ◡𝐵 ↔ ∀𝑥 ∈ 𝐴 ⟨𝑏, 𝑎⟩ ∈ 𝐵) |
24 | 14, 17, 23 | 3bitr4i 303 |
. . 3
⊢
(⟨𝑎, 𝑏⟩ ∈ ◡∩ 𝑥 ∈ 𝐴 𝐵 ↔ ⟨𝑎, 𝑏⟩ ∈ ∩ 𝑥 ∈ 𝐴 ◡𝐵) |
25 | 24 | eqrelriv 5746 |
. 2
⊢ ((Rel
◡∩
𝑥 ∈ 𝐴 𝐵 ∧ Rel ∩ 𝑥 ∈ 𝐴 ◡𝐵) → ◡∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 ◡𝐵) |
26 | 1, 11, 25 | sylancr 588 |
1
⊢ (𝐴 ≠ ∅ → ◡∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 ◡𝐵) |