Step | Hyp | Ref
| Expression |
1 | | pwexg 5301 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) |
2 | 1 | adantr 481 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → 𝒫 𝐴 ∈ V) |
3 | | inex1g 5243 |
. . . . 5
⊢
(𝒫 𝐴 ∈
V → (𝒫 𝐴 ∩
Fin) ∈ V) |
4 | 2, 3 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → (𝒫 𝐴 ∩ Fin) ∈ V) |
5 | | ssexg 5247 |
. . . . 5
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐵 ∈ V) |
6 | 5 | ancoms 459 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ V) |
7 | | restval 17137 |
. . . 4
⊢
(((𝒫 𝐴 ∩
Fin) ∈ V ∧ 𝐵
∈ V) → ((𝒫 𝐴 ∩ Fin) ↾t 𝐵) = ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝑥 ∩ 𝐵))) |
8 | 4, 6, 7 | syl2anc 584 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → ((𝒫 𝐴 ∩ Fin) ↾t 𝐵) = ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝑥 ∩ 𝐵))) |
9 | | inss2 4163 |
. . . . . . 7
⊢ (𝑥 ∩ 𝐵) ⊆ 𝐵 |
10 | 9 | a1i 11 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑥 ∩ 𝐵) ⊆ 𝐵) |
11 | | elinel2 4130 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ∈ Fin) |
12 | 11 | adantl 482 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ∈ Fin) |
13 | | inss1 4162 |
. . . . . . 7
⊢ (𝑥 ∩ 𝐵) ⊆ 𝑥 |
14 | | ssfi 8956 |
. . . . . . 7
⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ 𝐵) ⊆ 𝑥) → (𝑥 ∩ 𝐵) ∈ Fin) |
15 | 12, 13, 14 | sylancl 586 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑥 ∩ 𝐵) ∈ Fin) |
16 | | elfpw 9121 |
. . . . . 6
⊢ ((𝑥 ∩ 𝐵) ∈ (𝒫 𝐵 ∩ Fin) ↔ ((𝑥 ∩ 𝐵) ⊆ 𝐵 ∧ (𝑥 ∩ 𝐵) ∈ Fin)) |
17 | 10, 15, 16 | sylanbrc 583 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑥 ∩ 𝐵) ∈ (𝒫 𝐵 ∩ Fin)) |
18 | 17 | fmpttd 6989 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝑥 ∩ 𝐵)):(𝒫 𝐴 ∩ Fin)⟶(𝒫 𝐵 ∩ Fin)) |
19 | 18 | frnd 6608 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝑥 ∩ 𝐵)) ⊆ (𝒫 𝐵 ∩ Fin)) |
20 | 8, 19 | eqsstrd 3959 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → ((𝒫 𝐴 ∩ Fin) ↾t 𝐵) ⊆ (𝒫 𝐵 ∩ Fin)) |
21 | | elfpw 9121 |
. . . . . 6
⊢ (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝑥 ⊆ 𝐵 ∧ 𝑥 ∈ Fin)) |
22 | 21 | simplbi 498 |
. . . . 5
⊢ (𝑥 ∈ (𝒫 𝐵 ∩ Fin) → 𝑥 ⊆ 𝐵) |
23 | 22 | adantl 482 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑥 ⊆ 𝐵) |
24 | | df-ss 3904 |
. . . 4
⊢ (𝑥 ⊆ 𝐵 ↔ (𝑥 ∩ 𝐵) = 𝑥) |
25 | 23, 24 | sylib 217 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → (𝑥 ∩ 𝐵) = 𝑥) |
26 | 4 | adantr 481 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → (𝒫 𝐴 ∩ Fin) ∈
V) |
27 | 6 | adantr 481 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝐵 ∈ V) |
28 | | simplr 766 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝐵 ⊆ 𝐴) |
29 | 23, 28 | sstrd 3931 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑥 ⊆ 𝐴) |
30 | | elinel2 4130 |
. . . . . 6
⊢ (𝑥 ∈ (𝒫 𝐵 ∩ Fin) → 𝑥 ∈ Fin) |
31 | 30 | adantl 482 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑥 ∈ Fin) |
32 | | elfpw 9121 |
. . . . 5
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 ∈ Fin)) |
33 | 29, 31, 32 | sylanbrc 583 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) |
34 | | elrestr 17139 |
. . . 4
⊢
(((𝒫 𝐴 ∩
Fin) ∈ V ∧ 𝐵
∈ V ∧ 𝑥 ∈
(𝒫 𝐴 ∩ Fin))
→ (𝑥 ∩ 𝐵) ∈ ((𝒫 𝐴 ∩ Fin) ↾t
𝐵)) |
35 | 26, 27, 33, 34 | syl3anc 1370 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → (𝑥 ∩ 𝐵) ∈ ((𝒫 𝐴 ∩ Fin) ↾t 𝐵)) |
36 | 25, 35 | eqeltrrd 2840 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑥 ∈ ((𝒫 𝐴 ∩ Fin) ↾t 𝐵)) |
37 | 20, 36 | eqelssd 3942 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → ((𝒫 𝐴 ∩ Fin) ↾t 𝐵) = (𝒫 𝐵 ∩ Fin)) |