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 syl5eqr ⊢ ( 𝐹 : 𝐴 –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 ) )