Step | Hyp | Ref
| Expression |
1 | | pwexg 4776 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) |
2 | 1 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → 𝒫 𝐴 ∈ V) |
3 | | inex1g 4729 |
. . . . 5
⊢
(𝒫 𝐴 ∈
V → (𝒫 𝐴 ∩
Fin) ∈ V) |
4 | 2, 3 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → (𝒫 𝐴 ∩ Fin) ∈ V) |
5 | | ssexg 4732 |
. . . . 5
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐵 ∈ V) |
6 | 5 | ancoms 468 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ V) |
7 | | restval 15910 |
. . . 4
⊢
(((𝒫 𝐴 ∩
Fin) ∈ V ∧ 𝐵
∈ V) → ((𝒫 𝐴 ∩ Fin) ↾t 𝐵) = ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝑥 ∩ 𝐵))) |
8 | 4, 6, 7 | syl2anc 691 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → ((𝒫 𝐴 ∩ Fin) ↾t 𝐵) = ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝑥 ∩ 𝐵))) |
9 | | inss2 3796 |
. . . . . . 7
⊢ (𝑥 ∩ 𝐵) ⊆ 𝐵 |
10 | 9 | a1i 11 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑥 ∩ 𝐵) ⊆ 𝐵) |
11 | | elfpw 8151 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 ∈ Fin)) |
12 | 11 | simprbi 479 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ∈ Fin) |
13 | 12 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ∈ Fin) |
14 | | inss1 3795 |
. . . . . . 7
⊢ (𝑥 ∩ 𝐵) ⊆ 𝑥 |
15 | | ssfi 8065 |
. . . . . . 7
⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ 𝐵) ⊆ 𝑥) → (𝑥 ∩ 𝐵) ∈ Fin) |
16 | 13, 14, 15 | sylancl 693 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑥 ∩ 𝐵) ∈ Fin) |
17 | | elfpw 8151 |
. . . . . 6
⊢ ((𝑥 ∩ 𝐵) ∈ (𝒫 𝐵 ∩ Fin) ↔ ((𝑥 ∩ 𝐵) ⊆ 𝐵 ∧ (𝑥 ∩ 𝐵) ∈ Fin)) |
18 | 10, 16, 17 | sylanbrc 695 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑥 ∩ 𝐵) ∈ (𝒫 𝐵 ∩ Fin)) |
19 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝑥 ∩ 𝐵)) = (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝑥 ∩ 𝐵)) |
20 | 18, 19 | fmptd 6292 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝑥 ∩ 𝐵)):(𝒫 𝐴 ∩ Fin)⟶(𝒫 𝐵 ∩ Fin)) |
21 | | frn 5966 |
. . . 4
⊢ ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝑥 ∩ 𝐵)):(𝒫 𝐴 ∩ Fin)⟶(𝒫 𝐵 ∩ Fin) → ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝑥 ∩ 𝐵)) ⊆ (𝒫 𝐵 ∩ Fin)) |
22 | 20, 21 | syl 17 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝑥 ∩ 𝐵)) ⊆ (𝒫 𝐵 ∩ Fin)) |
23 | 8, 22 | eqsstrd 3602 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → ((𝒫 𝐴 ∩ Fin) ↾t 𝐵) ⊆ (𝒫 𝐵 ∩ Fin)) |
24 | | elfpw 8151 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝑥 ⊆ 𝐵 ∧ 𝑥 ∈ Fin)) |
25 | 24 | simplbi 475 |
. . . . . . 7
⊢ (𝑥 ∈ (𝒫 𝐵 ∩ Fin) → 𝑥 ⊆ 𝐵) |
26 | 25 | adantl 481 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑥 ⊆ 𝐵) |
27 | | df-ss 3554 |
. . . . . 6
⊢ (𝑥 ⊆ 𝐵 ↔ (𝑥 ∩ 𝐵) = 𝑥) |
28 | 26, 27 | sylib 207 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → (𝑥 ∩ 𝐵) = 𝑥) |
29 | 4 | adantr 480 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → (𝒫 𝐴 ∩ Fin) ∈
V) |
30 | 6 | adantr 480 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝐵 ∈ V) |
31 | | simplr 788 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝐵 ⊆ 𝐴) |
32 | 26, 31 | sstrd 3578 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑥 ⊆ 𝐴) |
33 | 24 | simprbi 479 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝒫 𝐵 ∩ Fin) → 𝑥 ∈ Fin) |
34 | 33 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑥 ∈ Fin) |
35 | 32, 34, 11 | sylanbrc 695 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) |
36 | | elrestr 15912 |
. . . . . 6
⊢
(((𝒫 𝐴 ∩
Fin) ∈ V ∧ 𝐵
∈ V ∧ 𝑥 ∈
(𝒫 𝐴 ∩ Fin))
→ (𝑥 ∩ 𝐵) ∈ ((𝒫 𝐴 ∩ Fin) ↾t
𝐵)) |
37 | 29, 30, 35, 36 | syl3anc 1318 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → (𝑥 ∩ 𝐵) ∈ ((𝒫 𝐴 ∩ Fin) ↾t 𝐵)) |
38 | 28, 37 | eqeltrrd 2689 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑥 ∈ ((𝒫 𝐴 ∩ Fin) ↾t 𝐵)) |
39 | 38 | ex 449 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → (𝑥 ∈ (𝒫 𝐵 ∩ Fin) → 𝑥 ∈ ((𝒫 𝐴 ∩ Fin) ↾t 𝐵))) |
40 | 39 | ssrdv 3574 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → (𝒫 𝐵 ∩ Fin) ⊆ ((𝒫 𝐴 ∩ Fin) ↾t
𝐵)) |
41 | 23, 40 | eqssd 3585 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → ((𝒫 𝐴 ∩ Fin) ↾t 𝐵) = (𝒫 𝐵 ∩ Fin)) |