Step |
Hyp |
Ref |
Expression |
1 |
|
pwexg |
⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V ) |
2 |
1
|
adantr |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) → 𝒫 𝐴 ∈ V ) |
3 |
|
inex1g |
⊢ ( 𝒫 𝐴 ∈ V → ( 𝒫 𝐴 ∩ Fin ) ∈ V ) |
4 |
2 3
|
syl |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝒫 𝐴 ∩ Fin ) ∈ V ) |
5 |
|
ssexg |
⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐵 ∈ V ) |
6 |
5
|
ancoms |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ V ) |
7 |
|
restval |
⊢ ( ( ( 𝒫 𝐴 ∩ Fin ) ∈ V ∧ 𝐵 ∈ V ) → ( ( 𝒫 𝐴 ∩ Fin ) ↾t 𝐵 ) = ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝑥 ∩ 𝐵 ) ) ) |
8 |
4 6 7
|
syl2anc |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝒫 𝐴 ∩ Fin ) ↾t 𝐵 ) = ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝑥 ∩ 𝐵 ) ) ) |
9 |
|
inss2 |
⊢ ( 𝑥 ∩ 𝐵 ) ⊆ 𝐵 |
10 |
9
|
a1i |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑥 ∩ 𝐵 ) ⊆ 𝐵 ) |
11 |
|
elinel2 |
⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑥 ∈ Fin ) |
12 |
11
|
adantl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑥 ∈ Fin ) |
13 |
|
inss1 |
⊢ ( 𝑥 ∩ 𝐵 ) ⊆ 𝑥 |
14 |
|
ssfi |
⊢ ( ( 𝑥 ∈ Fin ∧ ( 𝑥 ∩ 𝐵 ) ⊆ 𝑥 ) → ( 𝑥 ∩ 𝐵 ) ∈ Fin ) |
15 |
12 13 14
|
sylancl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑥 ∩ 𝐵 ) ∈ Fin ) |
16 |
|
elfpw |
⊢ ( ( 𝑥 ∩ 𝐵 ) ∈ ( 𝒫 𝐵 ∩ Fin ) ↔ ( ( 𝑥 ∩ 𝐵 ) ⊆ 𝐵 ∧ ( 𝑥 ∩ 𝐵 ) ∈ Fin ) ) |
17 |
10 15 16
|
sylanbrc |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑥 ∩ 𝐵 ) ∈ ( 𝒫 𝐵 ∩ Fin ) ) |
18 |
17
|
fmpttd |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝑥 ∩ 𝐵 ) ) : ( 𝒫 𝐴 ∩ Fin ) ⟶ ( 𝒫 𝐵 ∩ Fin ) ) |
19 |
18
|
frnd |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) → ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝑥 ∩ 𝐵 ) ) ⊆ ( 𝒫 𝐵 ∩ Fin ) ) |
20 |
8 19
|
eqsstrd |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝒫 𝐴 ∩ Fin ) ↾t 𝐵 ) ⊆ ( 𝒫 𝐵 ∩ Fin ) ) |
21 |
|
elfpw |
⊢ ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↔ ( 𝑥 ⊆ 𝐵 ∧ 𝑥 ∈ Fin ) ) |
22 |
21
|
simplbi |
⊢ ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) → 𝑥 ⊆ 𝐵 ) |
23 |
22
|
adantl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → 𝑥 ⊆ 𝐵 ) |
24 |
|
df-ss |
⊢ ( 𝑥 ⊆ 𝐵 ↔ ( 𝑥 ∩ 𝐵 ) = 𝑥 ) |
25 |
23 24
|
sylib |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → ( 𝑥 ∩ 𝐵 ) = 𝑥 ) |
26 |
4
|
adantr |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → ( 𝒫 𝐴 ∩ Fin ) ∈ V ) |
27 |
6
|
adantr |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → 𝐵 ∈ V ) |
28 |
|
simplr |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → 𝐵 ⊆ 𝐴 ) |
29 |
23 28
|
sstrd |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → 𝑥 ⊆ 𝐴 ) |
30 |
|
elinel2 |
⊢ ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) → 𝑥 ∈ Fin ) |
31 |
30
|
adantl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → 𝑥 ∈ Fin ) |
32 |
|
elfpw |
⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ∈ Fin ) ) |
33 |
29 31 32
|
sylanbrc |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) |
34 |
|
elrestr |
⊢ ( ( ( 𝒫 𝐴 ∩ Fin ) ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑥 ∩ 𝐵 ) ∈ ( ( 𝒫 𝐴 ∩ Fin ) ↾t 𝐵 ) ) |
35 |
26 27 33 34
|
syl3anc |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → ( 𝑥 ∩ 𝐵 ) ∈ ( ( 𝒫 𝐴 ∩ Fin ) ↾t 𝐵 ) ) |
36 |
25 35
|
eqeltrrd |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → 𝑥 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ↾t 𝐵 ) ) |
37 |
20 36
|
eqelssd |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝒫 𝐴 ∩ Fin ) ↾t 𝐵 ) = ( 𝒫 𝐵 ∩ Fin ) ) |