Theorem bitsf1 16373

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

Assertion

Ref	Expression
bitsf1	⊢ bits:ℤ–1-1→𝒫 ℕ0

Proof of Theorem bitsf1

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		bitsf 16354	. 2 ⊢ bits:ℤ⟶𝒫 ℕ0
2		simpl 482	. . . . . . . 8 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → 𝑥 ∈ ℤ)
3	2	zcnd 12597	. . . . . . 7 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → 𝑥 ∈ ℂ)
4	3	adantr 480	. . . . . 6 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → 𝑥 ∈ ℂ)
5		simpr 484	. . . . . . . 8 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → 𝑦 ∈ ℤ)
6	5	zcnd 12597	. . . . . . 7 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → 𝑦 ∈ ℂ)
7	6	adantr 480	. . . . . 6 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → 𝑦 ∈ ℂ)
8	4	negcld 11479	. . . . . . 7 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → -𝑥 ∈ ℂ)
9	7	negcld 11479	. . . . . . 7 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → -𝑦 ∈ ℂ)
10		1cnd 11127	. . . . . . 7 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → 1 ∈ ℂ)
11		simprr 772	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → (bits‘𝑥) = (bits‘𝑦))
12	11	difeq2d 4078	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → (ℕ0 ∖ (bits‘𝑥)) = (ℕ0 ∖ (bits‘𝑦)))
13		bitscmp 16365	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℤ → (ℕ0 ∖ (bits‘𝑥)) = (bits‘(-𝑥 − 1)))
14	13	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → (ℕ0 ∖ (bits‘𝑥)) = (bits‘(-𝑥 − 1)))
15		bitscmp 16365	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℤ → (ℕ0 ∖ (bits‘𝑦)) = (bits‘(-𝑦 − 1)))
16	15	ad2antlr 727	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → (ℕ0 ∖ (bits‘𝑦)) = (bits‘(-𝑦 − 1)))
17	12, 14, 16	3eqtr3d 2779	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → (bits‘(-𝑥 − 1)) = (bits‘(-𝑦 − 1)))
18		nnm1nn0 12442	. . . . . . . . . . 11 ⊢ (-𝑥 ∈ ℕ → (-𝑥 − 1) ∈ ℕ0)
19	18	ad2antrl 728	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → (-𝑥 − 1) ∈ ℕ0)
20	19	fvresd 6854	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → ((bits ↾ ℕ0)‘(-𝑥 − 1)) = (bits‘(-𝑥 − 1)))
21		ominf 9164	. . . . . . . . . . . . . . . . 17 ⊢ ¬ ω ∈ Fin
22		nn0ennn 13902	. . . . . . . . . . . . . . . . . . 19 ⊢ ℕ0 ≈ ℕ
23		nnenom 13903	. . . . . . . . . . . . . . . . . . 19 ⊢ ℕ ≈ ω
24	22, 23	entr2i 8946	. . . . . . . . . . . . . . . . . 18 ⊢ ω ≈ ℕ0
25		enfii 9110	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℕ0 ∈ Fin ∧ ω ≈ ℕ0) → ω ∈ Fin)
26	24, 25	mpan2 691	. . . . . . . . . . . . . . . . 17 ⊢ (ℕ0 ∈ Fin → ω ∈ Fin)
27	21, 26	mto 197	. . . . . . . . . . . . . . . 16 ⊢ ¬ ℕ0 ∈ Fin
28		difinf 9211	. . . . . . . . . . . . . . . 16 ⊢ ((¬ ℕ0 ∈ Fin ∧ (bits‘𝑥) ∈ Fin) → ¬ (ℕ0 ∖ (bits‘𝑥)) ∈ Fin)
29	27, 28	mpan 690	. . . . . . . . . . . . . . 15 ⊢ ((bits‘𝑥) ∈ Fin → ¬ (ℕ0 ∖ (bits‘𝑥)) ∈ Fin)
30		bitsfi 16364	. . . . . . . . . . . . . . . . 17 ⊢ ((-𝑥 − 1) ∈ ℕ0 → (bits‘(-𝑥 − 1)) ∈ Fin)
31	19, 30	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → (bits‘(-𝑥 − 1)) ∈ Fin)
32	14, 31	eqeltrd 2836	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → (ℕ0 ∖ (bits‘𝑥)) ∈ Fin)
33	29, 32	nsyl3 138	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → ¬ (bits‘𝑥) ∈ Fin)
34	11, 33	eqneltrrd 2857	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → ¬ (bits‘𝑦) ∈ Fin)
35		bitsfi 16364	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ0 → (bits‘𝑦) ∈ Fin)
36	34, 35	nsyl 140	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → ¬ 𝑦 ∈ ℕ0)
37	5	znegcld 12598	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → -𝑦 ∈ ℤ)
38		elznn 12504	. . . . . . . . . . . . . . . . 17 ⊢ (-𝑦 ∈ ℤ ↔ (-𝑦 ∈ ℝ ∧ (-𝑦 ∈ ℕ ∨ --𝑦 ∈ ℕ0)))
39	38	simprbi 496	. . . . . . . . . . . . . . . 16 ⊢ (-𝑦 ∈ ℤ → (-𝑦 ∈ ℕ ∨ --𝑦 ∈ ℕ0))
40	37, 39	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (-𝑦 ∈ ℕ ∨ --𝑦 ∈ ℕ0))
41	6	negnegd 11483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → --𝑦 = 𝑦)
42	41	eleq1d 2821	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (--𝑦 ∈ ℕ0 ↔ 𝑦 ∈ ℕ0))
43	42	orbi2d 915	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((-𝑦 ∈ ℕ ∨ --𝑦 ∈ ℕ0) ↔ (-𝑦 ∈ ℕ ∨ 𝑦 ∈ ℕ0)))
44	40, 43	mpbid 232	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (-𝑦 ∈ ℕ ∨ 𝑦 ∈ ℕ0))
45	44	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → (-𝑦 ∈ ℕ ∨ 𝑦 ∈ ℕ0))
46	45	ord 864	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → (¬ -𝑦 ∈ ℕ → 𝑦 ∈ ℕ0))
47	36, 46	mt3d 148	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → -𝑦 ∈ ℕ)
48		nnm1nn0 12442	. . . . . . . . . . 11 ⊢ (-𝑦 ∈ ℕ → (-𝑦 − 1) ∈ ℕ0)
49	47, 48	syl 17	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → (-𝑦 − 1) ∈ ℕ0)
50	49	fvresd 6854	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → ((bits ↾ ℕ0)‘(-𝑦 − 1)) = (bits‘(-𝑦 − 1)))
51	17, 20, 50	3eqtr4d 2781	. . . . . . . 8 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → ((bits ↾ ℕ0)‘(-𝑥 − 1)) = ((bits ↾ ℕ0)‘(-𝑦 − 1)))
52		bitsf1o 16372	. . . . . . . . . . 11 ⊢ (bits ↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
53		f1of1 6773	. . . . . . . . . . 11 ⊢ ((bits ↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin) → (bits ↾ ℕ0):ℕ0–1-1→(𝒫 ℕ0 ∩ Fin))
54	52, 53	ax-mp 5	. . . . . . . . . 10 ⊢ (bits ↾ ℕ0):ℕ0–1-1→(𝒫 ℕ0 ∩ Fin)
55		f1fveq 7208	. . . . . . . . . 10 ⊢ (((bits ↾ ℕ0):ℕ0–1-1→(𝒫 ℕ0 ∩ Fin) ∧ ((-𝑥 − 1) ∈ ℕ0 ∧ (-𝑦 − 1) ∈ ℕ0)) → (((bits ↾ ℕ0)‘(-𝑥 − 1)) = ((bits ↾ ℕ0)‘(-𝑦 − 1)) ↔ (-𝑥 − 1) = (-𝑦 − 1)))
56	54, 55	mpan 690	. . . . . . . . 9 ⊢ (((-𝑥 − 1) ∈ ℕ0 ∧ (-𝑦 − 1) ∈ ℕ0) → (((bits ↾ ℕ0)‘(-𝑥 − 1)) = ((bits ↾ ℕ0)‘(-𝑦 − 1)) ↔ (-𝑥 − 1) = (-𝑦 − 1)))
57	19, 49, 56	syl2anc 584	. . . . . . . 8 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → (((bits ↾ ℕ0)‘(-𝑥 − 1)) = ((bits ↾ ℕ0)‘(-𝑦 − 1)) ↔ (-𝑥 − 1) = (-𝑦 − 1)))
58	51, 57	mpbid 232	. . . . . . 7 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → (-𝑥 − 1) = (-𝑦 − 1))
59	8, 9, 10, 58	subcan2d 11534	. . . . . 6 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → -𝑥 = -𝑦)
60	4, 7, 59	neg11d 11504	. . . . 5 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → 𝑥 = 𝑦)
61	60	expr 456	. . . 4 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ -𝑥 ∈ ℕ) → ((bits‘𝑥) = (bits‘𝑦) → 𝑥 = 𝑦))
62	3	negnegd 11483	. . . . . . 7 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → --𝑥 = 𝑥)
63	62	eleq1d 2821	. . . . . 6 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (--𝑥 ∈ ℕ0 ↔ 𝑥 ∈ ℕ0))
64	63	biimpa 476	. . . . 5 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ --𝑥 ∈ ℕ0) → 𝑥 ∈ ℕ0)
65		simprr 772	. . . . . . . 8 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0 ∧ (bits‘𝑥) = (bits‘𝑦))) → (bits‘𝑥) = (bits‘𝑦))
66		fvres 6853	. . . . . . . . 9 ⊢ (𝑥 ∈ ℕ0 → ((bits ↾ ℕ0)‘𝑥) = (bits‘𝑥))
67	66	ad2antrl 728	. . . . . . . 8 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0 ∧ (bits‘𝑥) = (bits‘𝑦))) → ((bits ↾ ℕ0)‘𝑥) = (bits‘𝑥))
68	15	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0 ∧ (bits‘𝑥) = (bits‘𝑦))) → (ℕ0 ∖ (bits‘𝑦)) = (bits‘(-𝑦 − 1)))
69		bitsfi 16364	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℕ0 → (bits‘𝑥) ∈ Fin)
70	69	ad2antrl 728	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0 ∧ (bits‘𝑥) = (bits‘𝑦))) → (bits‘𝑥) ∈ Fin)
71	65, 70	eqeltrrd 2837	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0 ∧ (bits‘𝑥) = (bits‘𝑦))) → (bits‘𝑦) ∈ Fin)
72		difinf 9211	. . . . . . . . . . . . . 14 ⊢ ((¬ ℕ0 ∈ Fin ∧ (bits‘𝑦) ∈ Fin) → ¬ (ℕ0 ∖ (bits‘𝑦)) ∈ Fin)
73	27, 71, 72	sylancr 587	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0 ∧ (bits‘𝑥) = (bits‘𝑦))) → ¬ (ℕ0 ∖ (bits‘𝑦)) ∈ Fin)
74	68, 73	eqneltrrd 2857	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0 ∧ (bits‘𝑥) = (bits‘𝑦))) → ¬ (bits‘(-𝑦 − 1)) ∈ Fin)
75		bitsfi 16364	. . . . . . . . . . . 12 ⊢ ((-𝑦 − 1) ∈ ℕ0 → (bits‘(-𝑦 − 1)) ∈ Fin)
76	74, 75	nsyl 140	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0 ∧ (bits‘𝑥) = (bits‘𝑦))) → ¬ (-𝑦 − 1) ∈ ℕ0)
77	76, 48	nsyl 140	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0 ∧ (bits‘𝑥) = (bits‘𝑦))) → ¬ -𝑦 ∈ ℕ)
78	44	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0 ∧ (bits‘𝑥) = (bits‘𝑦))) → (-𝑦 ∈ ℕ ∨ 𝑦 ∈ ℕ0))
79	78	ord 864	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0 ∧ (bits‘𝑥) = (bits‘𝑦))) → (¬ -𝑦 ∈ ℕ → 𝑦 ∈ ℕ0))
80	77, 79	mpd 15	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0 ∧ (bits‘𝑥) = (bits‘𝑦))) → 𝑦 ∈ ℕ0)
81	80	fvresd 6854	. . . . . . . 8 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0 ∧ (bits‘𝑥) = (bits‘𝑦))) → ((bits ↾ ℕ0)‘𝑦) = (bits‘𝑦))
82	65, 67, 81	3eqtr4d 2781	. . . . . . 7 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0 ∧ (bits‘𝑥) = (bits‘𝑦))) → ((bits ↾ ℕ0)‘𝑥) = ((bits ↾ ℕ0)‘𝑦))
83		simprl 770	. . . . . . . 8 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0 ∧ (bits‘𝑥) = (bits‘𝑦))) → 𝑥 ∈ ℕ0)
84		f1fveq 7208	. . . . . . . . 9 ⊢ (((bits ↾ ℕ0):ℕ0–1-1→(𝒫 ℕ0 ∩ Fin) ∧ (𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0)) → (((bits ↾ ℕ0)‘𝑥) = ((bits ↾ ℕ0)‘𝑦) ↔ 𝑥 = 𝑦))
85	54, 84	mpan 690	. . . . . . . 8 ⊢ ((𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → (((bits ↾ ℕ0)‘𝑥) = ((bits ↾ ℕ0)‘𝑦) ↔ 𝑥 = 𝑦))
86	83, 80, 85	syl2anc 584	. . . . . . 7 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0 ∧ (bits‘𝑥) = (bits‘𝑦))) → (((bits ↾ ℕ0)‘𝑥) = ((bits ↾ ℕ0)‘𝑦) ↔ 𝑥 = 𝑦))
87	82, 86	mpbid 232	. . . . . 6 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ0 ∧ (bits‘𝑥) = (bits‘𝑦))) → 𝑥 = 𝑦)
88	87	expr 456	. . . . 5 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ 𝑥 ∈ ℕ0) → ((bits‘𝑥) = (bits‘𝑦) → 𝑥 = 𝑦))
89	64, 88	syldan 591	. . . 4 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ --𝑥 ∈ ℕ0) → ((bits‘𝑥) = (bits‘𝑦) → 𝑥 = 𝑦))
90	2	znegcld 12598	. . . . 5 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → -𝑥 ∈ ℤ)
91		elznn 12504	. . . . . 6 ⊢ (-𝑥 ∈ ℤ ↔ (-𝑥 ∈ ℝ ∧ (-𝑥 ∈ ℕ ∨ --𝑥 ∈ ℕ0)))
92	91	simprbi 496	. . . . 5 ⊢ (-𝑥 ∈ ℤ → (-𝑥 ∈ ℕ ∨ --𝑥 ∈ ℕ0))
93	90, 92	syl 17	. . . 4 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (-𝑥 ∈ ℕ ∨ --𝑥 ∈ ℕ0))
94	61, 89, 93	mpjaodan 960	. . 3 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((bits‘𝑥) = (bits‘𝑦) → 𝑥 = 𝑦))
95	94	rgen2 3176	. 2 ⊢ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ ((bits‘𝑥) = (bits‘𝑦) → 𝑥 = 𝑦)
96		dff13 7200	. 2 ⊢ (bits:ℤ–1-1→𝒫 ℕ0 ↔ (bits:ℤ⟶𝒫 ℕ0 ∧ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ ((bits‘𝑥) = (bits‘𝑦) → 𝑥 = 𝑦)))
97	1, 95, 96	mpbir2an 711	1 ⊢ bits:ℤ–1-1→𝒫 ℕ0

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1541   ∈ wcel 2113  ∀wral 3051   ∖ cdif 3898   ∩ cin 3900  𝒫 cpw 4554   class class class wbr 5098   ↾ cres 5626  ⟶wf 6488  –1-1→wf1 6489  –1-1-onto→wf1o 6491  ‘cfv 6492  (class class class)co 7358  ωcom 7808   ≈ cen 8880  Fincfn 8883  ℂcc 11024  ℝcr 11025  1c1 11027   − cmin 11364  -cneg 11365  ℕcn 12145  ℕ₀cn0 12401  ℤcz 12488  bitscbits 16346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-rep 5224  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-inf2 9550  ax-cnex 11082  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102  ax-pre-mulgt0 11103  ax-pre-sup 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3350  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-int 4903  df-iun 4948  df-disj 5066  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-se 5578  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-isom 6501  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-1st 7933  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-1o 8397  df-2o 8398  df-oadd 8401  df-er 8635  df-map 8765  df-pm 8766  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-sup 9345  df-inf 9346  df-oi 9415  df-dju 9813  df-card 9851  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-sub 11366  df-neg 11367  df-div 11795  df-nn 12146  df-2 12208  df-3 12209  df-n0 12402  df-xnn0 12475  df-z 12489  df-uz 12752  df-rp 12906  df-fz 13424  df-fzo 13571  df-fl 13712  df-mod 13790  df-seq 13925  df-exp 13985  df-hash 14254  df-cj 15022  df-re 15023  df-im 15024  df-sqrt 15158  df-abs 15159  df-clim 15411  df-sum 15610  df-dvds 16180  df-bits 16349

This theorem is referenced by:  bitsuz  16401  eulerpartlemmf  34532