Step | Hyp | Ref
| Expression |
1 | | cnvcnv 5840 |
. . . . . . . . . 10
⊢ ◡◡𝑥 = (𝑥 ∩ (V × V)) |
2 | 1 | eleq2i 2851 |
. . . . . . . . 9
⊢ (𝑦 ∈ ◡◡𝑥 ↔ 𝑦 ∈ (𝑥 ∩ (V × V))) |
3 | | elin 4019 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝑥 ∩ (V × V)) ↔ (𝑦 ∈ 𝑥 ∧ 𝑦 ∈ (V × V))) |
4 | 3 | rbaib 534 |
. . . . . . . . 9
⊢ (𝑦 ∈ (V × V) →
(𝑦 ∈ (𝑥 ∩ (V × V)) ↔
𝑦 ∈ 𝑥)) |
5 | 2, 4 | syl5bb 275 |
. . . . . . . 8
⊢ (𝑦 ∈ (V × V) →
(𝑦 ∈ ◡◡𝑥 ↔ 𝑦 ∈ 𝑥)) |
6 | 5 | bicomd 215 |
. . . . . . 7
⊢ (𝑦 ∈ (V × V) →
(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ ◡◡𝑥)) |
7 | 6 | imbi2d 332 |
. . . . . 6
⊢ (𝑦 ∈ (V × V) →
((𝜓 → 𝑦 ∈ 𝑥) ↔ (𝜓 → 𝑦 ∈ ◡◡𝑥))) |
8 | 7 | albidv 1963 |
. . . . 5
⊢ (𝑦 ∈ (V × V) →
(∀𝑥(𝜓 → 𝑦 ∈ 𝑥) ↔ ∀𝑥(𝜓 → 𝑦 ∈ ◡◡𝑥))) |
9 | 8 | pm5.32i 570 |
. . . 4
⊢ ((𝑦 ∈ (V × V) ∧
∀𝑥(𝜓 → 𝑦 ∈ 𝑥)) ↔ (𝑦 ∈ (V × V) ∧ ∀𝑥(𝜓 → 𝑦 ∈ ◡◡𝑥))) |
10 | | cnvcnvintabd.x |
. . . . . . 7
⊢ (𝜑 → ∃𝑥𝜓) |
11 | | pm5.5 353 |
. . . . . . 7
⊢
(∃𝑥𝜓 → ((∃𝑥𝜓 → 𝑦 ∈ (V × V)) ↔ 𝑦 ∈ (V ×
V))) |
12 | 10, 11 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((∃𝑥𝜓 → 𝑦 ∈ (V × V)) ↔ 𝑦 ∈ (V ×
V))) |
13 | 12 | bicomd 215 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (V × V) ↔ (∃𝑥𝜓 → 𝑦 ∈ (V × V)))) |
14 | 13 | anbi1d 623 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ (V × V) ∧ ∀𝑥(𝜓 → 𝑦 ∈ ◡◡𝑥)) ↔ ((∃𝑥𝜓 → 𝑦 ∈ (V × V)) ∧ ∀𝑥(𝜓 → 𝑦 ∈ ◡◡𝑥)))) |
15 | 9, 14 | syl5bb 275 |
. . 3
⊢ (𝜑 → ((𝑦 ∈ (V × V) ∧ ∀𝑥(𝜓 → 𝑦 ∈ 𝑥)) ↔ ((∃𝑥𝜓 → 𝑦 ∈ (V × V)) ∧ ∀𝑥(𝜓 → 𝑦 ∈ ◡◡𝑥)))) |
16 | | elcnvcnvintab 38845 |
. . 3
⊢ (𝑦 ∈ ◡◡∩ {𝑥 ∣ 𝜓} ↔ (𝑦 ∈ (V × V) ∧ ∀𝑥(𝜓 → 𝑦 ∈ 𝑥))) |
17 | | vex 3401 |
. . . 4
⊢ 𝑦 ∈ V |
18 | | vex 3401 |
. . . . . 6
⊢ 𝑥 ∈ V |
19 | | cnvexg 7391 |
. . . . . 6
⊢ (𝑥 ∈ V → ◡𝑥 ∈ V) |
20 | | cnvexg 7391 |
. . . . . 6
⊢ (◡𝑥 ∈ V → ◡◡𝑥 ∈ V) |
21 | 18, 19, 20 | mp2b 10 |
. . . . 5
⊢ ◡◡𝑥 ∈ V |
22 | | relcnv 5757 |
. . . . . 6
⊢ Rel ◡◡𝑥 |
23 | | df-rel 5362 |
. . . . . 6
⊢ (Rel
◡◡𝑥 ↔ ◡◡𝑥 ⊆ (V × V)) |
24 | 22, 23 | mpbi 222 |
. . . . 5
⊢ ◡◡𝑥 ⊆ (V × V) |
25 | 21, 24 | elmapintrab 38839 |
. . . 4
⊢ (𝑦 ∈ V → (𝑦 ∈ ∩ {𝑤
∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜓)} ↔ ((∃𝑥𝜓 → 𝑦 ∈ (V × V)) ∧ ∀𝑥(𝜓 → 𝑦 ∈ ◡◡𝑥)))) |
26 | 17, 25 | ax-mp 5 |
. . 3
⊢ (𝑦 ∈ ∩ {𝑤
∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜓)} ↔ ((∃𝑥𝜓 → 𝑦 ∈ (V × V)) ∧ ∀𝑥(𝜓 → 𝑦 ∈ ◡◡𝑥))) |
27 | 15, 16, 26 | 3bitr4g 306 |
. 2
⊢ (𝜑 → (𝑦 ∈ ◡◡∩ {𝑥 ∣ 𝜓} ↔ 𝑦 ∈ ∩ {𝑤 ∈ 𝒫 (V × V)
∣ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜓)})) |
28 | 27 | eqrdv 2776 |
1
⊢ (𝜑 → ◡◡∩ {𝑥 ∣ 𝜓} = ∩ {𝑤 ∈ 𝒫 (V × V)
∣ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜓)}) |