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 
|- ( ( A e. V /\ B C_ A ) -> ( ( ~P A i^i Fin ) |`t B ) = ( ~P B i^i Fin ) )

Proof

Step Hyp Ref Expression
1 pwexg 
 |-  ( A e. V -> ~P A e. _V )
2 1 adantr 
 |-  ( ( A e. V /\ B C_ A ) -> ~P A e. _V )
3 inex1g 
 |-  ( ~P A e. _V -> ( ~P A i^i Fin ) e. _V )
4 2 3 syl 
 |-  ( ( A e. V /\ B C_ A ) -> ( ~P A i^i Fin ) e. _V )
5 ssexg 
 |-  ( ( B C_ A /\ A e. V ) -> B e. _V )
6 5 ancoms 
 |-  ( ( A e. V /\ B C_ A ) -> B e. _V )
7 restval 
 |-  ( ( ( ~P A i^i Fin ) e. _V /\ B e. _V ) -> ( ( ~P A i^i Fin ) |`t B ) = ran ( x e. ( ~P A i^i Fin ) |-> ( x i^i B ) ) )
8 4 6 7 syl2anc 
 |-  ( ( A e. V /\ B C_ A ) -> ( ( ~P A i^i Fin ) |`t B ) = ran ( x e. ( ~P A i^i Fin ) |-> ( x i^i B ) ) )
9 inss2 
 |-  ( x i^i B ) C_ B
10 9 a1i 
 |-  ( ( ( A e. V /\ B C_ A ) /\ x e. ( ~P A i^i Fin ) ) -> ( x i^i B ) C_ B )
11 elinel2 
 |-  ( x e. ( ~P A i^i Fin ) -> x e. Fin )
12 11 adantl 
 |-  ( ( ( A e. V /\ B C_ A ) /\ x e. ( ~P A i^i Fin ) ) -> x e. Fin )
13 inss1 
 |-  ( x i^i B ) C_ x
14 ssfi 
 |-  ( ( x e. Fin /\ ( x i^i B ) C_ x ) -> ( x i^i B ) e. Fin )
15 12 13 14 sylancl 
 |-  ( ( ( A e. V /\ B C_ A ) /\ x e. ( ~P A i^i Fin ) ) -> ( x i^i B ) e. Fin )
16 elfpw 
 |-  ( ( x i^i B ) e. ( ~P B i^i Fin ) <-> ( ( x i^i B ) C_ B /\ ( x i^i B ) e. Fin ) )
17 10 15 16 sylanbrc 
 |-  ( ( ( A e. V /\ B C_ A ) /\ x e. ( ~P A i^i Fin ) ) -> ( x i^i B ) e. ( ~P B i^i Fin ) )
18 17 fmpttd 
 |-  ( ( A e. V /\ B C_ A ) -> ( x e. ( ~P A i^i Fin ) |-> ( x i^i B ) ) : ( ~P A i^i Fin ) --> ( ~P B i^i Fin ) )
19 18 frnd 
 |-  ( ( A e. V /\ B C_ A ) -> ran ( x e. ( ~P A i^i Fin ) |-> ( x i^i B ) ) C_ ( ~P B i^i Fin ) )
20 8 19 eqsstrd 
 |-  ( ( A e. V /\ B C_ A ) -> ( ( ~P A i^i Fin ) |`t B ) C_ ( ~P B i^i Fin ) )
21 elfpw 
 |-  ( x e. ( ~P B i^i Fin ) <-> ( x C_ B /\ x e. Fin ) )
22 21 simplbi 
 |-  ( x e. ( ~P B i^i Fin ) -> x C_ B )
23 22 adantl 
 |-  ( ( ( A e. V /\ B C_ A ) /\ x e. ( ~P B i^i Fin ) ) -> x C_ B )
24 df-ss 
 |-  ( x C_ B <-> ( x i^i B ) = x )
25 23 24 sylib 
 |-  ( ( ( A e. V /\ B C_ A ) /\ x e. ( ~P B i^i Fin ) ) -> ( x i^i B ) = x )
26 4 adantr 
 |-  ( ( ( A e. V /\ B C_ A ) /\ x e. ( ~P B i^i Fin ) ) -> ( ~P A i^i Fin ) e. _V )
27 6 adantr 
 |-  ( ( ( A e. V /\ B C_ A ) /\ x e. ( ~P B i^i Fin ) ) -> B e. _V )
28 simplr 
 |-  ( ( ( A e. V /\ B C_ A ) /\ x e. ( ~P B i^i Fin ) ) -> B C_ A )
29 23 28 sstrd 
 |-  ( ( ( A e. V /\ B C_ A ) /\ x e. ( ~P B i^i Fin ) ) -> x C_ A )
30 elinel2 
 |-  ( x e. ( ~P B i^i Fin ) -> x e. Fin )
31 30 adantl 
 |-  ( ( ( A e. V /\ B C_ A ) /\ x e. ( ~P B i^i Fin ) ) -> x e. Fin )
32 elfpw 
 |-  ( x e. ( ~P A i^i Fin ) <-> ( x C_ A /\ x e. Fin ) )
33 29 31 32 sylanbrc 
 |-  ( ( ( A e. V /\ B C_ A ) /\ x e. ( ~P B i^i Fin ) ) -> x e. ( ~P A i^i Fin ) )
34 elrestr 
 |-  ( ( ( ~P A i^i Fin ) e. _V /\ B e. _V /\ x e. ( ~P A i^i Fin ) ) -> ( x i^i B ) e. ( ( ~P A i^i Fin ) |`t B ) )
35 26 27 33 34 syl3anc 
 |-  ( ( ( A e. V /\ B C_ A ) /\ x e. ( ~P B i^i Fin ) ) -> ( x i^i B ) e. ( ( ~P A i^i Fin ) |`t B ) )
36 25 35 eqeltrrd 
 |-  ( ( ( A e. V /\ B C_ A ) /\ x e. ( ~P B i^i Fin ) ) -> x e. ( ( ~P A i^i Fin ) |`t B ) )
37 20 36 eqelssd 
 |-  ( ( A e. V /\ B C_ A ) -> ( ( ~P A i^i Fin ) |`t B ) = ( ~P B i^i Fin ) )