Metamath Proof Explorer


Theorem restfpw

Description: The restriction of the set of finite subsets of A is the set of finite subsets of B . (Contributed by Mario Carneiro, 18-Sep-2015)

Ref Expression
Assertion restfpw ( ( 𝐴𝑉𝐵𝐴 ) → ( ( 𝒫 𝐴 ∩ Fin ) ↾t 𝐵 ) = ( 𝒫 𝐵 ∩ Fin ) )

Proof

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 ) )