Metamath Proof Explorer

Theorem bitsf1ocnv

Description: The bits function restricted to nonnegative integers is a bijection from the integers to the finite sets of integers. It is in fact the inverse of the Ackermann bijection ackbijnn . (Contributed by Mario Carneiro, 8-Sep-2016)

Ref Expression
Assertion bitsf1ocnv 
|- ( ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) /\ `' ( bits |` NN0 ) = ( x e. ( ~P NN0 i^i Fin ) |-> sum_ n e. x ( 2 ^ n ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( k e. NN0 |-> ( bits ` k ) ) = ( k e. NN0 |-> ( bits ` k ) )
2 bitsss 
 |-  ( bits ` k ) C_ NN0
3 2 a1i 
 |-  ( k e. NN0 -> ( bits ` k ) C_ NN0 )
4 bitsfi 
 |-  ( k e. NN0 -> ( bits ` k ) e. Fin )
5 elfpw 
 |-  ( ( bits ` k ) e. ( ~P NN0 i^i Fin ) <-> ( ( bits ` k ) C_ NN0 /\ ( bits ` k ) e. Fin ) )
6 3 4 5 sylanbrc 
 |-  ( k e. NN0 -> ( bits ` k ) e. ( ~P NN0 i^i Fin ) )
7 6 adantl 
 |-  ( ( T. /\ k e. NN0 ) -> ( bits ` k ) e. ( ~P NN0 i^i Fin ) )
8 elinel2 
 |-  ( x e. ( ~P NN0 i^i Fin ) -> x e. Fin )
9 2nn0 
 |-  2 e. NN0
10 9 a1i 
 |-  ( ( x e. ( ~P NN0 i^i Fin ) /\ n e. x ) -> 2 e. NN0 )
11 elfpw 
 |-  ( x e. ( ~P NN0 i^i Fin ) <-> ( x C_ NN0 /\ x e. Fin ) )
12 11 simplbi 
 |-  ( x e. ( ~P NN0 i^i Fin ) -> x C_ NN0 )
13 12 sselda 
 |-  ( ( x e. ( ~P NN0 i^i Fin ) /\ n e. x ) -> n e. NN0 )
14 10 13 nn0expcld 
 |-  ( ( x e. ( ~P NN0 i^i Fin ) /\ n e. x ) -> ( 2 ^ n ) e. NN0 )
15 8 14 fsumnn0cl 
 |-  ( x e. ( ~P NN0 i^i Fin ) -> sum_ n e. x ( 2 ^ n ) e. NN0 )
16 15 adantl 
 |-  ( ( T. /\ x e. ( ~P NN0 i^i Fin ) ) -> sum_ n e. x ( 2 ^ n ) e. NN0 )
17 bitsinv2 
 |-  ( x e. ( ~P NN0 i^i Fin ) -> ( bits ` sum_ n e. x ( 2 ^ n ) ) = x )
18 17 eqcomd 
 |-  ( x e. ( ~P NN0 i^i Fin ) -> x = ( bits ` sum_ n e. x ( 2 ^ n ) ) )
19 18 ad2antll 
 |-  ( ( T. /\ ( k e. NN0 /\ x e. ( ~P NN0 i^i Fin ) ) ) -> x = ( bits ` sum_ n e. x ( 2 ^ n ) ) )
20 fveq2 
 |-  ( k = sum_ n e. x ( 2 ^ n ) -> ( bits ` k ) = ( bits ` sum_ n e. x ( 2 ^ n ) ) )
21 20 eqeq2d 
 |-  ( k = sum_ n e. x ( 2 ^ n ) -> ( x = ( bits ` k ) <-> x = ( bits ` sum_ n e. x ( 2 ^ n ) ) ) )
22 19 21 syl5ibrcom 
 |-  ( ( T. /\ ( k e. NN0 /\ x e. ( ~P NN0 i^i Fin ) ) ) -> ( k = sum_ n e. x ( 2 ^ n ) -> x = ( bits ` k ) ) )
23 bitsinv1 
 |-  ( k e. NN0 -> sum_ n e. ( bits ` k ) ( 2 ^ n ) = k )
24 23 eqcomd 
 |-  ( k e. NN0 -> k = sum_ n e. ( bits ` k ) ( 2 ^ n ) )
