Metamath Proof Explorer

Theorem f1opwfi

Description: A one-to-one mapping induces a one-to-one mapping on finite subsets. (Contributed by Mario Carneiro, 25-Jan-2015)

Ref Expression
Assertion f1opwfi 
|- ( F : A -1-1-onto-> B -> ( b e. ( ~P A i^i Fin ) |-> ( F " b ) ) : ( ~P A i^i Fin ) -1-1-onto-> ( ~P B i^i Fin ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( b e. ( ~P A i^i Fin ) |-> ( F " b ) ) = ( b e. ( ~P A i^i Fin ) |-> ( F " b ) )
2 simpr 
 |-  ( ( F : A -1-1-onto-> B /\ b e. ( ~P A i^i Fin ) ) -> b e. ( ~P A i^i Fin ) )
3 2 elin2d 
 |-  ( ( F : A -1-1-onto-> B /\ b e. ( ~P A i^i Fin ) ) -> b e. Fin )
4 f1ofun 
 |-  ( F : A -1-1-onto-> B -> Fun F )
5 elinel1 
 |-  ( b e. ( ~P A i^i Fin ) -> b e. ~P A )
6 elpwi 
 |-  ( b e. ~P A -> b C_ A )
7 5 6 syl 
 |-  ( b e. ( ~P A i^i Fin ) -> b C_ A )
8 7 adantl 
 |-  ( ( F : A -1-1-onto-> B /\ b e. ( ~P A i^i Fin ) ) -> b C_ A )
9 f1odm 
 |-  ( F : A -1-1-onto-> B -> dom F = A )
10 9 adantr 
 |-  ( ( F : A -1-1-onto-> B /\ b e. ( ~P A i^i Fin ) ) -> dom F = A )
11 8 10 sseqtrrd 
 |-  ( ( F : A -1-1-onto-> B /\ b e. ( ~P A i^i Fin ) ) -> b C_ dom F )
12 fores 
 |-  ( ( Fun F /\ b C_ dom F ) -> ( F |` b ) : b -onto-> ( F " b ) )
13 4 11 12 syl2an2r 
 |-  ( ( F : A -1-1-onto-> B /\ b e. ( ~P A i^i Fin ) ) -> ( F |` b ) : b -onto-> ( F " b ) )
14 fofi 
 |-  ( ( b e. Fin /\ ( F |` b ) : b -onto-> ( F " b ) ) -> ( F " b ) e. Fin )
15 3 13 14 syl2anc 
 |-  ( ( F : A -1-1-onto-> B /\ b e. ( ~P A i^i Fin ) ) -> ( F " b ) e. Fin )
16 imassrn 
 |-  ( F " b ) C_ ran F
17 f1ofo 
 |-  ( F : A -1-1-onto-> B -> F : A -onto-> B )
18 forn 
 |-  ( F : A -onto-> B -> ran F = B )
19 17 18 syl 
 |-  ( F : A -1-1-onto-> B -> ran F = B )
20 16 19 sseqtrid 
 |-  ( F : A -1-1-onto-> B -> ( F " b ) C_ B )
21 20 adantr 
 |-  ( ( F : A -1-1-onto-> B /\ b e. ( ~P A i^i Fin ) ) -> ( F " b ) C_ B )
22 15 21 elpwd 
 |-  ( ( F : A -1-1-onto-> B /\ b e. ( ~P A i^i Fin ) ) -> ( F " b ) e. ~P B )
23 22 15 elind 
 |-  ( ( F : A -1-1-onto-> B /\ b e. ( ~P A i^i Fin ) ) -> ( F " b ) e. ( ~P B i^i Fin ) )
24 simpr 
 |-  ( ( F : A -1-1-onto-> B /\ a e. ( ~P B i^i Fin ) ) -> a e. ( ~P B i^i Fin ) )
25 24 elin2d 
 |-  ( ( F : A -1-1-onto-> B /\ a e. ( ~P B i^i Fin ) ) -> a e. Fin )
26 dff1o3 
 |-  ( F : A -1-1-onto-> B <-> ( F : A -onto-> B /\ Fun `' F ) )
27 26 simprbi 
 |-  ( F : A -1-1-onto-> B -> Fun `' F )
28 elinel1 
 |-  ( a e. ( ~P B i^i Fin ) -> a e. ~P B )
29 28 adantl 
 |-  ( ( F : A -1-1-onto-> B /\ a e. ( ~P B i^i Fin ) ) -> a e. ~P B )
30 elpwi 
 |-  ( a e. ~P B -> a C_ B )
31 29 30 syl 
 |-  ( ( F : A -1-1-onto-> B /\ a e. ( ~P B i^i Fin ) ) -> a C_ B )
32 f1ocnv 
 |-  ( F : A -1-1-onto-> B -> `' F : B -1-1-onto-> A )
33 32 adantr 
 |-  ( ( F : A -1-1-onto-> B /\ a e. ( ~P B i^i Fin ) ) -> `' F : B -1-1-onto-> A )
34 f1odm 
 |-  ( `' F : B -1-1-onto-> A -> dom `' F = B )
35 33 34 syl 
 |-  ( ( F : A -1-1-onto-> B /\ a e. ( ~P B i^i Fin ) ) -> dom `' F = B )
36 31 35 sseqtrrd 
 |-  ( ( F : A -1-1-onto-> B /\ a e. ( ~P B i^i Fin ) ) -> a C_ dom `' F )
37 fores 
 |-  ( ( Fun `' F /\ a C_ dom `' F ) -> ( `' F |` a ) : a -onto-> ( `' F " a ) )
38 27 36 37 syl2an2r 
 |-  ( ( F : A -1-1-onto-> B /\ a e. ( ~P B i^i Fin ) ) -> ( `' F |` a ) : a -onto-> ( `' F " a ) )
39 fofi 
 |-  ( ( a e. Fin /\ ( `' F |` a ) : a -onto-> ( `' F " a ) ) -> ( `' F " a ) e. Fin )
40 25 38 39 syl2anc 
 |-  ( ( F : A -1-1-onto-> B /\ a e. ( ~P B i^i Fin ) ) -> ( `' F " a ) e. Fin )
41 imassrn 
 |-  ( `' F " a ) C_ ran `' F
42 dfdm4 
 |-  dom F = ran `' F
43 42 9 eqtr3id 
 |-  ( F : A -1-1-onto-> B -> ran `' F = A )
44 41 43 sseqtrid 
 |-  ( F : A -1-1-onto-> B -> ( `' F " a ) C_ A )
45 44 adantr 
 |-  ( ( F : A -1-1-onto-> B /\ a e. ( ~P B i^i Fin ) ) -> ( `' F " a ) C_ A )
46 40 45 elpwd 
 |-  ( ( F : A -1-1-onto-> B /\ a e. ( ~P B i^i Fin ) ) -> ( `' F " a ) e. ~P A )
47 46 40 elind 
 |-  ( ( F : A -1-1-onto-> B /\ a e. ( ~P B i^i Fin ) ) -> ( `' F " a ) e. ( ~P A i^i Fin ) )
48 5 28 anim12i 
 |-  ( ( b e. ( ~P A i^i Fin ) /\ a e. ( ~P B i^i Fin ) ) -> ( b e. ~P A /\ a e. ~P B ) )
49 30 adantl 
 |-  ( ( b e. ~P A /\ a e. ~P B ) -> a C_ B )
50 foimacnv 
 |-  ( ( F : A -onto-> B /\ a C_ B ) -> ( F " ( `' F " a ) ) = a )
51 17 49 50 syl2an 
 |-  ( ( F : A -1-1-onto-> B /\ ( b e. ~P A /\ a e. ~P B ) ) -> ( F " ( `' F " a ) ) = a )
52 51 eqcomd 
 |-  ( ( F : A -1-1-onto-> B /\ ( b e. ~P A /\ a e. ~P B ) ) -> a = ( F " ( `' F " a ) ) )
53 imaeq2 
 |-  ( b = ( `' F " a ) -> ( F " b ) = ( F " ( `' F " a ) ) )
54 53 eqeq2d 
 |-  ( b = ( `' F " a ) -> ( a = ( F " b ) <-> a = ( F " ( `' F " a ) ) ) )
55 52 54 syl5ibrcom 
 |-  ( ( F : A -1-1-onto-> B /\ ( b e. ~P A /\ a e. ~P B ) ) -> ( b = ( `' F " a ) -> a = ( F " b ) ) )
56 f1of1 
 |-  ( F : A -1-1-onto-> B -> F : A -1-1-> B )
57 6 adantr 
 |-  ( ( b e. ~P A /\ a e. ~P B ) -> b C_ A )
58 f1imacnv 
 |-  ( ( F : A -1-1-> B /\ b C_ A ) -> ( `' F " ( F " b ) ) = b )
59 56 57 58 syl2an 
 |-  ( ( F : A -1-1-onto-> B /\ ( b e. ~P A /\ a e. ~P B ) ) -> ( `' F " ( F " b ) ) = b )
60 59 eqcomd 
 |-  ( ( F : A -1-1-onto-> B /\ ( b e. ~P A /\ a e. ~P B ) ) -> b = ( `' F " ( F " b ) ) )
61 imaeq2 
 |-  ( a = ( F " b ) -> ( `' F " a ) = ( `' F " ( F " b ) ) )
62 61 eqeq2d 
 |-  ( a = ( F " b ) -> ( b = ( `' F " a ) <-> b = ( `' F " ( F " b ) ) ) )
63 60 62 syl5ibrcom 
 |-  ( ( F : A -1-1-onto-> B /\ ( b e. ~P A /\ a e. ~P B ) ) -> ( a = ( F " b ) -> b = ( `' F " a ) ) )
64 55 63 impbid 
 |-  ( ( F : A -1-1-onto-> B /\ ( b e. ~P A /\ a e. ~P B ) ) -> ( b = ( `' F " a ) <-> a = ( F " b ) ) )
65 48 64 sylan2 
 |-  ( ( F : A -1-1-onto-> B /\ ( b e. ( ~P A i^i Fin ) /\ a e. ( ~P B i^i Fin ) ) ) -> ( b = ( `' F " a ) <-> a = ( F " b ) ) )
66 1 23 47 65 f1o2d 
 |-  ( F : A -1-1-onto-> B -> ( b e. ( ~P A i^i Fin ) |-> ( F " b ) ) : ( ~P A i^i Fin ) -1-1-onto-> ( ~P B i^i Fin ) )