| Step | Hyp | Ref
| Expression |
| 1 | | pwexg 5378 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) |
| 2 | 1 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → 𝒫 𝐴 ∈ V) |
| 3 | | inex1g 5319 |
. . . . 5
⊢
(𝒫 𝐴 ∈
V → (𝒫 𝐴 ∩
Fin) ∈ V) |
| 4 | 2, 3 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → (𝒫 𝐴 ∩ Fin) ∈ V) |
| 5 | | ssexg 5323 |
. . . . 5
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐵 ∈ V) |
| 6 | 5 | ancoms 458 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ V) |
| 7 | | restval 17471 |
. . . 4
⊢
(((𝒫 𝐴 ∩
Fin) ∈ V ∧ 𝐵
∈ V) → ((𝒫 𝐴 ∩ Fin) ↾t 𝐵) = ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝑥 ∩ 𝐵))) |
| 8 | 4, 6, 7 | syl2anc 584 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → ((𝒫 𝐴 ∩ Fin) ↾t 𝐵) = ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝑥 ∩ 𝐵))) |
| 9 | | inss2 4238 |
. . . . . . 7
⊢ (𝑥 ∩ 𝐵) ⊆ 𝐵 |
| 10 | 9 | a1i 11 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑥 ∩ 𝐵) ⊆ 𝐵) |
| 11 | | elinel2 4202 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ∈ Fin) |
| 12 | 11 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ∈ Fin) |
| 13 | | inss1 4237 |
. . . . . . 7
⊢ (𝑥 ∩ 𝐵) ⊆ 𝑥 |
| 14 | | ssfi 9213 |
. . . . . . 7
⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ 𝐵) ⊆ 𝑥) → (𝑥 ∩ 𝐵) ∈ Fin) |
| 15 | 12, 13, 14 | sylancl 586 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑥 ∩ 𝐵) ∈ Fin) |
| 16 | | elfpw 9394 |
. . . . . 6
⊢ ((𝑥 ∩ 𝐵) ∈ (𝒫 𝐵 ∩ Fin) ↔ ((𝑥 ∩ 𝐵) ⊆ 𝐵 ∧ (𝑥 ∩ 𝐵) ∈ Fin)) |
| 17 | 10, 15, 16 | sylanbrc 583 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑥 ∩ 𝐵) ∈ (𝒫 𝐵 ∩ Fin)) |
| 18 | 17 | fmpttd 7135 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝑥 ∩ 𝐵)):(𝒫 𝐴 ∩ Fin)⟶(𝒫 𝐵 ∩ Fin)) |
| 19 | 18 | frnd 6744 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝑥 ∩ 𝐵)) ⊆ (𝒫 𝐵 ∩ Fin)) |
| 20 | 8, 19 | eqsstrd 4018 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → ((𝒫 𝐴 ∩ Fin) ↾t 𝐵) ⊆ (𝒫 𝐵 ∩ Fin)) |
| 21 | | elfpw 9394 |
. . . . . 6
⊢ (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝑥 ⊆ 𝐵 ∧ 𝑥 ∈ Fin)) |
| 22 | 21 | simplbi 497 |
. . . . 5
⊢ (𝑥 ∈ (𝒫 𝐵 ∩ Fin) → 𝑥 ⊆ 𝐵) |
| 23 | 22 | adantl 481 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑥 ⊆ 𝐵) |
| 24 | | dfss2 3969 |
. . . 4
⊢ (𝑥 ⊆ 𝐵 ↔ (𝑥 ∩ 𝐵) = 𝑥) |
| 25 | 23, 24 | sylib 218 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → (𝑥 ∩ 𝐵) = 𝑥) |
| 26 | 4 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → (𝒫 𝐴 ∩ Fin) ∈
V) |
| 27 | 6 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝐵 ∈ V) |
| 28 | | simplr 769 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝐵 ⊆ 𝐴) |
| 29 | 23, 28 | sstrd 3994 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑥 ⊆ 𝐴) |
| 30 | | elinel2 4202 |
. . . . . 6
⊢ (𝑥 ∈ (𝒫 𝐵 ∩ Fin) → 𝑥 ∈ Fin) |
| 31 | 30 | adantl 481 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑥 ∈ Fin) |
| 32 | | elfpw 9394 |
. . . . 5
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 ∈ Fin)) |
| 33 | 29, 31, 32 | sylanbrc 583 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) |
| 34 | | elrestr 17473 |
. . . 4
⊢
(((𝒫 𝐴 ∩
Fin) ∈ V ∧ 𝐵
∈ V ∧ 𝑥 ∈
(𝒫 𝐴 ∩ Fin))
→ (𝑥 ∩ 𝐵) ∈ ((𝒫 𝐴 ∩ Fin) ↾t
𝐵)) |
| 35 | 26, 27, 33, 34 | syl3anc 1373 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → (𝑥 ∩ 𝐵) ∈ ((𝒫 𝐴 ∩ Fin) ↾t 𝐵)) |
| 36 | 25, 35 | eqeltrrd 2842 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑥 ∈ ((𝒫 𝐴 ∩ Fin) ↾t 𝐵)) |
| 37 | 20, 36 | eqelssd 4005 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → ((𝒫 𝐴 ∩ Fin) ↾t 𝐵) = (𝒫 𝐵 ∩ Fin)) |