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 : ℤ \underset{1-1}{⟶} 𝒫 ℕ_{0}$

Proof

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

Metamath Proof Explorer

Theorem bitsf1

Proof