Metamath Proof Explorer

Theorem bitsf1

Description: The bits function is an injection from ZZ to ~P NN0 . It is obviously not a bijection (by Cantor's theorem canth2 ), and in fact its range is the set of finite and cofinite subsets of NN0 . (Contributed by Mario Carneiro, 22-Sep-2016)

Ref Expression
Assertion bitsf1 
|- bits : ZZ -1-1-> ~P NN0

Proof

Step Hyp Ref Expression
1 bitsf 
 |-  bits : ZZ --> ~P NN0
2 simpl 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> x e. ZZ )
3 2 zcnd 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> x e. CC )
4 3 adantr 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( -u x e. NN /\ ( bits ` x ) = ( bits ` y ) ) ) -> x e. CC )
5 simpr 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> y e. ZZ )
6 5 zcnd 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> y e. CC )
7 6 adantr 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( -u x e. NN /\ ( bits ` x ) = ( bits ` y ) ) ) -> y e. CC )
8 4 negcld 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( -u x e. NN /\ ( bits ` x ) = ( bits ` y ) ) ) -> -u x e. CC )
9 7 negcld 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( -u x e. NN /\ ( bits ` x ) = ( bits ` y ) ) ) -> -u y e. CC )
10 1cnd 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( -u x e. NN /\ ( bits ` x ) = ( bits ` y ) ) ) -> 1 e. CC )
11 simprr 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( -u x e. NN /\ ( bits ` x ) = ( bits ` y ) ) ) -> ( bits ` x ) = ( bits ` y ) )
12 11 difeq2d 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( -u x e. NN /\ ( bits ` x ) = ( bits ` y ) ) ) -> ( NN0 \ ( bits ` x ) ) = ( NN0 \ ( bits ` y ) ) )
13 bitscmp 
 |-  ( x e. ZZ -> ( NN0 \ ( bits ` x ) ) = ( bits ` ( -u x - 1 ) ) )
14 13 ad2antrr 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( -u x e. NN /\ ( bits ` x ) = ( bits ` y ) ) ) -> ( NN0 \ ( bits ` x ) ) = ( bits ` ( -u x - 1 ) ) )
15 bitscmp 
 |-  ( y e. ZZ -> ( NN0 \ ( bits ` y ) ) = ( bits ` ( -u y - 1 ) ) )
16 15 ad2antlr 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( -u x e. NN /\ ( bits ` x ) = ( bits ` y ) ) ) -> ( NN0 \ ( bits ` y ) ) = ( bits ` ( -u y - 1 ) ) )
17 12 14 16 3eqtr3d 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( -u x e. NN /\ ( bits ` x ) = ( bits ` y ) ) ) -> ( bits ` ( -u x - 1 ) ) = ( bits ` ( -u y - 1 ) ) )
18 nnm1nn0 
 |-  ( -u x e. NN -> ( -u x - 1 ) e. NN0 )
