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 𝒫 A Fin F b : 𝒫 A Fin 1-1 onto 𝒫 B Fin

Proof

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