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 : ℤ –1-1→ 𝒫 ℕ0

Proof

Step Hyp Ref Expression
1 bitsf ⊢ bits : ℤ ⟶ 𝒫 ℕ0
2 simpl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → 𝑥 ∈ ℤ )
3 2 zcnd ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → 𝑥 ∈ ℂ )
4 3 adantr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( - 𝑥 ∈ ℕ ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → 𝑥 ∈ ℂ )
5 simpr ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → 𝑦 ∈ ℤ )
6 5 zcnd ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → 𝑦 ∈ ℂ )
7 6 adantr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( - 𝑥 ∈ ℕ ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → 𝑦 ∈ ℂ )
8 4 negcld ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( - 𝑥 ∈ ℕ ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → - 𝑥 ∈ ℂ )
9 7 negcld ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( - 𝑥 ∈ ℕ ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → - 𝑦 ∈ ℂ )
10 1cnd ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( - 𝑥 ∈ ℕ ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → 1 ∈ ℂ )
11 simprr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( - 𝑥 ∈ ℕ ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) )
12 11 difeq2d ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( - 𝑥 ∈ ℕ ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ( ℕ0 ∖ ( bits ‘ 𝑥 ) ) = ( ℕ0 ∖ ( bits ‘ 𝑦 ) ) )
13 bitscmp ⊢ ( 𝑥 ∈ ℤ → ( ℕ0 ∖ ( bits ‘ 𝑥 ) ) = ( bits ‘ ( - 𝑥 − 1 ) ) )
14 13 ad2antrr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( - 𝑥 ∈ ℕ ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ( ℕ0 ∖ ( bits ‘ 𝑥 ) ) = ( bits ‘ ( - 𝑥 − 1 ) ) )
15 bitscmp ⊢ ( 𝑦 ∈ ℤ → ( ℕ0 ∖ ( bits ‘ 𝑦 ) ) = ( bits ‘ ( - 𝑦 − 1 ) ) )
16 15 ad2antlr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( - 𝑥 ∈ ℕ ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ( ℕ0 ∖ ( bits ‘ 𝑦 ) ) = ( bits ‘ ( - 𝑦 − 1 ) ) )
17 12 14 16 3eqtr3d ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( - 𝑥 ∈ ℕ ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ( bits ‘ ( - 𝑥 − 1 ) ) = ( bits ‘ ( - 𝑦 − 1 ) ) )
18 nnm1nn0 ⊢ ( - 𝑥 ∈ ℕ → ( - 𝑥 − 1 ) ∈ ℕ0 )
19 18 ad2antrl ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( - 𝑥 ∈ ℕ ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ( - 𝑥 − 1 ) ∈ ℕ0 )
20 19 fvresd ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( - 𝑥 ∈ ℕ ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ( ( bits ↾ ℕ0 ) ‘ ( - 𝑥 − 1 ) ) = ( bits ‘ ( - 𝑥 − 1 ) ) )
21 ominf ⊢ ¬ ω ∈ Fin
22 nn0ennn ⊢ ℕ0 ≈ ℕ
23 nnenom ⊢ ℕ ≈ ω
24 22 23 entr2i ⊢ ω ≈ ℕ0
25 enfii ⊢ ( ( ℕ0 ∈ Fin ∧ ω ≈ ℕ0 ) → ω ∈ Fin )
26 24 25 mpan2 ⊢ ( ℕ0 ∈ Fin → ω ∈ Fin )
27 21 26 mto ⊢ ¬ ℕ0 ∈ Fin
28 difinf ⊢ ( ( ¬ ℕ0 ∈ Fin ∧ ( bits ‘ 𝑥 ) ∈ Fin ) → ¬ ( ℕ0 ∖ ( bits ‘ 𝑥 ) ) ∈ Fin )
29 27 28 mpan ⊢ ( ( bits ‘ 𝑥 ) ∈ Fin → ¬ ( ℕ0 ∖ ( bits ‘ 𝑥 ) ) ∈ Fin )
30 bitsfi ⊢ ( ( - 𝑥 − 1 ) ∈ ℕ0 → ( bits ‘ ( - 𝑥 − 1 ) ) ∈ Fin )
31 19 30 syl ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( - 𝑥 ∈ ℕ ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ( bits ‘ ( - 𝑥 − 1 ) ) ∈ Fin )
32 14 31 eqeltrd ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( - 𝑥 ∈ ℕ ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ( ℕ0 ∖ ( bits ‘ 𝑥 ) ) ∈ Fin )
33 29 32 nsyl3 ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( - 𝑥 ∈ ℕ ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ¬ ( bits ‘ 𝑥 ) ∈ Fin )
34 11 33 eqneltrrd ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( - 𝑥 ∈ ℕ ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ¬ ( bits ‘ 𝑦 ) ∈ Fin )
35 bitsfi ⊢ ( 𝑦 ∈ ℕ0 → ( bits ‘ 𝑦 ) ∈ Fin )
36 34 35 nsyl ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( - 𝑥 ∈ ℕ ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ¬ 𝑦 ∈ ℕ0 )
37 5 znegcld ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → - 𝑦 ∈ ℤ )
38 elznn ⊢ ( - 𝑦 ∈ ℤ ↔ ( - 𝑦 ∈ ℝ ∧ ( - 𝑦 ∈ ℕ ∨ - - 𝑦 ∈ ℕ0 ) ) )
39 38 simprbi ⊢ ( - 𝑦 ∈ ℤ → ( - 𝑦 ∈ ℕ ∨ - - 𝑦 ∈ ℕ0 ) )
40 37 39 syl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( - 𝑦 ∈ ℕ ∨ - - 𝑦 ∈ ℕ0 ) )
41 6 negnegd ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → - - 𝑦 = 𝑦 )
42 41 eleq1d ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( - - 𝑦 ∈ ℕ0 ↔ 𝑦 ∈ ℕ0 ) )
43 42 orbi2d ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( - 𝑦 ∈ ℕ ∨ - - 𝑦 ∈ ℕ0 ) ↔ ( - 𝑦 ∈ ℕ ∨ 𝑦 ∈ ℕ0 ) ) )
44 40 43 mpbid ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( - 𝑦 ∈ ℕ ∨ 𝑦 ∈ ℕ0 ) )
45 44 adantr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( - 𝑥 ∈ ℕ ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ( - 𝑦 ∈ ℕ ∨ 𝑦 ∈ ℕ0 ) )
46 45 ord ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( - 𝑥 ∈ ℕ ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ( ¬ - 𝑦 ∈ ℕ → 𝑦 ∈ ℕ0 ) )
47 36 46 mt3d ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( - 𝑥 ∈ ℕ ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → - 𝑦 ∈ ℕ )
48 nnm1nn0 ⊢ ( - 𝑦 ∈ ℕ → ( - 𝑦 − 1 ) ∈ ℕ0 )
49 47 48 syl ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( - 𝑥 ∈ ℕ ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ( - 𝑦 − 1 ) ∈ ℕ0 )
50 49 fvresd ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( - 𝑥 ∈ ℕ ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ( ( bits ↾ ℕ0 ) ‘ ( - 𝑦 − 1 ) ) = ( bits ‘ ( - 𝑦 − 1 ) ) )
51 17 20 50 3eqtr4d ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( - 𝑥 ∈ ℕ ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ( ( bits ↾ ℕ0 ) ‘ ( - 𝑥 − 1 ) ) = ( ( bits ↾ ℕ0 ) ‘ ( - 𝑦 − 1 ) ) )
52 bitsf1o ⊢ ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin )
53 f1of1 ⊢ ( ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) → ( bits ↾ ℕ0 ) : ℕ0 –1-1→ ( 𝒫 ℕ0 ∩ Fin ) )
54 52 53 ax-mp ⊢ ( bits ↾ ℕ0 ) : ℕ0 –1-1→ ( 𝒫 ℕ0 ∩ Fin )
55 f1fveq ⊢ ( ( ( bits ↾ ℕ0 ) : ℕ0 –1-1→ ( 𝒫 ℕ0 ∩ Fin ) ∧ ( ( - 𝑥 − 1 ) ∈ ℕ0 ∧ ( - 𝑦 − 1 ) ∈ ℕ0 ) ) → ( ( ( bits ↾ ℕ0 ) ‘ ( - 𝑥 − 1 ) ) = ( ( bits ↾ ℕ0 ) ‘ ( - 𝑦 − 1 ) ) ↔ ( - 𝑥 − 1 ) = ( - 𝑦 − 1 ) ) )
56 54 55 mpan ⊢ ( ( ( - 𝑥 − 1 ) ∈ ℕ0 ∧ ( - 𝑦 − 1 ) ∈ ℕ0 ) → ( ( ( bits ↾ ℕ0 ) ‘ ( - 𝑥 − 1 ) ) = ( ( bits ↾ ℕ0 ) ‘ ( - 𝑦 − 1 ) ) ↔ ( - 𝑥 − 1 ) = ( - 𝑦 − 1 ) ) )
57 19 49 56 syl2anc ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( - 𝑥 ∈ ℕ ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ( ( ( bits ↾ ℕ0 ) ‘ ( - 𝑥 − 1 ) ) = ( ( bits ↾ ℕ0 ) ‘ ( - 𝑦 − 1 ) ) ↔ ( - 𝑥 − 1 ) = ( - 𝑦 − 1 ) ) )
58 51 57 mpbid ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( - 𝑥 ∈ ℕ ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ( - 𝑥 − 1 ) = ( - 𝑦 − 1 ) )
59 8 9 10 58 subcan2d ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( - 𝑥 ∈ ℕ ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → - 𝑥 = - 𝑦 )
60 4 7 59 neg11d ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( - 𝑥 ∈ ℕ ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → 𝑥 = 𝑦 )
61 60 expr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ - 𝑥 ∈ ℕ ) → ( ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
62 3 negnegd ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → - - 𝑥 = 𝑥 )
63 62 eleq1d ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( - - 𝑥 ∈ ℕ0 ↔ 𝑥 ∈ ℕ0 ) )
64 63 biimpa ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ - - 𝑥 ∈ ℕ0 ) → 𝑥 ∈ ℕ0 )
65 simprr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 ∈ ℕ0 ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) )
66 fvres ⊢ ( 𝑥 ∈ ℕ0 → ( ( bits ↾ ℕ0 ) ‘ 𝑥 ) = ( bits ‘ 𝑥 ) )
67 66 ad2antrl ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 ∈ ℕ0 ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ( ( bits ↾ ℕ0 ) ‘ 𝑥 ) = ( bits ‘ 𝑥 ) )
68 15 ad2antlr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 ∈ ℕ0 ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ( ℕ0 ∖ ( bits ‘ 𝑦 ) ) = ( bits ‘ ( - 𝑦 − 1 ) ) )
69 bitsfi ⊢ ( 𝑥 ∈ ℕ0 → ( bits ‘ 𝑥 ) ∈ Fin )
70 69 ad2antrl ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 ∈ ℕ0 ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ( bits ‘ 𝑥 ) ∈ Fin )
71 65 70 eqeltrrd ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 ∈ ℕ0 ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ( bits ‘ 𝑦 ) ∈ Fin )
72 difinf ⊢ ( ( ¬ ℕ0 ∈ Fin ∧ ( bits ‘ 𝑦 ) ∈ Fin ) → ¬ ( ℕ0 ∖ ( bits ‘ 𝑦 ) ) ∈ Fin )
73 27 71 72 sylancr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 ∈ ℕ0 ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ¬ ( ℕ0 ∖ ( bits ‘ 𝑦 ) ) ∈ Fin )
74 68 73 eqneltrrd ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 ∈ ℕ0 ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ¬ ( bits ‘ ( - 𝑦 − 1 ) ) ∈ Fin )
75 bitsfi ⊢ ( ( - 𝑦 − 1 ) ∈ ℕ0 → ( bits ‘ ( - 𝑦 − 1 ) ) ∈ Fin )
76 74 75 nsyl ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 ∈ ℕ0 ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ¬ ( - 𝑦 − 1 ) ∈ ℕ0 )
77 76 48 nsyl ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 ∈ ℕ0 ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ¬ - 𝑦 ∈ ℕ )
78 44 adantr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 ∈ ℕ0 ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ( - 𝑦 ∈ ℕ ∨ 𝑦 ∈ ℕ0 ) )
79 78 ord ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 ∈ ℕ0 ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ( ¬ - 𝑦 ∈ ℕ → 𝑦 ∈ ℕ0 ) )
80 77 79 mpd ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 ∈ ℕ0 ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → 𝑦 ∈ ℕ0 )
81 80 fvresd ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 ∈ ℕ0 ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ( ( bits ↾ ℕ0 ) ‘ 𝑦 ) = ( bits ‘ 𝑦 ) )
82 65 67 81 3eqtr4d ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 ∈ ℕ0 ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ( ( bits ↾ ℕ0 ) ‘ 𝑥 ) = ( ( bits ↾ ℕ0 ) ‘ 𝑦 ) )
83 simprl ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 ∈ ℕ0 ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → 𝑥 ∈ ℕ0 )
84 f1fveq ⊢ ( ( ( bits ↾ ℕ0 ) : ℕ0 –1-1→ ( 𝒫 ℕ0 ∩ Fin ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( ( ( bits ↾ ℕ0 ) ‘ 𝑥 ) = ( ( bits ↾ ℕ0 ) ‘ 𝑦 ) ↔ 𝑥 = 𝑦 ) )
85 54 84 mpan ⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ( ( ( bits ↾ ℕ0 ) ‘ 𝑥 ) = ( ( bits ↾ ℕ0 ) ‘ 𝑦 ) ↔ 𝑥 = 𝑦 ) )
86 83 80 85 syl2anc ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 ∈ ℕ0 ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → ( ( ( bits ↾ ℕ0 ) ‘ 𝑥 ) = ( ( bits ↾ ℕ0 ) ‘ 𝑦 ) ↔ 𝑥 = 𝑦 ) )
87 82 86 mpbid ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 ∈ ℕ0 ∧ ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) ) ) → 𝑥 = 𝑦 )
88 87 expr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ 𝑥 ∈ ℕ0 ) → ( ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
89 64 88 syldan ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ - - 𝑥 ∈ ℕ0 ) → ( ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
90 2 znegcld ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → - 𝑥 ∈ ℤ )
91 elznn ⊢ ( - 𝑥 ∈ ℤ ↔ ( - 𝑥 ∈ ℝ ∧ ( - 𝑥 ∈ ℕ ∨ - - 𝑥 ∈ ℕ0 ) ) )
92 91 simprbi ⊢ ( - 𝑥 ∈ ℤ → ( - 𝑥 ∈ ℕ ∨ - - 𝑥 ∈ ℕ0 ) )
93 90 92 syl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( - 𝑥 ∈ ℕ ∨ - - 𝑥 ∈ ℕ0 ) )
94 61 89 93 mpjaodan ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
95 94 rgen2 ⊢ ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ℤ ( ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) → 𝑥 = 𝑦 )
96 dff13 ⊢ ( bits : ℤ –1-1→ 𝒫 ℕ0 ↔ ( bits : ℤ ⟶ 𝒫 ℕ0 ∧ ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ℤ ( ( bits ‘ 𝑥 ) = ( bits ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
97 1 95 96 mpbir2an ⊢ bits : ℤ –1-1→ 𝒫 ℕ0