19 18 ad2antrl 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( -u x e. NN /\ ( bits ` x ) = ( bits ` y ) ) ) -> ( -u x - 1 ) e. NN0 )
20 19 fvresd 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( -u x e. NN /\ ( bits ` x ) = ( bits ` y ) ) ) -> ( ( bits |` NN0 ) ` ( -u x - 1 ) ) = ( bits ` ( -u x - 1 ) ) )
21 ominf 
 |-  -. _om e. Fin
22 nn0ennn 
 |-  NN0 ~~ NN
23 nnenom 
 |-  NN ~~ _om
24 22 23 entr2i 
 |-  _om ~~ NN0
25 enfii 
 |-  ( ( NN0 e. Fin /\ _om ~~ NN0 ) -> _om e. Fin )
26 24 25 mpan2 
 |-  ( NN0 e. Fin -> _om e. Fin )
27 21 26 mto 
 |-  -. NN0 e. Fin
28 difinf 
 |-  ( ( -. NN0 e. Fin /\ ( bits ` x ) e. Fin ) -> -. ( NN0 \ ( bits ` x ) ) e. Fin )
29 27 28 mpan 
 |-  ( ( bits ` x ) e. Fin -> -. ( NN0 \ ( bits ` x ) ) e. Fin )
30 bitsfi 
 |-  ( ( -u x - 1 ) e. NN0 -> ( bits ` ( -u x - 1 ) ) e. Fin )
31 19 30 syl 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( -u x e. NN /\ ( bits ` x ) = ( bits ` y ) ) ) -> ( bits ` ( -u x - 1 ) ) e. Fin )
32 14 31 eqeltrd 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( -u x e. NN /\ ( bits ` x ) = ( bits ` y ) ) ) -> ( NN0 \ ( bits ` x ) ) e. Fin )
33 29 32 nsyl3 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( -u x e. NN /\ ( bits ` x ) = ( bits ` y ) ) ) -> -. ( bits ` x ) e. Fin )
34 11 33 eqneltrrd 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( -u x e. NN /\ ( bits ` x ) = ( bits ` y ) ) ) -> -. ( bits ` y ) e. Fin )
35 bitsfi 
 |-  ( y e. NN0 -> ( bits ` y ) e. Fin )
36 34 35 nsyl 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( -u x e. NN /\ ( bits ` x ) = ( bits ` y ) ) ) -> -. y e. NN0 )
37 5 znegcld 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> -u y e. ZZ )
38 elznn 
 |-  ( -u y e. ZZ <-> ( -u y e. RR /\ ( -u y e. NN \/ -u -u y e. NN0 ) ) )
39 38 simprbi 
 |-  ( -u y e. ZZ -> ( -u y e. NN \/ -u -u y e. NN0 ) )
40 37 39 syl 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( -u y e. NN \/ -u -u y e. NN0 ) )
41 6 negnegd 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> -u -u y = y )
42 41 eleq1d 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( -u -u y e. NN0 <-> y e. NN0 ) )
43 42 orbi2d 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( ( -u y e. NN \/ -u -u y e. NN0 ) <-> ( -u y e. NN \/ y e. NN0 ) ) )
44 40 43 mpbid 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( -u y e. NN \/ y e. NN0 ) )
45 44 adantr 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( -u x e. NN /\ ( bits ` x ) = ( bits ` y ) ) ) -> ( -u y e. NN \/ y e. NN0 ) )
46 45 ord 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( -u x e. NN /\ ( bits ` x ) = ( bits ` y ) ) ) -> ( -. -u y e. NN -> y e. NN0 ) )
47 36 46 mt3d 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( -u x e. NN /\ ( bits ` x ) = ( bits ` y ) ) ) -> -u y e. NN )
48 nnm1nn0 
 |-  ( -u y e. NN -> ( -u y - 1 ) e. NN0 )
49 47 48 syl 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( -u x e. NN /\ ( bits ` x ) = ( bits ` y ) ) ) -> ( -u y - 1 ) e. NN0 )
50 49 fvresd 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( -u x e. NN /\ ( bits ` x ) = ( bits ` y ) ) ) -> ( ( bits |` NN0 ) ` ( -u y - 1 ) ) = ( bits ` ( -u y - 1 ) ) )
51 17 20 50 3eqtr4d 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( -u x e. NN /\ ( bits ` x ) = ( bits ` y ) ) ) -> ( ( bits |` NN0 ) ` ( -u x - 1 ) ) = ( ( bits |` NN0 ) ` ( -u y - 1 ) ) )
52 bitsf1o 
 |-  ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin )
53 f1of1 
 |-  ( ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) -> ( bits |` NN0 ) : NN0 -1-1-> ( ~P NN0 i^i Fin ) )
54 52 53 ax-mp 
 |-  ( bits |` NN0 ) : NN0 -1-1-> ( ~P NN0 i^i Fin )
55 f1fveq 
 |-  ( ( ( bits |` NN0 ) : NN0 -1-1-> ( ~P NN0 i^i Fin ) /\ ( ( -u x - 1 ) e. NN0 /\ ( -u y - 1 ) e. NN0 ) ) -> ( ( ( bits |` NN0 ) ` ( -u x - 1 ) ) = ( ( bits |` NN0 ) ` ( -u y - 1 ) ) <-> ( -u x - 1 ) = ( -u y - 1 ) ) )
56 54 55 mpan 
 |-  ( ( ( -u x - 1 ) e. NN0 /\ ( -u y - 1 ) e. NN0 ) -> ( ( ( bits |` NN0 ) ` ( -u x - 1 ) ) = ( ( bits |` NN0 ) ` ( -u y - 1 ) ) <-> ( -u x - 1 ) = ( -u y - 1 ) ) )
57 19 49 56 syl2anc 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( -u x e. NN /\ ( bits ` x ) = ( bits ` y ) ) ) -> ( ( ( bits |` NN0 ) ` ( -u x - 1 ) ) = ( ( bits |` NN0 ) ` ( -u y - 1 ) ) <-> ( -u x - 1 ) = ( -u y - 1 ) ) )
58 51 57 mpbid 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( -u x e. NN /\ ( bits ` x ) = ( bits ` y ) ) ) -> ( -u x - 1 ) = ( -u y - 1 ) )
59 8 9 10 58 subcan2d 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( -u x e. NN /\ ( bits ` x ) = ( bits ` y ) ) ) -> -u x = -u y )
60 4 7 59 neg11d 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( -u x e. NN /\ ( bits ` x ) = ( bits ` y ) ) ) -> x = y )
61 60 expr 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ -u x e. NN ) -> ( ( bits ` x ) = ( bits ` y ) -> x = y ) )
62 3 negnegd 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> -u -u x = x )
63 62 eleq1d 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( -u -u x e. NN0 <-> x e. NN0 ) )
64 63 biimpa 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ -u -u x e. NN0 ) -> x e. NN0 )
65 simprr 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x e. NN0 /\ ( bits ` x ) = ( bits ` y ) ) ) -> ( bits ` x ) = ( bits ` y ) )
66 fvres 
 |-  ( x e. NN0 -> ( ( bits |` NN0 ) ` x ) = ( bits ` x ) )
