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