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