Step | Hyp | Ref
| Expression |
1 | | pwexg 5271 |
. . . 4
⊢ (𝑌 ∈ 𝑉 → 𝒫 𝑌 ∈ V) |
2 | | elrest 16932 |
. . . 4
⊢
((𝒫 𝑌 ∈
V ∧ 𝐴 ∈ 𝑊) → (𝑥 ∈ (𝒫 𝑌 ↾t 𝐴) ↔ ∃𝑦 ∈ 𝒫 𝑌𝑥 = (𝑦 ∩ 𝐴))) |
3 | 1, 2 | sylan 583 |
. . 3
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑥 ∈ (𝒫 𝑌 ↾t 𝐴) ↔ ∃𝑦 ∈ 𝒫 𝑌𝑥 = (𝑦 ∩ 𝐴))) |
4 | | velpw 4518 |
. . . . . . 7
⊢ (𝑦 ∈ 𝒫 𝑌 ↔ 𝑦 ⊆ 𝑌) |
5 | 4 | anbi1i 627 |
. . . . . 6
⊢ ((𝑦 ∈ 𝒫 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴)) ↔ (𝑦 ⊆ 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴))) |
6 | 5 | exbii 1855 |
. . . . 5
⊢
(∃𝑦(𝑦 ∈ 𝒫 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴)) ↔ ∃𝑦(𝑦 ⊆ 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴))) |
7 | | sstr2 3908 |
. . . . . . . . . 10
⊢ (𝑥 ⊆ 𝑦 → (𝑦 ⊆ 𝑌 → 𝑥 ⊆ 𝑌)) |
8 | 7 | com12 32 |
. . . . . . . . 9
⊢ (𝑦 ⊆ 𝑌 → (𝑥 ⊆ 𝑦 → 𝑥 ⊆ 𝑌)) |
9 | | inss1 4143 |
. . . . . . . . . 10
⊢ (𝑦 ∩ 𝐴) ⊆ 𝑦 |
10 | | sseq1 3926 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑦 ∩ 𝐴) → (𝑥 ⊆ 𝑦 ↔ (𝑦 ∩ 𝐴) ⊆ 𝑦)) |
11 | 9, 10 | mpbiri 261 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 ∩ 𝐴) → 𝑥 ⊆ 𝑦) |
12 | 8, 11 | impel 509 |
. . . . . . . 8
⊢ ((𝑦 ⊆ 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴)) → 𝑥 ⊆ 𝑌) |
13 | | inss2 4144 |
. . . . . . . . . 10
⊢ (𝑦 ∩ 𝐴) ⊆ 𝐴 |
14 | | sseq1 3926 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑦 ∩ 𝐴) → (𝑥 ⊆ 𝐴 ↔ (𝑦 ∩ 𝐴) ⊆ 𝐴)) |
15 | 13, 14 | mpbiri 261 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 ∩ 𝐴) → 𝑥 ⊆ 𝐴) |
16 | 15 | adantl 485 |
. . . . . . . 8
⊢ ((𝑦 ⊆ 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴)) → 𝑥 ⊆ 𝐴) |
17 | 12, 16 | ssind 4147 |
. . . . . . 7
⊢ ((𝑦 ⊆ 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴)) → 𝑥 ⊆ (𝑌 ∩ 𝐴)) |
18 | 17 | exlimiv 1938 |
. . . . . 6
⊢
(∃𝑦(𝑦 ⊆ 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴)) → 𝑥 ⊆ (𝑌 ∩ 𝐴)) |
19 | | inss1 4143 |
. . . . . . . 8
⊢ (𝑌 ∩ 𝐴) ⊆ 𝑌 |
20 | | sstr2 3908 |
. . . . . . . 8
⊢ (𝑥 ⊆ (𝑌 ∩ 𝐴) → ((𝑌 ∩ 𝐴) ⊆ 𝑌 → 𝑥 ⊆ 𝑌)) |
21 | 19, 20 | mpi 20 |
. . . . . . 7
⊢ (𝑥 ⊆ (𝑌 ∩ 𝐴) → 𝑥 ⊆ 𝑌) |
22 | | inss2 4144 |
. . . . . . . 8
⊢ (𝑌 ∩ 𝐴) ⊆ 𝐴 |
23 | | sstr2 3908 |
. . . . . . . 8
⊢ (𝑥 ⊆ (𝑌 ∩ 𝐴) → ((𝑌 ∩ 𝐴) ⊆ 𝐴 → 𝑥 ⊆ 𝐴)) |
24 | 22, 23 | mpi 20 |
. . . . . . 7
⊢ (𝑥 ⊆ (𝑌 ∩ 𝐴) → 𝑥 ⊆ 𝐴) |
25 | | ssidd 3924 |
. . . . . . . . . 10
⊢ (𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝑥) |
26 | | id 22 |
. . . . . . . . . 10
⊢ (𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐴) |
27 | 25, 26 | ssind 4147 |
. . . . . . . . 9
⊢ (𝑥 ⊆ 𝐴 → 𝑥 ⊆ (𝑥 ∩ 𝐴)) |
28 | | inss1 4143 |
. . . . . . . . . 10
⊢ (𝑥 ∩ 𝐴) ⊆ 𝑥 |
29 | 28 | a1i 11 |
. . . . . . . . 9
⊢ (𝑥 ⊆ 𝐴 → (𝑥 ∩ 𝐴) ⊆ 𝑥) |
30 | 27, 29 | eqssd 3918 |
. . . . . . . 8
⊢ (𝑥 ⊆ 𝐴 → 𝑥 = (𝑥 ∩ 𝐴)) |
31 | | vex 3412 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
32 | | sseq1 3926 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (𝑦 ⊆ 𝑌 ↔ 𝑥 ⊆ 𝑌)) |
33 | | ineq1 4120 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (𝑦 ∩ 𝐴) = (𝑥 ∩ 𝐴)) |
34 | 33 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (𝑥 = (𝑦 ∩ 𝐴) ↔ 𝑥 = (𝑥 ∩ 𝐴))) |
35 | 32, 34 | anbi12d 634 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → ((𝑦 ⊆ 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴)) ↔ (𝑥 ⊆ 𝑌 ∧ 𝑥 = (𝑥 ∩ 𝐴)))) |
36 | 31, 35 | spcev 3521 |
. . . . . . . 8
⊢ ((𝑥 ⊆ 𝑌 ∧ 𝑥 = (𝑥 ∩ 𝐴)) → ∃𝑦(𝑦 ⊆ 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴))) |
37 | 30, 36 | sylan2 596 |
. . . . . . 7
⊢ ((𝑥 ⊆ 𝑌 ∧ 𝑥 ⊆ 𝐴) → ∃𝑦(𝑦 ⊆ 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴))) |
38 | 21, 24, 37 | syl2anc 587 |
. . . . . 6
⊢ (𝑥 ⊆ (𝑌 ∩ 𝐴) → ∃𝑦(𝑦 ⊆ 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴))) |
39 | 18, 38 | impbii 212 |
. . . . 5
⊢
(∃𝑦(𝑦 ⊆ 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴)) ↔ 𝑥 ⊆ (𝑌 ∩ 𝐴)) |
40 | 6, 39 | bitri 278 |
. . . 4
⊢
(∃𝑦(𝑦 ∈ 𝒫 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴)) ↔ 𝑥 ⊆ (𝑌 ∩ 𝐴)) |
41 | | df-rex 3067 |
. . . 4
⊢
(∃𝑦 ∈
𝒫 𝑌𝑥 = (𝑦 ∩ 𝐴) ↔ ∃𝑦(𝑦 ∈ 𝒫 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴))) |
42 | | velpw 4518 |
. . . 4
⊢ (𝑥 ∈ 𝒫 (𝑌 ∩ 𝐴) ↔ 𝑥 ⊆ (𝑌 ∩ 𝐴)) |
43 | 40, 41, 42 | 3bitr4i 306 |
. . 3
⊢
(∃𝑦 ∈
𝒫 𝑌𝑥 = (𝑦 ∩ 𝐴) ↔ 𝑥 ∈ 𝒫 (𝑌 ∩ 𝐴)) |
44 | 3, 43 | bitrdi 290 |
. 2
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑥 ∈ (𝒫 𝑌 ↾t 𝐴) ↔ 𝑥 ∈ 𝒫 (𝑌 ∩ 𝐴))) |
45 | 44 | eqrdv 2735 |
1
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝒫 𝑌 ↾t 𝐴) = 𝒫 (𝑌 ∩ 𝐴)) |