Step | Hyp | Ref
| Expression |
1 | | pwexg 4776 |
. . . 4
⊢ (𝑌 ∈ 𝑉 → 𝒫 𝑌 ∈ V) |
2 | | elrest 15911 |
. . . 4
⊢
((𝒫 𝑌 ∈
V ∧ 𝐴 ∈ 𝑊) → (𝑥 ∈ (𝒫 𝑌 ↾t 𝐴) ↔ ∃𝑦 ∈ 𝒫 𝑌𝑥 = (𝑦 ∩ 𝐴))) |
3 | 1, 2 | sylan 487 |
. . 3
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑥 ∈ (𝒫 𝑌 ↾t 𝐴) ↔ ∃𝑦 ∈ 𝒫 𝑌𝑥 = (𝑦 ∩ 𝐴))) |
4 | | selpw 4115 |
. . . . . . 7
⊢ (𝑦 ∈ 𝒫 𝑌 ↔ 𝑦 ⊆ 𝑌) |
5 | 4 | anbi1i 727 |
. . . . . 6
⊢ ((𝑦 ∈ 𝒫 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴)) ↔ (𝑦 ⊆ 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴))) |
6 | 5 | exbii 1764 |
. . . . 5
⊢
(∃𝑦(𝑦 ∈ 𝒫 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴)) ↔ ∃𝑦(𝑦 ⊆ 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴))) |
7 | | sstr2 3575 |
. . . . . . . . . 10
⊢ (𝑥 ⊆ 𝑦 → (𝑦 ⊆ 𝑌 → 𝑥 ⊆ 𝑌)) |
8 | 7 | com12 32 |
. . . . . . . . 9
⊢ (𝑦 ⊆ 𝑌 → (𝑥 ⊆ 𝑦 → 𝑥 ⊆ 𝑌)) |
9 | | inss1 3795 |
. . . . . . . . . 10
⊢ (𝑦 ∩ 𝐴) ⊆ 𝑦 |
10 | | sseq1 3589 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑦 ∩ 𝐴) → (𝑥 ⊆ 𝑦 ↔ (𝑦 ∩ 𝐴) ⊆ 𝑦)) |
11 | 9, 10 | mpbiri 247 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 ∩ 𝐴) → 𝑥 ⊆ 𝑦) |
12 | 8, 11 | impel 484 |
. . . . . . . 8
⊢ ((𝑦 ⊆ 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴)) → 𝑥 ⊆ 𝑌) |
13 | | inss2 3796 |
. . . . . . . . . 10
⊢ (𝑦 ∩ 𝐴) ⊆ 𝐴 |
14 | | sseq1 3589 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑦 ∩ 𝐴) → (𝑥 ⊆ 𝐴 ↔ (𝑦 ∩ 𝐴) ⊆ 𝐴)) |
15 | 13, 14 | mpbiri 247 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 ∩ 𝐴) → 𝑥 ⊆ 𝐴) |
16 | 15 | adantl 481 |
. . . . . . . 8
⊢ ((𝑦 ⊆ 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴)) → 𝑥 ⊆ 𝐴) |
17 | 12, 16 | ssind 3799 |
. . . . . . 7
⊢ ((𝑦 ⊆ 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴)) → 𝑥 ⊆ (𝑌 ∩ 𝐴)) |
18 | 17 | exlimiv 1845 |
. . . . . 6
⊢
(∃𝑦(𝑦 ⊆ 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴)) → 𝑥 ⊆ (𝑌 ∩ 𝐴)) |
19 | | inss1 3795 |
. . . . . . . 8
⊢ (𝑌 ∩ 𝐴) ⊆ 𝑌 |
20 | | sstr2 3575 |
. . . . . . . 8
⊢ (𝑥 ⊆ (𝑌 ∩ 𝐴) → ((𝑌 ∩ 𝐴) ⊆ 𝑌 → 𝑥 ⊆ 𝑌)) |
21 | 19, 20 | mpi 20 |
. . . . . . 7
⊢ (𝑥 ⊆ (𝑌 ∩ 𝐴) → 𝑥 ⊆ 𝑌) |
22 | | inss2 3796 |
. . . . . . . 8
⊢ (𝑌 ∩ 𝐴) ⊆ 𝐴 |
23 | | sstr2 3575 |
. . . . . . . 8
⊢ (𝑥 ⊆ (𝑌 ∩ 𝐴) → ((𝑌 ∩ 𝐴) ⊆ 𝐴 → 𝑥 ⊆ 𝐴)) |
24 | 22, 23 | mpi 20 |
. . . . . . 7
⊢ (𝑥 ⊆ (𝑌 ∩ 𝐴) → 𝑥 ⊆ 𝐴) |
25 | | ssid 3587 |
. . . . . . . . . . 11
⊢ 𝑥 ⊆ 𝑥 |
26 | 25 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝑥) |
27 | | id 22 |
. . . . . . . . . 10
⊢ (𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐴) |
28 | 26, 27 | ssind 3799 |
. . . . . . . . 9
⊢ (𝑥 ⊆ 𝐴 → 𝑥 ⊆ (𝑥 ∩ 𝐴)) |
29 | | inss1 3795 |
. . . . . . . . . 10
⊢ (𝑥 ∩ 𝐴) ⊆ 𝑥 |
30 | 29 | a1i 11 |
. . . . . . . . 9
⊢ (𝑥 ⊆ 𝐴 → (𝑥 ∩ 𝐴) ⊆ 𝑥) |
31 | 28, 30 | eqssd 3585 |
. . . . . . . 8
⊢ (𝑥 ⊆ 𝐴 → 𝑥 = (𝑥 ∩ 𝐴)) |
32 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
33 | | sseq1 3589 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (𝑦 ⊆ 𝑌 ↔ 𝑥 ⊆ 𝑌)) |
34 | | ineq1 3769 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (𝑦 ∩ 𝐴) = (𝑥 ∩ 𝐴)) |
35 | 34 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (𝑥 = (𝑦 ∩ 𝐴) ↔ 𝑥 = (𝑥 ∩ 𝐴))) |
36 | 33, 35 | anbi12d 743 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → ((𝑦 ⊆ 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴)) ↔ (𝑥 ⊆ 𝑌 ∧ 𝑥 = (𝑥 ∩ 𝐴)))) |
37 | 32, 36 | spcev 3273 |
. . . . . . . 8
⊢ ((𝑥 ⊆ 𝑌 ∧ 𝑥 = (𝑥 ∩ 𝐴)) → ∃𝑦(𝑦 ⊆ 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴))) |
38 | 31, 37 | sylan2 490 |
. . . . . . 7
⊢ ((𝑥 ⊆ 𝑌 ∧ 𝑥 ⊆ 𝐴) → ∃𝑦(𝑦 ⊆ 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴))) |
39 | 21, 24, 38 | syl2anc 691 |
. . . . . 6
⊢ (𝑥 ⊆ (𝑌 ∩ 𝐴) → ∃𝑦(𝑦 ⊆ 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴))) |
40 | 18, 39 | impbii 198 |
. . . . 5
⊢
(∃𝑦(𝑦 ⊆ 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴)) ↔ 𝑥 ⊆ (𝑌 ∩ 𝐴)) |
41 | 6, 40 | bitri 263 |
. . . 4
⊢
(∃𝑦(𝑦 ∈ 𝒫 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴)) ↔ 𝑥 ⊆ (𝑌 ∩ 𝐴)) |
42 | | df-rex 2902 |
. . . 4
⊢
(∃𝑦 ∈
𝒫 𝑌𝑥 = (𝑦 ∩ 𝐴) ↔ ∃𝑦(𝑦 ∈ 𝒫 𝑌 ∧ 𝑥 = (𝑦 ∩ 𝐴))) |
43 | | selpw 4115 |
. . . 4
⊢ (𝑥 ∈ 𝒫 (𝑌 ∩ 𝐴) ↔ 𝑥 ⊆ (𝑌 ∩ 𝐴)) |
44 | 41, 42, 43 | 3bitr4i 291 |
. . 3
⊢
(∃𝑦 ∈
𝒫 𝑌𝑥 = (𝑦 ∩ 𝐴) ↔ 𝑥 ∈ 𝒫 (𝑌 ∩ 𝐴)) |
45 | 3, 44 | syl6bb 275 |
. 2
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑥 ∈ (𝒫 𝑌 ↾t 𝐴) ↔ 𝑥 ∈ 𝒫 (𝑌 ∩ 𝐴))) |
46 | 45 | eqrdv 2608 |
1
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝒫 𝑌 ↾t 𝐴) = 𝒫 (𝑌 ∩ 𝐴)) |