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 ( 𝐹 : 𝐴1-1-onto𝐵 → ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐹𝑏 ) ) : ( 𝒫 𝐴 ∩ Fin ) –1-1-onto→ ( 𝒫 𝐵 ∩ Fin ) )

Proof

Step Hyp Ref Expression
1 eqid ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐹𝑏 ) ) = ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐹𝑏 ) )
2 simpr ( ( 𝐹 : 𝐴1-1-onto𝐵𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) )
3 2 elin2d ( ( 𝐹 : 𝐴1-1-onto𝐵𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑏 ∈ Fin )
4 f1ofun ( 𝐹 : 𝐴1-1-onto𝐵 → Fun 𝐹 )
5 elinel1 ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑏 ∈ 𝒫 𝐴 )
6 elpwi ( 𝑏 ∈ 𝒫 𝐴𝑏𝐴 )
7 5 6 syl ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑏𝐴 )
8 7 adantl ( ( 𝐹 : 𝐴1-1-onto𝐵𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑏𝐴 )
9 f1odm ( 𝐹 : 𝐴1-1-onto𝐵 → dom 𝐹 = 𝐴 )
10 9 adantr ( ( 𝐹 : 𝐴1-1-onto𝐵𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → dom 𝐹 = 𝐴 )
11 8 10 sseqtrrd ( ( 𝐹 : 𝐴1-1-onto𝐵𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑏 ⊆ dom 𝐹 )
12 fores ( ( Fun 𝐹𝑏 ⊆ dom 𝐹 ) → ( 𝐹𝑏 ) : 𝑏onto→ ( 𝐹𝑏 ) )
13 4 11 12 syl2an2r ( ( 𝐹 : 𝐴1-1-onto𝐵𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹𝑏 ) : 𝑏onto→ ( 𝐹𝑏 ) )
14 fofi ( ( 𝑏 ∈ Fin ∧ ( 𝐹𝑏 ) : 𝑏onto→ ( 𝐹𝑏 ) ) → ( 𝐹𝑏 ) ∈ Fin )
15 3 13 14 syl2anc ( ( 𝐹 : 𝐴1-1-onto𝐵𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹𝑏 ) ∈ Fin )
16 imassrn ( 𝐹𝑏 ) ⊆ ran 𝐹
17 f1ofo ( 𝐹 : 𝐴1-1-onto𝐵𝐹 : 𝐴onto𝐵 )
18 forn ( 𝐹 : 𝐴onto𝐵 → ran 𝐹 = 𝐵 )
19 17 18 syl ( 𝐹 : 𝐴1-1-onto𝐵 → ran 𝐹 = 𝐵 )
20 16 19 sseqtrid ( 𝐹 : 𝐴1-1-onto𝐵 → ( 𝐹𝑏 ) ⊆ 𝐵 )
21 20 adantr ( ( 𝐹 : 𝐴1-1-onto𝐵𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹𝑏 ) ⊆ 𝐵 )
22 15 21 elpwd ( ( 𝐹 : 𝐴1-1-onto𝐵𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹𝑏 ) ∈ 𝒫 𝐵 )
23 22 15 elind ( ( 𝐹 : 𝐴1-1-onto𝐵𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹𝑏 ) ∈ ( 𝒫 𝐵 ∩ Fin ) )
24 simpr ( ( 𝐹 : 𝐴1-1-onto𝐵𝑎 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → 𝑎 ∈ ( 𝒫 𝐵 ∩ Fin ) )
25 24 elin2d ( ( 𝐹 : 𝐴1-1-onto𝐵𝑎 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → 𝑎 ∈ Fin )
26 dff1o3 ( 𝐹 : 𝐴1-1-onto𝐵 ↔ ( 𝐹 : 𝐴onto𝐵 ∧ Fun 𝐹 ) )
27 26 simprbi ( 𝐹 : 𝐴1-1-onto𝐵 → Fun 𝐹 )
28 elinel1 ( 𝑎 ∈ ( 𝒫 𝐵 ∩ Fin ) → 𝑎 ∈ 𝒫 𝐵 )
29 28 adantl ( ( 𝐹 : 𝐴1-1-onto𝐵𝑎 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → 𝑎 ∈ 𝒫 𝐵 )
30 elpwi ( 𝑎 ∈ 𝒫 𝐵𝑎𝐵 )
31 29 30 syl ( ( 𝐹 : 𝐴1-1-onto𝐵𝑎 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → 𝑎𝐵 )
32 f1ocnv ( 𝐹 : 𝐴1-1-onto𝐵 𝐹 : 𝐵1-1-onto𝐴 )
33 32 adantr ( ( 𝐹 : 𝐴1-1-onto𝐵𝑎 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → 𝐹 : 𝐵1-1-onto𝐴 )
34 f1odm ( 𝐹 : 𝐵1-1-onto𝐴 → dom 𝐹 = 𝐵 )
35 33 34 syl ( ( 𝐹 : 𝐴1-1-onto𝐵𝑎 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → dom 𝐹 = 𝐵 )
36 31 35 sseqtrrd ( ( 𝐹 : 𝐴1-1-onto𝐵𝑎 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → 𝑎 ⊆ dom 𝐹 )
37 fores ( ( Fun 𝐹𝑎 ⊆ dom 𝐹 ) → ( 𝐹𝑎 ) : 𝑎onto→ ( 𝐹𝑎 ) )
38 27 36 37 syl2an2r ( ( 𝐹 : 𝐴1-1-onto𝐵𝑎 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → ( 𝐹𝑎 ) : 𝑎onto→ ( 𝐹𝑎 ) )
39 fofi ( ( 𝑎 ∈ Fin ∧ ( 𝐹𝑎 ) : 𝑎onto→ ( 𝐹𝑎 ) ) → ( 𝐹𝑎 ) ∈ Fin )
40 25 38 39 syl2anc ( ( 𝐹 : 𝐴1-1-onto𝐵𝑎 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → ( 𝐹𝑎 ) ∈ Fin )
41 imassrn ( 𝐹𝑎 ) ⊆ ran 𝐹
42 dfdm4 dom 𝐹 = ran 𝐹
43 42 9 eqtr3id ( 𝐹 : 𝐴1-1-onto𝐵 → ran 𝐹 = 𝐴 )
44 41 43 sseqtrid ( 𝐹 : 𝐴1-1-onto𝐵 → ( 𝐹𝑎 ) ⊆ 𝐴 )
45 44 adantr ( ( 𝐹 : 𝐴1-1-onto𝐵𝑎 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → ( 𝐹𝑎 ) ⊆ 𝐴 )
46 40 45 elpwd ( ( 𝐹 : 𝐴1-1-onto𝐵𝑎 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → ( 𝐹𝑎 ) ∈ 𝒫 𝐴 )
47 46 40 elind ( ( 𝐹 : 𝐴1-1-onto𝐵𝑎 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → ( 𝐹𝑎 ) ∈ ( 𝒫 𝐴 ∩ Fin ) )
48 5 28 anim12i ( ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑎 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → ( 𝑏 ∈ 𝒫 𝐴𝑎 ∈ 𝒫 𝐵 ) )
49 30 adantl ( ( 𝑏 ∈ 𝒫 𝐴𝑎 ∈ 𝒫 𝐵 ) → 𝑎𝐵 )
50 foimacnv ( ( 𝐹 : 𝐴onto𝐵𝑎𝐵 ) → ( 𝐹 “ ( 𝐹𝑎 ) ) = 𝑎 )
51 17 49 50 syl2an ( ( 𝐹 : 𝐴1-1-onto𝐵 ∧ ( 𝑏 ∈ 𝒫 𝐴𝑎 ∈ 𝒫 𝐵 ) ) → ( 𝐹 “ ( 𝐹𝑎 ) ) = 𝑎 )
52 51 eqcomd ( ( 𝐹 : 𝐴1-1-onto𝐵 ∧ ( 𝑏 ∈ 𝒫 𝐴𝑎 ∈ 𝒫 𝐵 ) ) → 𝑎 = ( 𝐹 “ ( 𝐹𝑎 ) ) )
53 imaeq2 ( 𝑏 = ( 𝐹𝑎 ) → ( 𝐹𝑏 ) = ( 𝐹 “ ( 𝐹𝑎 ) ) )
54 53 eqeq2d ( 𝑏 = ( 𝐹𝑎 ) → ( 𝑎 = ( 𝐹𝑏 ) ↔ 𝑎 = ( 𝐹 “ ( 𝐹𝑎 ) ) ) )
55 52 54 syl5ibrcom ( ( 𝐹 : 𝐴1-1-onto𝐵 ∧ ( 𝑏 ∈ 𝒫 𝐴𝑎 ∈ 𝒫 𝐵 ) ) → ( 𝑏 = ( 𝐹𝑎 ) → 𝑎 = ( 𝐹𝑏 ) ) )
56 f1of1 ( 𝐹 : 𝐴1-1-onto𝐵𝐹 : 𝐴1-1𝐵 )
57 6 adantr ( ( 𝑏 ∈ 𝒫 𝐴𝑎 ∈ 𝒫 𝐵 ) → 𝑏𝐴 )
58 f1imacnv ( ( 𝐹 : 𝐴1-1𝐵𝑏𝐴 ) → ( 𝐹 “ ( 𝐹𝑏 ) ) = 𝑏 )
59 56 57 58 syl2an ( ( 𝐹 : 𝐴1-1-onto𝐵 ∧ ( 𝑏 ∈ 𝒫 𝐴𝑎 ∈ 𝒫 𝐵 ) ) → ( 𝐹 “ ( 𝐹𝑏 ) ) = 𝑏 )
60 59 eqcomd ( ( 𝐹 : 𝐴1-1-onto𝐵 ∧ ( 𝑏 ∈ 𝒫 𝐴𝑎 ∈ 𝒫 𝐵 ) ) → 𝑏 = ( 𝐹 “ ( 𝐹𝑏 ) ) )
61 imaeq2 ( 𝑎 = ( 𝐹𝑏 ) → ( 𝐹𝑎 ) = ( 𝐹 “ ( 𝐹𝑏 ) ) )
62 61 eqeq2d ( 𝑎 = ( 𝐹𝑏 ) → ( 𝑏 = ( 𝐹𝑎 ) ↔ 𝑏 = ( 𝐹 “ ( 𝐹𝑏 ) ) ) )
63 60 62 syl5ibrcom ( ( 𝐹 : 𝐴1-1-onto𝐵 ∧ ( 𝑏 ∈ 𝒫 𝐴𝑎 ∈ 𝒫 𝐵 ) ) → ( 𝑎 = ( 𝐹𝑏 ) → 𝑏 = ( 𝐹𝑎 ) ) )
64 55 63 impbid ( ( 𝐹 : 𝐴1-1-onto𝐵 ∧ ( 𝑏 ∈ 𝒫 𝐴𝑎 ∈ 𝒫 𝐵 ) ) → ( 𝑏 = ( 𝐹𝑎 ) ↔ 𝑎 = ( 𝐹𝑏 ) ) )
65 48 64 sylan2 ( ( 𝐹 : 𝐴1-1-onto𝐵 ∧ ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑎 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) → ( 𝑏 = ( 𝐹𝑎 ) ↔ 𝑎 = ( 𝐹𝑏 ) ) )
66 1 23 47 65 f1o2d ( 𝐹 : 𝐴1-1-onto𝐵 → ( 𝑏 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐹𝑏 ) ) : ( 𝒫 𝐴 ∩ Fin ) –1-1-onto→ ( 𝒫 𝐵 ∩ Fin ) )