25 24 ad2antrl 
 |-  ( ( T. /\ ( k e. NN0 /\ x e. ( ~P NN0 i^i Fin ) ) ) -> k = sum_ n e. ( bits ` k ) ( 2 ^ n ) )
26 sumeq1 
 |-  ( x = ( bits ` k ) -> sum_ n e. x ( 2 ^ n ) = sum_ n e. ( bits ` k ) ( 2 ^ n ) )
27 26 eqeq2d 
 |-  ( x = ( bits ` k ) -> ( k = sum_ n e. x ( 2 ^ n ) <-> k = sum_ n e. ( bits ` k ) ( 2 ^ n ) ) )
28 25 27 syl5ibrcom 
 |-  ( ( T. /\ ( k e. NN0 /\ x e. ( ~P NN0 i^i Fin ) ) ) -> ( x = ( bits ` k ) -> k = sum_ n e. x ( 2 ^ n ) ) )
29 22 28 impbid 
 |-  ( ( T. /\ ( k e. NN0 /\ x e. ( ~P NN0 i^i Fin ) ) ) -> ( k = sum_ n e. x ( 2 ^ n ) <-> x = ( bits ` k ) ) )
30 1 7 16 29 f1ocnv2d 
 |-  ( T. -> ( ( k e. NN0 |-> ( bits ` k ) ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) /\ `' ( k e. NN0 |-> ( bits ` k ) ) = ( x e. ( ~P NN0 i^i Fin ) |-> sum_ n e. x ( 2 ^ n ) ) ) )
31 30 simpld 
 |-  ( T. -> ( k e. NN0 |-> ( bits ` k ) ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) )
32 bitsf 
 |-  bits : ZZ --> ~P NN0
33 32 a1i 
 |-  ( T. -> bits : ZZ --> ~P NN0 )
34 33 feqmptd 
 |-  ( T. -> bits = ( k e. ZZ |-> ( bits ` k ) ) )
35 34 reseq1d 
 |-  ( T. -> ( bits |` NN0 ) = ( ( k e. ZZ |-> ( bits ` k ) ) |` NN0 ) )
36 nn0ssz 
 |-  NN0 C_ ZZ
37 resmpt 
 |-  ( NN0 C_ ZZ -> ( ( k e. ZZ |-> ( bits ` k ) ) |` NN0 ) = ( k e. NN0 |-> ( bits ` k ) ) )
38 36 37 ax-mp 
 |-  ( ( k e. ZZ |-> ( bits ` k ) ) |` NN0 ) = ( k e. NN0 |-> ( bits ` k ) )
39 35 38 eqtrdi 
 |-  ( T. -> ( bits |` NN0 ) = ( k e. NN0 |-> ( bits ` k ) ) )
40 39 f1oeq1d 
 |-  ( T. -> ( ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) <-> ( k e. NN0 |-> ( bits ` k ) ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) ) )
41 31 40 mpbird 
 |-  ( T. -> ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) )
42 39 cnveqd 
 |-  ( T. -> `' ( bits |` NN0 ) = `' ( k e. NN0 |-> ( bits ` k ) ) )
43 30 simprd 
 |-  ( T. -> `' ( k e. NN0 |-> ( bits ` k ) ) = ( x e. ( ~P NN0 i^i Fin ) |-> sum_ n e. x ( 2 ^ n ) ) )
44 42 43 eqtrd 
 |-  ( T. -> `' ( bits |` NN0 ) = ( x e. ( ~P NN0 i^i Fin ) |-> sum_ n e. x ( 2 ^ n ) ) )
45 41 44 jca 
 |-  ( T. -> ( ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) /\ `' ( bits |` NN0 ) = ( x e. ( ~P NN0 i^i Fin ) |-> sum_ n e. x ( 2 ^ n ) ) ) )
46 45 mptru 
 |-  ( ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) /\ `' ( bits |` NN0 ) = ( x e. ( ~P NN0 i^i Fin ) |-> sum_ n e. x ( 2 ^ n ) ) )