bitsf1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > bitsf1		Structured version Visualization version GIF version

Theorem bitsf1 16383

Description: The bits function is an injection from ℤ to 𝒫 ℕ₀. It is obviously not a bijection (by Cantor's theorem canth2 9126), 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→𝒫 ℕ₀

Proof of Theorem bitsf1 Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		bitsf 16364	. 2 ⊢ bits:ℤ⟶𝒫 ℕ₀
2		simpl 483	. . . . . . . 8 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → 𝑥 ∈ ℤ)
3	2	zcnd 12663	. . . . . . 7 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → 𝑥 ∈ ℂ)
4	3	adantr 481	. . . . . 6 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → 𝑥 ∈ ℂ)
5		simpr 485	. . . . . . . 8 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → 𝑦 ∈ ℤ)
6	5	zcnd 12663	. . . . . . 7 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → 𝑦 ∈ ℂ)
7	6	adantr 481	. . . . . 6 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → 𝑦 ∈ ℂ)
8	4	negcld 11554	. . . . . . 7 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → -𝑥 ∈ ℂ)
9	7	negcld 11554	. . . . . . 7 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → -𝑦 ∈ ℂ)
10		1cnd 11205	. . . . . . 7 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → 1 ∈ ℂ)
11		simprr 771	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → (bits‘𝑥) = (bits‘𝑦))
12	11	difeq2d 4121	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → (ℕ₀ ∖ (bits‘𝑥)) = (ℕ₀ ∖ (bits‘𝑦)))
13		bitscmp 16375	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℤ → (ℕ₀ ∖ (bits‘𝑥)) = (bits‘(-𝑥 − 1)))
14	13	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → (ℕ₀ ∖ (bits‘𝑥)) = (bits‘(-𝑥 − 1)))
15		bitscmp 16375	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℤ → (ℕ₀ ∖ (bits‘𝑦)) = (bits‘(-𝑦 − 1)))
16	15	ad2antlr 725	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → (ℕ₀ ∖ (bits‘𝑦)) = (bits‘(-𝑦 − 1)))
17	12, 14, 16	3eqtr3d 2780	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → (bits‘(-𝑥 − 1)) = (bits‘(-𝑦 − 1)))
18		nnm1nn0 12509	. . . . . . . . . . 11 ⊢ (-𝑥 ∈ ℕ → (-𝑥 − 1) ∈ ℕ₀)
19	18	ad2antrl 726	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → (-𝑥 − 1) ∈ ℕ₀)
20	19	fvresd 6908	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → ((bits ↾ ℕ₀)‘(-𝑥 − 1)) = (bits‘(-𝑥 − 1)))
21		ominf 9254	. . . . . . . . . . . . . . . . 17 ⊢ ¬ ω ∈ Fin
22		nn0ennn 13940	. . . . . . . . . . . . . . . . . . 19 ⊢ ℕ₀ ≈ ℕ
23		nnenom 13941	. . . . . . . . . . . . . . . . . . 19 ⊢ ℕ ≈ ω
24	22, 23	entr2i 9001	. . . . . . . . . . . . . . . . . 18 ⊢ ω ≈ ℕ₀
25		enfii 9185	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℕ₀ ∈ Fin ∧ ω ≈ ℕ₀) → ω ∈ Fin)
26	24, 25	mpan2 689	. . . . . . . . . . . . . . . . 17 ⊢ (ℕ₀ ∈ Fin → ω ∈ Fin)
27	21, 26	mto 196	. . . . . . . . . . . . . . . 16 ⊢ ¬ ℕ₀ ∈ Fin
28		difinf 9312	. . . . . . . . . . . . . . . 16 ⊢ ((¬ ℕ₀ ∈ Fin ∧ (bits‘𝑥) ∈ Fin) → ¬ (ℕ₀ ∖ (bits‘𝑥)) ∈ Fin)
29	27, 28	mpan 688	. . . . . . . . . . . . . . 15 ⊢ ((bits‘𝑥) ∈ Fin → ¬ (ℕ₀ ∖ (bits‘𝑥)) ∈ Fin)
30		bitsfi 16374	. . . . . . . . . . . . . . . . 17 ⊢ ((-𝑥 − 1) ∈ ℕ₀ → (bits‘(-𝑥 − 1)) ∈ Fin)
31	19, 30	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → (bits‘(-𝑥 − 1)) ∈ Fin)
32	14, 31	eqeltrd 2833	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → (ℕ₀ ∖ (bits‘𝑥)) ∈ Fin)
33	29, 32	nsyl3 138	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → ¬ (bits‘𝑥) ∈ Fin)
34	11, 33	eqneltrrd 2854	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → ¬ (bits‘𝑦) ∈ Fin)
35		bitsfi 16374	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ₀ → (bits‘𝑦) ∈ Fin)
36	34, 35	nsyl 140	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → ¬ 𝑦 ∈ ℕ₀)
37	5	znegcld 12664	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → -𝑦 ∈ ℤ)
38		elznn 12570	. . . . . . . . . . . . . . . . 17 ⊢ (-𝑦 ∈ ℤ ↔ (-𝑦 ∈ ℝ ∧ (-𝑦 ∈ ℕ ∨ --𝑦 ∈ ℕ₀)))
39	38	simprbi 497	. . . . . . . . . . . . . . . 16 ⊢ (-𝑦 ∈ ℤ → (-𝑦 ∈ ℕ ∨ --𝑦 ∈ ℕ₀))
40	37, 39	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (-𝑦 ∈ ℕ ∨ --𝑦 ∈ ℕ₀))
41	6	negnegd 11558	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → --𝑦 = 𝑦)
42	41	eleq1d 2818	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (--𝑦 ∈ ℕ₀ ↔ 𝑦 ∈ ℕ₀))
43	42	orbi2d 914	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((-𝑦 ∈ ℕ ∨ --𝑦 ∈ ℕ₀) ↔ (-𝑦 ∈ ℕ ∨ 𝑦 ∈ ℕ₀)))
44	40, 43	mpbid 231	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (-𝑦 ∈ ℕ ∨ 𝑦 ∈ ℕ₀))
45	44	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → (-𝑦 ∈ ℕ ∨ 𝑦 ∈ ℕ₀))
46	45	ord 862	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → (¬ -𝑦 ∈ ℕ → 𝑦 ∈ ℕ₀))
47	36, 46	mt3d 148	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → -𝑦 ∈ ℕ)
48		nnm1nn0 12509	. . . . . . . . . . 11 ⊢ (-𝑦 ∈ ℕ → (-𝑦 − 1) ∈ ℕ₀)
49	47, 48	syl 17	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → (-𝑦 − 1) ∈ ℕ₀)
50	49	fvresd 6908	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → ((bits ↾ ℕ₀)‘(-𝑦 − 1)) = (bits‘(-𝑦 − 1)))
51	17, 20, 50	3eqtr4d 2782	. . . . . . . 8 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → ((bits ↾ ℕ₀)‘(-𝑥 − 1)) = ((bits ↾ ℕ₀)‘(-𝑦 − 1)))
52		bitsf1o 16382	. . . . . . . . . . 11 ⊢ (bits ↾ ℕ₀):ℕ₀–1-1-onto→(𝒫 ℕ₀ ∩ Fin)
53		f1of1 6829	. . . . . . . . . . 11 ⊢ ((bits ↾ ℕ₀):ℕ₀–1-1-onto→(𝒫 ℕ₀ ∩ Fin) → (bits ↾ ℕ₀):ℕ₀–1-1→(𝒫 ℕ₀ ∩ Fin))
54	52, 53	ax-mp 5	. . . . . . . . . 10 ⊢ (bits ↾ ℕ₀):ℕ₀–1-1→(𝒫 ℕ₀ ∩ Fin)
55		f1fveq 7257	. . . . . . . . . 10 ⊢ (((bits ↾ ℕ₀):ℕ₀–1-1→(𝒫 ℕ₀ ∩ Fin) ∧ ((-𝑥 − 1) ∈ ℕ₀ ∧ (-𝑦 − 1) ∈ ℕ₀)) → (((bits ↾ ℕ₀)‘(-𝑥 − 1)) = ((bits ↾ ℕ₀)‘(-𝑦 − 1)) ↔ (-𝑥 − 1) = (-𝑦 − 1)))
56	54, 55	mpan 688	. . . . . . . . 9 ⊢ (((-𝑥 − 1) ∈ ℕ₀ ∧ (-𝑦 − 1) ∈ ℕ₀) → (((bits ↾ ℕ₀)‘(-𝑥 − 1)) = ((bits ↾ ℕ₀)‘(-𝑦 − 1)) ↔ (-𝑥 − 1) = (-𝑦 − 1)))
57	19, 49, 56	syl2anc 584	. . . . . . . 8 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → (((bits ↾ ℕ₀)‘(-𝑥 − 1)) = ((bits ↾ ℕ₀)‘(-𝑦 − 1)) ↔ (-𝑥 − 1) = (-𝑦 − 1)))
58	51, 57	mpbid 231	. . . . . . 7 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → (-𝑥 − 1) = (-𝑦 − 1))
59	8, 9, 10, 58	subcan2d 11609	. . . . . 6 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → -𝑥 = -𝑦)
60	4, 7, 59	neg11d 11579	. . . . 5 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (-𝑥 ∈ ℕ ∧ (bits‘𝑥) = (bits‘𝑦))) → 𝑥 = 𝑦)
61	60	expr 457	. . . 4 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ -𝑥 ∈ ℕ) → ((bits‘𝑥) = (bits‘𝑦) → 𝑥 = 𝑦))
62	3	negnegd 11558	. . . . . . 7 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → --𝑥 = 𝑥)
63	62	eleq1d 2818	. . . . . 6 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (--𝑥 ∈ ℕ₀ ↔ 𝑥 ∈ ℕ₀))
64	63	biimpa 477	. . . . 5 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ --𝑥 ∈ ℕ₀) → 𝑥 ∈ ℕ₀)
65		simprr 771	. . . . . . . 8 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ₀ ∧ (bits‘𝑥) = (bits‘𝑦))) → (bits‘𝑥) = (bits‘𝑦))
66		fvres 6907	. . . . . . . . 9 ⊢ (𝑥 ∈ ℕ₀ → ((bits ↾ ℕ₀)‘𝑥) = (bits‘𝑥))
67	66	ad2antrl 726	. . . . . . . 8 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ₀ ∧ (bits‘𝑥) = (bits‘𝑦))) → ((bits ↾ ℕ₀)‘𝑥) = (bits‘𝑥))
68	15	ad2antlr 725	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ₀ ∧ (bits‘𝑥) = (bits‘𝑦))) → (ℕ₀ ∖ (bits‘𝑦)) = (bits‘(-𝑦 − 1)))
69		bitsfi 16374	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℕ₀ → (bits‘𝑥) ∈ Fin)
70	69	ad2antrl 726	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ₀ ∧ (bits‘𝑥) = (bits‘𝑦))) → (bits‘𝑥) ∈ Fin)
71	65, 70	eqeltrrd 2834	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ₀ ∧ (bits‘𝑥) = (bits‘𝑦))) → (bits‘𝑦) ∈ Fin)
72		difinf 9312	. . . . . . . . . . . . . 14 ⊢ ((¬ ℕ₀ ∈ Fin ∧ (bits‘𝑦) ∈ Fin) → ¬ (ℕ₀ ∖ (bits‘𝑦)) ∈ Fin)
73	27, 71, 72	sylancr 587	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ₀ ∧ (bits‘𝑥) = (bits‘𝑦))) → ¬ (ℕ₀ ∖ (bits‘𝑦)) ∈ Fin)
74	68, 73	eqneltrrd 2854	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ₀ ∧ (bits‘𝑥) = (bits‘𝑦))) → ¬ (bits‘(-𝑦 − 1)) ∈ Fin)
75		bitsfi 16374	. . . . . . . . . . . 12 ⊢ ((-𝑦 − 1) ∈ ℕ₀ → (bits‘(-𝑦 − 1)) ∈ Fin)
76	74, 75	nsyl 140	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ₀ ∧ (bits‘𝑥) = (bits‘𝑦))) → ¬ (-𝑦 − 1) ∈ ℕ₀)
77	76, 48	nsyl 140	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ₀ ∧ (bits‘𝑥) = (bits‘𝑦))) → ¬ -𝑦 ∈ ℕ)
78	44	adantr 481	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ₀ ∧ (bits‘𝑥) = (bits‘𝑦))) → (-𝑦 ∈ ℕ ∨ 𝑦 ∈ ℕ₀))
79	78	ord 862	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ₀ ∧ (bits‘𝑥) = (bits‘𝑦))) → (¬ -𝑦 ∈ ℕ → 𝑦 ∈ ℕ₀))
80	77, 79	mpd 15	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ₀ ∧ (bits‘𝑥) = (bits‘𝑦))) → 𝑦 ∈ ℕ₀)
81	80	fvresd 6908	. . . . . . . 8 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ₀ ∧ (bits‘𝑥) = (bits‘𝑦))) → ((bits ↾ ℕ₀)‘𝑦) = (bits‘𝑦))
82	65, 67, 81	3eqtr4d 2782	. . . . . . 7 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ₀ ∧ (bits‘𝑥) = (bits‘𝑦))) → ((bits ↾ ℕ₀)‘𝑥) = ((bits ↾ ℕ₀)‘𝑦))
83		simprl 769	. . . . . . . 8 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ₀ ∧ (bits‘𝑥) = (bits‘𝑦))) → 𝑥 ∈ ℕ₀)
84		f1fveq 7257	. . . . . . . . 9 ⊢ (((bits ↾ ℕ₀):ℕ₀–1-1→(𝒫 ℕ₀ ∩ Fin) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑦 ∈ ℕ₀)) → (((bits ↾ ℕ₀)‘𝑥) = ((bits ↾ ℕ₀)‘𝑦) ↔ 𝑥 = 𝑦))
85	54, 84	mpan 688	. . . . . . . 8 ⊢ ((𝑥 ∈ ℕ₀ ∧ 𝑦 ∈ ℕ₀) → (((bits ↾ ℕ₀)‘𝑥) = ((bits ↾ ℕ₀)‘𝑦) ↔ 𝑥 = 𝑦))
86	83, 80, 85	syl2anc 584	. . . . . . 7 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ₀ ∧ (bits‘𝑥) = (bits‘𝑦))) → (((bits ↾ ℕ₀)‘𝑥) = ((bits ↾ ℕ₀)‘𝑦) ↔ 𝑥 = 𝑦))
87	82, 86	mpbid 231	. . . . . 6 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑥 ∈ ℕ₀ ∧ (bits‘𝑥) = (bits‘𝑦))) → 𝑥 = 𝑦)
88	87	expr 457	. . . . 5 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ 𝑥 ∈ ℕ₀) → ((bits‘𝑥) = (bits‘𝑦) → 𝑥 = 𝑦))
89	64, 88	syldan 591	. . . 4 ⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ --𝑥 ∈ ℕ₀) → ((bits‘𝑥) = (bits‘𝑦) → 𝑥 = 𝑦))
90	2	znegcld 12664	. . . . 5 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → -𝑥 ∈ ℤ)
91		elznn 12570	. . . . . 6 ⊢ (-𝑥 ∈ ℤ ↔ (-𝑥 ∈ ℝ ∧ (-𝑥 ∈ ℕ ∨ --𝑥 ∈ ℕ₀)))
92	91	simprbi 497	. . . . 5 ⊢ (-𝑥 ∈ ℤ → (-𝑥 ∈ ℕ ∨ --𝑥 ∈ ℕ₀))
93	90, 92	syl 17	. . . 4 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (-𝑥 ∈ ℕ ∨ --𝑥 ∈ ℕ₀))
94	61, 89, 93	mpjaodan 957	. . 3 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((bits‘𝑥) = (bits‘𝑦) → 𝑥 = 𝑦))
95	94	rgen2 3197	. 2 ⊢ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ ((bits‘𝑥) = (bits‘𝑦) → 𝑥 = 𝑦)
96		dff13 7250	. 2 ⊢ (bits:ℤ–1-1→𝒫 ℕ₀ ↔ (bits:ℤ⟶𝒫 ℕ₀ ∧ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ ((bits‘𝑥) = (bits‘𝑦) → 𝑥 = 𝑦)))
97	1, 95, 96	mpbir2an 709	1 ⊢ bits:ℤ–1-1→𝒫 ℕ₀

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 845 = wceq 1541 ∈ wcel 2106 ∀wral 3061 ∖ cdif 3944 ∩ cin 3946 𝒫 cpw 4601 class class class wbr 5147 ↾ cres 5677 ⟶wf 6536 –1-1→wf1 6537 –1-1-onto→wf1o 6539 ‘cfv 6540 (class class class)co 7405 ωcom 7851 ≈ cen 8932 Fincfn 8935 ℂcc 11104 ℝcr 11105 1c1 11107 − cmin 11440 -cneg 11441 ℕcn 12208 ℕ₀cn0 12468 ℤcz 12554 bitscbits 16356

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721 ax-inf2 9632 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-pre-sup 11184

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-disj 5113 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-se 5631 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6297 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7852 df-1st 7971 df-2nd 7972 df-frecs 8262 df-wrecs 8293 df-recs 8367 df-rdg 8406 df-1o 8462 df-2o 8463 df-oadd 8466 df-er 8699 df-map 8818 df-pm 8819 df-en 8936 df-dom 8937 df-sdom 8938 df-fin 8939 df-sup 9433 df-inf 9434 df-oi 9501 df-dju 9892 df-card 9930 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11442 df-neg 11443 df-div 11868 df-nn 12209 df-2 12271 df-3 12272 df-n0 12469 df-xnn0 12541 df-z 12555 df-uz 12819 df-rp 12971 df-fz 13481 df-fzo 13624 df-fl 13753 df-mod 13831 df-seq 13963 df-exp 14024 df-hash 14287 df-cj 15042 df-re 15043 df-im 15044 df-sqrt 15178 df-abs 15179 df-clim 15428 df-sum 15629 df-dvds 16194 df-bits 16359

This theorem is referenced by: bitsuz 16411 eulerpartlemmf 33362

W3C validator