67 66 ad2antrl 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x e. NN0 /\ ( bits ` x ) = ( bits ` y ) ) ) -> ( ( bits |` NN0 ) ` x ) = ( bits ` x ) )
68 15 ad2antlr 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x e. NN0 /\ ( bits ` x ) = ( bits ` y ) ) ) -> ( NN0 \ ( bits ` y ) ) = ( bits ` ( -u y - 1 ) ) )
69 bitsfi 
 |-  ( x e. NN0 -> ( bits ` x ) e. Fin )
70 69 ad2antrl 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x e. NN0 /\ ( bits ` x ) = ( bits ` y ) ) ) -> ( bits ` x ) e. Fin )
71 65 70 eqeltrrd 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x e. NN0 /\ ( bits ` x ) = ( bits ` y ) ) ) -> ( bits ` y ) e. Fin )
72 difinf 
 |-  ( ( -. NN0 e. Fin /\ ( bits ` y ) e. Fin ) -> -. ( NN0 \ ( bits ` y ) ) e. Fin )
73 27 71 72 sylancr 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x e. NN0 /\ ( bits ` x ) = ( bits ` y ) ) ) -> -. ( NN0 \ ( bits ` y ) ) e. Fin )
74 68 73 eqneltrrd 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x e. NN0 /\ ( bits ` x ) = ( bits ` y ) ) ) -> -. ( bits ` ( -u y - 1 ) ) e. Fin )
75 bitsfi 
 |-  ( ( -u y - 1 ) e. NN0 -> ( bits ` ( -u y - 1 ) ) e. Fin )
76 74 75 nsyl 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x e. NN0 /\ ( bits ` x ) = ( bits ` y ) ) ) -> -. ( -u y - 1 ) e. NN0 )
77 76 48 nsyl 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x e. NN0 /\ ( bits ` x ) = ( bits ` y ) ) ) -> -. -u y e. NN )
78 44 adantr 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x e. NN0 /\ ( bits ` x ) = ( bits ` y ) ) ) -> ( -u y e. NN \/ y e. NN0 ) )
79 78 ord 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x e. NN0 /\ ( bits ` x ) = ( bits ` y ) ) ) -> ( -. -u y e. NN -> y e. NN0 ) )
80 77 79 mpd 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x e. NN0 /\ ( bits ` x ) = ( bits ` y ) ) ) -> y e. NN0 )
81 80 fvresd 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x e. NN0 /\ ( bits ` x ) = ( bits ` y ) ) ) -> ( ( bits |` NN0 ) ` y ) = ( bits ` y ) )
82 65 67 81 3eqtr4d 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x e. NN0 /\ ( bits ` x ) = ( bits ` y ) ) ) -> ( ( bits |` NN0 ) ` x ) = ( ( bits |` NN0 ) ` y ) )
83 simprl 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x e. NN0 /\ ( bits ` x ) = ( bits ` y ) ) ) -> x e. NN0 )
84 f1fveq 
 |-  ( ( ( bits |` NN0 ) : NN0 -1-1-> ( ~P NN0 i^i Fin ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> ( ( ( bits |` NN0 ) ` x ) = ( ( bits |` NN0 ) ` y ) <-> x = y ) )
85 54 84 mpan 
 |-  ( ( x e. NN0 /\ y e. NN0 ) -> ( ( ( bits |` NN0 ) ` x ) = ( ( bits |` NN0 ) ` y ) <-> x = y ) )
86 83 80 85 syl2anc 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x e. NN0 /\ ( bits ` x ) = ( bits ` y ) ) ) -> ( ( ( bits |` NN0 ) ` x ) = ( ( bits |` NN0 ) ` y ) <-> x = y ) )
87 82 86 mpbid 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x e. NN0 /\ ( bits ` x ) = ( bits ` y ) ) ) -> x = y )
88 87 expr 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ x e. NN0 ) -> ( ( bits ` x ) = ( bits ` y ) -> x = y ) )
89 64 88 syldan 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ -u -u x e. NN0 ) -> ( ( bits ` x ) = ( bits ` y ) -> x = y ) )
90 2 znegcld 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> -u x e. ZZ )
91 elznn 
 |-  ( -u x e. ZZ <-> ( -u x e. RR /\ ( -u x e. NN \/ -u -u x e. NN0 ) ) )
92 91 simprbi 
 |-  ( -u x e. ZZ -> ( -u x e. NN \/ -u -u x e. NN0 ) )
93 90 92 syl 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( -u x e. NN \/ -u -u x e. NN0 ) )
94 61 89 93 mpjaodan 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( ( bits ` x ) = ( bits ` y ) -> x = y ) )
95 94 rgen2 
 |-  A. x e. ZZ A. y e. ZZ ( ( bits ` x ) = ( bits ` y ) -> x = y )
96 dff13 
 |-  ( bits : ZZ -1-1-> ~P NN0 <-> ( bits : ZZ --> ~P NN0 /\ A. x e. ZZ A. y e. ZZ ( ( bits ` x ) = ( bits ` y ) -> x = y ) ) )
97 1 95 96 mpbir2an 
 |-  bits : ZZ -1-1-> ~P NN0