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 dfss2 ⊢ ( 𝑥 ⊆ 𝐵 ↔ ( 𝑥 ∩ 𝐵 ) = 𝑥 )
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 ) )