Theorem eulerpartgbij 35050

Description: Lemma for eulerpart 35060: The 𝐺 function is a bijection. (Contributed by Thierry Arnoux, 27-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.)

Hypotheses

Ref	Expression
eulerpart.p	⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}
eulerpart.o	⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}
eulerpart.d	⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}
eulerpart.j	⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
eulerpart.f	⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))
eulerpart.h	⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
eulerpart.m	⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})
eulerpart.r	⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}
eulerpart.t	⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}
eulerpart.g	⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))

Assertion

Ref	Expression
eulerpartgbij	⊢ 𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅)

Distinct variable groups:   𝑓,𝑔,𝑘,𝑛,𝑜,𝑥,𝑦,𝑧   𝑜,𝐹   𝑓,𝑟,𝐽,𝑜,𝑥,𝑦   𝑜,𝑀,𝑟   𝑓,𝑁,𝑔,𝑥   𝑃,𝑔   𝑅,𝑓,𝑜   𝑜,𝐻,𝑟   𝑇,𝑓,𝑜

Allowed substitution hints:   𝐷(𝑥, 𝑦, 𝑧, 𝑓, 𝑔, 𝑘, 𝑛, 𝑜, 𝑟)   𝑃(𝑥, 𝑦, 𝑧, 𝑓, 𝑘, 𝑛, 𝑜, 𝑟)   𝑅(𝑥, 𝑦, 𝑧, 𝑔, 𝑘, 𝑛, 𝑟)   𝑇(𝑥, 𝑦, 𝑧, 𝑔, 𝑘, 𝑛, 𝑟)   𝐹(𝑥, 𝑦, 𝑧, 𝑓, 𝑔, 𝑘, 𝑛, 𝑟)   𝐺(𝑥, 𝑦, 𝑧, 𝑓, 𝑔, 𝑘, 𝑛, 𝑜, 𝑟)   𝐻(𝑥, 𝑦, 𝑧, 𝑓, 𝑔, 𝑘, 𝑛)   𝐽(𝑧, 𝑔, 𝑘, 𝑛)   𝑀(𝑥, 𝑦, 𝑧, 𝑓, 𝑔, 𝑘, 𝑛)   𝑁(𝑦, 𝑧, 𝑘, 𝑛, 𝑜, 𝑟)   𝑂(𝑥, 𝑦, 𝑧, 𝑓, 𝑔, 𝑘, 𝑛, 𝑜, 𝑟)

Proof of Theorem eulerpartgbij

Dummy variables 𝑎 𝑚 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnex 12344	. . . . 5 ⊢ ℕ ∈ V
2		indf1ofs 33479	. . . . 5 ⊢ (ℕ ∈ V → ((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (◡𝑓 “ {1}) ∈ Fin})
3	1, 2	ax-mp 5	. . . 4 ⊢ ((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (◡𝑓 “ {1}) ∈ Fin}
4		incom 4106	. . . . . . 7 ⊢ (({0, 1} ↑m ℕ) ∩ {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}) = ({𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} ∩ ({0, 1} ↑m ℕ))
5		eulerpart.r	. . . . . . . 8 ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}
6	5	ineq2i 4114	. . . . . . 7 ⊢ (({0, 1} ↑m ℕ) ∩ 𝑅) = (({0, 1} ↑m ℕ) ∩ {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin})
7		dfrab2 4265	. . . . . . 7 ⊢ {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (◡𝑓 “ ℕ) ∈ Fin} = ({𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} ∩ ({0, 1} ↑m ℕ))
8	4, 6, 7	3eqtr4i 2793	. . . . . 6 ⊢ (({0, 1} ↑m ℕ) ∩ 𝑅) = {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (◡𝑓 “ ℕ) ∈ Fin}
9		elmapfun 8891	. . . . . . . . 9 ⊢ (𝑓 ∈ ({0, 1} ↑m ℕ) → Fun 𝑓)
10		elmapi 8872	. . . . . . . . . 10 ⊢ (𝑓 ∈ ({0, 1} ↑m ℕ) → 𝑓:ℕ⟶{0, 1})
11	10	frnd 6718	. . . . . . . . 9 ⊢ (𝑓 ∈ ({0, 1} ↑m ℕ) → ran 𝑓 ⊆ {0, 1})
12		fimacnvinrn2 7072	. . . . . . . . . 10 ⊢ ((Fun 𝑓 ∧ ran 𝑓 ⊆ {0, 1}) → (◡𝑓 “ ℕ) = (◡𝑓 “ (ℕ ∩ {0, 1})))
13		df-pr 4587	. . . . . . . . . . . . . 14 ⊢ {0, 1} = ({0} ∪ {1})
14	13	ineq2i 4114	. . . . . . . . . . . . 13 ⊢ (ℕ ∩ {0, 1}) = (ℕ ∩ ({0} ∪ {1}))
15		indi 4229	. . . . . . . . . . . . 13 ⊢ (ℕ ∩ ({0} ∪ {1})) = ((ℕ ∩ {0}) ∪ (ℕ ∩ {1}))
16		0nnn 12377	. . . . . . . . . . . . . . 15 ⊢ ¬ 0 ∈ ℕ
17		disjsn 4668	. . . . . . . . . . . . . . 15 ⊢ ((ℕ ∩ {0}) = ∅ ↔ ¬ 0 ∈ ℕ)
18	16, 17	mpbir 234	. . . . . . . . . . . . . 14 ⊢ (ℕ ∩ {0}) = ∅
19		1nn 12349	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℕ
20		1ex 11306	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ V
21	20	snss 4741	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ ℕ ↔ {1} ⊆ ℕ)
22	19, 21	mpbi 233	. . . . . . . . . . . . . . . 16 ⊢ {1} ⊆ ℕ
23		dfss 4095	. . . . . . . . . . . . . . . 16 ⊢ ({1} ⊆ ℕ ↔ {1} = ({1} ∩ ℕ))
24	22, 23	mpbi 233	. . . . . . . . . . . . . . 15 ⊢ {1} = ({1} ∩ ℕ)
25		incom 4106	. . . . . . . . . . . . . . 15 ⊢ ({1} ∩ ℕ) = (ℕ ∩ {1})
26	24, 25	eqtr2i 2784	. . . . . . . . . . . . . 14 ⊢ (ℕ ∩ {1}) = {1}
27	18, 26	uneq12i 4165	. . . . . . . . . . . . 13 ⊢ ((ℕ ∩ {0}) ∪ (ℕ ∩ {1})) = (∅ ∪ {1})
28	14, 15, 27	3eqtri 2787	. . . . . . . . . . . 12 ⊢ (ℕ ∩ {0, 1}) = (∅ ∪ {1})
29		uncom 4157	. . . . . . . . . . . 12 ⊢ (∅ ∪ {1}) = ({1} ∪ ∅)
30		un0 4343	. . . . . . . . . . . 12 ⊢ ({1} ∪ ∅) = {1}
31	28, 29, 30	3eqtri 2787	. . . . . . . . . . 11 ⊢ (ℕ ∩ {0, 1}) = {1}
32	31	imaeq2i 6049	. . . . . . . . . 10 ⊢ (◡𝑓 “ (ℕ ∩ {0, 1})) = (◡𝑓 “ {1})
33	12, 32	eqtrdi 2811	. . . . . . . . 9 ⊢ ((Fun 𝑓 ∧ ran 𝑓 ⊆ {0, 1}) → (◡𝑓 “ ℕ) = (◡𝑓 “ {1}))
34	9, 11, 33	syl2anc 596	. . . . . . . 8 ⊢ (𝑓 ∈ ({0, 1} ↑m ℕ) → (◡𝑓 “ ℕ) = (◡𝑓 “ {1}))
35	34	eleq1d 2845	. . . . . . 7 ⊢ (𝑓 ∈ ({0, 1} ↑m ℕ) → ((◡𝑓 “ ℕ) ∈ Fin ↔ (◡𝑓 “ {1}) ∈ Fin))
36	35	rabbiia 3416	. . . . . 6 ⊢ {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (◡𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (◡𝑓 “ {1}) ∈ Fin}
37	8, 36	eqtr2i 2784	. . . . 5 ⊢ {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (◡𝑓 “ {1}) ∈ Fin} = (({0, 1} ↑m ℕ) ∩ 𝑅)
38		f1oeq3 6814	. . . . 5 ⊢ ({𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (◡𝑓 “ {1}) ∈ Fin} = (({0, 1} ↑m ℕ) ∩ 𝑅) → (((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (◡𝑓 “ {1}) ∈ Fin} ↔ ((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅)))
39	37, 38	ax-mp 5	. . . 4 ⊢ (((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (◡𝑓 “ {1}) ∈ Fin} ↔ ((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅))
40	3, 39	mpbi 233	. . 3 ⊢ ((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅)
41		eulerpart.j	. . . . . . 7 ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
42		eulerpart.f	. . . . . . 7 ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))
43	41, 42	oddpwdc 35032	. . . . . 6 ⊢ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ
44		f1opwfi 9348	. . . . . 6 ⊢ (𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ → (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)):(𝒫 (𝐽 × ℕ0) ∩ Fin)–1-1-onto→(𝒫 ℕ ∩ Fin))
45	43, 44	ax-mp 5	. . . . 5 ⊢ (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)):(𝒫 (𝐽 × ℕ0) ∩ Fin)–1-1-onto→(𝒫 ℕ ∩ Fin)
46		eulerpart.p	. . . . . . . 8 ⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}
47		eulerpart.o	. . . . . . . 8 ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}
48		eulerpart.d	. . . . . . . 8 ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}
49		eulerpart.h	. . . . . . . 8 ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
50		eulerpart.m	. . . . . . . 8 ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})
51	46, 47, 48, 41, 42, 49, 50	eulerpartlem1 35045	. . . . . . 7 ⊢ 𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
52		bitsf1o 16620	. . . . . . . . . . . . . 14 ⊢ (bits ↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
53	52	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (bits ↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin))
54	41, 1	rabex2 5301	. . . . . . . . . . . . . 14 ⊢ 𝐽 ∈ V
55	54	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → 𝐽 ∈ V)
56		nn0ex 12615	. . . . . . . . . . . . . 14 ⊢ ℕ0 ∈ V
57	56	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → ℕ0 ∈ V)
58	56	pwex 5341	. . . . . . . . . . . . . . 15 ⊢ 𝒫 ℕ0 ∈ V
59	58	inex1 5276	. . . . . . . . . . . . . 14 ⊢ (𝒫 ℕ0 ∩ Fin) ∈ V
60	59	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝒫 ℕ0 ∩ Fin) ∈ V)
61		0nn0 12624	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℕ0
62	61	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → 0 ∈ ℕ0)
63		fvres 6904	. . . . . . . . . . . . . . 15 ⊢ (0 ∈ ℕ0 → ((bits ↾ ℕ0)‘0) = (bits‘0))
64	61, 63	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((bits ↾ ℕ0)‘0) = (bits‘0)
65		0bits 16614	. . . . . . . . . . . . . 14 ⊢ (bits‘0) = ∅
66	64, 65	eqtr2i 2784	. . . . . . . . . . . . 13 ⊢ ∅ = ((bits ↾ ℕ0)‘0)
67		elmapi 8872	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ (ℕ0 ↑m 𝐽) → 𝑓:𝐽⟶ℕ0)
68		fcdmnn0supp 12666	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ V ∧ 𝑓:𝐽⟶ℕ0) → (𝑓 supp 0) = (◡𝑓 “ ℕ))
69	54, 67, 68	sylancr 599	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ (ℕ0 ↑m 𝐽) → (𝑓 supp 0) = (◡𝑓 “ ℕ))
70	69	eleq1d 2845	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ (ℕ0 ↑m 𝐽) → ((𝑓 supp 0) ∈ Fin ↔ (◡𝑓 “ ℕ) ∈ Fin))
71	70	rabbiia 3416	. . . . . . . . . . . . . 14 ⊢ {𝑓 ∈ (ℕ0 ↑m 𝐽) ∣ (𝑓 supp 0) ∈ Fin} = {𝑓 ∈ (ℕ0 ↑m 𝐽) ∣ (◡𝑓 “ ℕ) ∈ Fin}
72		elmapfun 8891	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ (ℕ0 ↑m 𝐽) → Fun 𝑓)
73		vex 3454	. . . . . . . . . . . . . . . . 17 ⊢ 𝑓 ∈ V
74		funisfsupp 9362	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝑓 ∧ 𝑓 ∈ V ∧ 0 ∈ ℕ0) → (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
75	73, 61, 74	mp3an23 1482	. . . . . . . . . . . . . . . 16 ⊢ (Fun 𝑓 → (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
76	72, 75	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ (ℕ0 ↑m 𝐽) → (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
77	76	rabbiia 3416	. . . . . . . . . . . . . 14 ⊢ {𝑓 ∈ (ℕ0 ↑m 𝐽) ∣ 𝑓 finSupp 0} = {𝑓 ∈ (ℕ0 ↑m 𝐽) ∣ (𝑓 supp 0) ∈ Fin}
78		incom 4106	. . . . . . . . . . . . . . 15 ⊢ ({𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} ∩ (ℕ0 ↑m 𝐽)) = ((ℕ0 ↑m 𝐽) ∩ {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin})
79		dfrab2 4265	. . . . . . . . . . . . . . 15 ⊢ {𝑓 ∈ (ℕ0 ↑m 𝐽) ∣ (◡𝑓 “ ℕ) ∈ Fin} = ({𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} ∩ (ℕ0 ↑m 𝐽))
80	5	ineq2i 4114	. . . . . . . . . . . . . . 15 ⊢ ((ℕ0 ↑m 𝐽) ∩ 𝑅) = ((ℕ0 ↑m 𝐽) ∩ {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin})
81	78, 79, 80	3eqtr4ri 2794	. . . . . . . . . . . . . 14 ⊢ ((ℕ0 ↑m 𝐽) ∩ 𝑅) = {𝑓 ∈ (ℕ0 ↑m 𝐽) ∣ (◡𝑓 “ ℕ) ∈ Fin}
82	71, 77, 81	3eqtr4ri 2794	. . . . . . . . . . . . 13 ⊢ ((ℕ0 ↑m 𝐽) ∩ 𝑅) = {𝑓 ∈ (ℕ0 ↑m 𝐽) ∣ 𝑓 finSupp 0}
83		elmapfun 8891	. . . . . . . . . . . . . . 15 ⊢ (𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) → Fun 𝑟)
84		vex 3454	. . . . . . . . . . . . . . . . 17 ⊢ 𝑟 ∈ V
85		0ex 5260	. . . . . . . . . . . . . . . . 17 ⊢ ∅ ∈ V
86		funisfsupp 9362	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝑟 ∧ 𝑟 ∈ V ∧ ∅ ∈ V) → (𝑟 finSupp ∅ ↔ (𝑟 supp ∅) ∈ Fin))
87	84, 85, 86	mp3an23 1482	. . . . . . . . . . . . . . . 16 ⊢ (Fun 𝑟 → (𝑟 finSupp ∅ ↔ (𝑟 supp ∅) ∈ Fin))
88	87	bicomd 226	. . . . . . . . . . . . . . 15 ⊢ (Fun 𝑟 → ((𝑟 supp ∅) ∈ Fin ↔ 𝑟 finSupp ∅))
89	83, 88	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) → ((𝑟 supp ∅) ∈ Fin ↔ 𝑟 finSupp ∅))
90	89	rabbiia 3416	. . . . . . . . . . . . 13 ⊢ {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ 𝑟 finSupp ∅}
91	53, 55, 57, 60, 62, 66, 82, 90	fcobijfs 33359	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)):((ℕ0 ↑m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
92		elinel1 4098	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) → 𝑓 ∈ (ℕ0 ↑m 𝐽))
93		frn 6717	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:𝐽⟶ℕ0 → ran 𝑓 ⊆ ℕ0)
94		cores 6250	. . . . . . . . . . . . . . . 16 ⊢ (ran 𝑓 ⊆ ℕ0 → ((bits ↾ ℕ0) ∘ 𝑓) = (bits ∘ 𝑓))
95	92, 67, 93, 94	4syl 20	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) → ((bits ↾ ℕ0) ∘ 𝑓) = (bits ∘ 𝑓))
96	95	mpteq2ia 5199	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)) = (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓))
97	96	eqcomi 2769	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓))
98		f1oeq1 6812	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)) → ((𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0 ↑m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} ↔ (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)):((ℕ0 ↑m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}))
99	97, 98	mp1i 14	. . . . . . . . . . . 12 ⊢ (⊤ → ((𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0 ↑m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} ↔ (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)):((ℕ0 ↑m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}))
100	91, 99	mpbird 260	. . . . . . . . . . 11 ⊢ (⊤ → (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0 ↑m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
101	100	mptru 1576	. . . . . . . . . 10 ⊢ (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0 ↑m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
102		ssrab2 4005	. . . . . . . . . . . . . . . 16 ⊢ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ⊆ ℕ
103	41, 102	eqsstri 3954	. . . . . . . . . . . . . . 15 ⊢ 𝐽 ⊆ ℕ
104	1, 56, 103	3pm3.2i 1358	. . . . . . . . . . . . . 14 ⊢ (ℕ ∈ V ∧ ℕ0 ∈ V ∧ 𝐽 ⊆ ℕ)
105		eulerpart.t	. . . . . . . . . . . . . . . 16 ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}
106		cnveq 5850	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = 𝑜 → ◡𝑓 = ◡𝑜)
107		dfn2 12622	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ = (ℕ0 ∖ {0})
108	107	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = 𝑜 → ℕ = (ℕ0 ∖ {0}))
109	106, 108	imaeq12d 6052	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = 𝑜 → (◡𝑓 “ ℕ) = (◡𝑜 “ (ℕ0 ∖ {0})))
110	109	sseq1d 3939	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑜 → ((◡𝑓 “ ℕ) ⊆ 𝐽 ↔ (◡𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽))
111	110	cbvrabv 3422	. . . . . . . . . . . . . . . 16 ⊢ {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽} = {𝑜 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽}
112	105, 111	eqtri 2783	. . . . . . . . . . . . . . 15 ⊢ 𝑇 = {𝑜 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽}
113		eqid 2760	. . . . . . . . . . . . . . 15 ⊢ (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) = (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))
114	112, 113	resf1o 33368	. . . . . . . . . . . . . 14 ⊢ (((ℕ ∈ V ∧ ℕ0 ∈ V ∧ 𝐽 ⊆ ℕ) ∧ 0 ∈ ℕ0) → (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1-onto→(ℕ0 ↑m 𝐽))
115	104, 61, 114	mp2an 705	. . . . . . . . . . . . 13 ⊢ (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1-onto→(ℕ0 ↑m 𝐽)
116		f1of1 6823	. . . . . . . . . . . . 13 ⊢ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1-onto→(ℕ0 ↑m 𝐽) → (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1→(ℕ0 ↑m 𝐽))
117	115, 116	ax-mp 5	. . . . . . . . . . . 12 ⊢ (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1→(ℕ0 ↑m 𝐽)
118		inss1 4133	. . . . . . . . . . . 12 ⊢ (𝑇 ∩ 𝑅) ⊆ 𝑇
119		f1ores 6839	. . . . . . . . . . . 12 ⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1→(ℕ0 ↑m 𝐽) ∧ (𝑇 ∩ 𝑅) ⊆ 𝑇) → ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)))
120	117, 118, 119	mp2an 705	. . . . . . . . . . 11 ⊢ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅))
121		vex 3454	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑜 ∈ V
122	121	resex 6017	. . . . . . . . . . . . . . . . 17 ⊢ (𝑜 ↾ 𝐽) ∈ V
123	122, 113	fnmpti 6682	. . . . . . . . . . . . . . . 16 ⊢ (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) Fn 𝑇
124		fvelimab 6957	. . . . . . . . . . . . . . . 16 ⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) Fn 𝑇 ∧ (𝑇 ∩ 𝑅) ⊆ 𝑇) → (𝑓 ∈ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓))
125	123, 118, 124	mp2an 705	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓)
126		eqid 2760	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) = (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽))
127		vex 3454	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑚 ∈ V
128	127	resex 6017	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ↾ 𝐽) ∈ V
129	126, 128	elrnmpti 5943	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑓 = (𝑚 ↾ 𝐽))
130	46, 47, 48, 41, 42, 49, 50, 5, 105	eulerpartlemt 35049	. . . . . . . . . . . . . . . . 17 ⊢ ((ℕ0 ↑m 𝐽) ∩ 𝑅) = ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽))
131	130	eleq2i 2852	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↔ 𝑓 ∈ ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)))
132		elinel1 4098	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) → 𝑚 ∈ 𝑇)
133	113	fvtresfn 6996	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ 𝑇 → ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = (𝑚 ↾ 𝐽))
134	133	eqeq1d 2762	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ 𝑇 → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ (𝑚 ↾ 𝐽) = 𝑓))
135	132, 134	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ (𝑚 ↾ 𝐽) = 𝑓))
136		eqcom 2767	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 ↾ 𝐽) = 𝑓 ↔ 𝑓 = (𝑚 ↾ 𝐽))
137	135, 136	bitrdi 290	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ 𝑓 = (𝑚 ↾ 𝐽)))
138	137	rexbiia 3107	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑚 ∈ (𝑇 ∩ 𝑅)((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑓 = (𝑚 ↾ 𝐽))
139	129, 131, 138	3bitr4ri 307	. . . . . . . . . . . . . . 15 ⊢ (∃𝑚 ∈ (𝑇 ∩ 𝑅)((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ 𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅))
140	125, 139	bitri 278	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ 𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅))
141	140	eqriv 2757	. . . . . . . . . . . . 13 ⊢ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) = ((ℕ0 ↑m 𝐽) ∩ 𝑅)
142		f1oeq3 6814	. . . . . . . . . . . . 13 ⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) = ((ℕ0 ↑m 𝐽) ∩ 𝑅) → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅)))
143	141, 142	ax-mp 5	. . . . . . . . . . . 12 ⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅))
144		resmpt 6028	. . . . . . . . . . . . 13 ⊢ ((𝑇 ∩ 𝑅) ⊆ 𝑇 → ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)))
145		f1oeq1 6812	. . . . . . . . . . . . 13 ⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)) → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅)))
146	118, 144, 145	mp2b 10	. . . . . . . . . . . 12 ⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅))
147	143, 146	bitri 278	. . . . . . . . . . 11 ⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅))
148	120, 147	mpbi 233	. . . . . . . . . 10 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅)
149		f1oco 6848	. . . . . . . . . 10 ⊢ (((𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0 ↑m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} ∧ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅)) → ((𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
150	101, 148, 149	mp2an 705	. . . . . . . . 9 ⊢ ((𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
151		f1of 6824	. . . . . . . . . . . . . 14 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅) → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)⟶((ℕ0 ↑m 𝐽) ∩ 𝑅))
152		eqid 2760	. . . . . . . . . . . . . . . 16 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))
153	152	fmpt 7110	. . . . . . . . . . . . . . 15 ⊢ (∀𝑜 ∈ (𝑇 ∩ 𝑅)(𝑜 ↾ 𝐽) ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)⟶((ℕ0 ↑m 𝐽) ∩ 𝑅))
154	153	biimpri 231	. . . . . . . . . . . . . 14 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)⟶((ℕ0 ↑m 𝐽) ∩ 𝑅) → ∀𝑜 ∈ (𝑇 ∩ 𝑅)(𝑜 ↾ 𝐽) ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅))
155	148, 151, 154	mp2b 10	. . . . . . . . . . . . 13 ⊢ ∀𝑜 ∈ (𝑇 ∩ 𝑅)(𝑜 ↾ 𝐽) ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅)
156	155	a1i 11	. . . . . . . . . . . 12 ⊢ (⊤ → ∀𝑜 ∈ (𝑇 ∩ 𝑅)(𝑜 ↾ 𝐽) ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅))
157		eqidd 2761	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)))
158		eqidd 2761	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)))
159		coeq2 5835	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑜 ↾ 𝐽) → (bits ∘ 𝑓) = (bits ∘ (𝑜 ↾ 𝐽)))
160	156, 157, 158, 159	fmptcof 7131	. . . . . . . . . . 11 ⊢ (⊤ → ((𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))))
161	160	eqcomd 2766	. . . . . . . . . 10 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))) = ((𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))))
162		eqidd 2761	. . . . . . . . . 10 ⊢ (⊤ → (𝑇 ∩ 𝑅) = (𝑇 ∩ 𝑅))
163	49	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
164	161, 162, 163	f1oeq123d 6818	. . . . . . . . 9 ⊢ (⊤ → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻 ↔ ((𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}))
165	150, 164	mpbiri 261	. . . . . . . 8 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻)
166	165	mptru 1576	. . . . . . 7 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻
167		f1oco 6848	. . . . . . 7 ⊢ ((𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) ∧ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻) → (𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin))
168	51, 166, 167	mp2an 705	. . . . . 6 ⊢ (𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
169		eqidd 2761	. . . . . . . . . . 11 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))))
170		bitsf 16602	. . . . . . . . . . . . . 14 ⊢ bits:ℤ⟶𝒫 ℕ0
171		zex 12705	. . . . . . . . . . . . . 14 ⊢ ℤ ∈ V
172		fex 7232	. . . . . . . . . . . . . 14 ⊢ ((bits:ℤ⟶𝒫 ℕ0 ∧ ℤ ∈ V) → bits ∈ V)
173	170, 171, 172	mp2an 705	. . . . . . . . . . . . 13 ⊢ bits ∈ V
174	173, 122	coex 7942	. . . . . . . . . . . 12 ⊢ (bits ∘ (𝑜 ↾ 𝐽)) ∈ V
175	174	a1i 11	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → (bits ∘ (𝑜 ↾ 𝐽)) ∈ V)
176	169, 175	fvmpt2d 7007	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))‘𝑜) = (bits ∘ (𝑜 ↾ 𝐽)))
177		f1of 6824	. . . . . . . . . . . 12 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻 → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)⟶𝐻)
178	165, 177	syl 18	. . . . . . . . . . 11 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)⟶𝐻)
179	178	ffvelcdmda 7084	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))‘𝑜) ∈ 𝐻)
180	176, 179	eqeltrrd 2861	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → (bits ∘ (𝑜 ↾ 𝐽)) ∈ 𝐻)
181		f1ofn 6825	. . . . . . . . . . . 12 ⊢ (𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) → 𝑀 Fn 𝐻)
182	51, 181	ax-mp 5	. . . . . . . . . . 11 ⊢ 𝑀 Fn 𝐻
183		dffn5 6943	. . . . . . . . . . 11 ⊢ (𝑀 Fn 𝐻 ↔ 𝑀 = (𝑟 ∈ 𝐻 ↦ (𝑀‘𝑟)))
184	182, 183	mpbi 233	. . . . . . . . . 10 ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ (𝑀‘𝑟))
185	184	a1i 11	. . . . . . . . 9 ⊢ (⊤ → 𝑀 = (𝑟 ∈ 𝐻 ↦ (𝑀‘𝑟)))
186		fveq2 6885	. . . . . . . . 9 ⊢ (𝑟 = (bits ∘ (𝑜 ↾ 𝐽)) → (𝑀‘𝑟) = (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))
187	180, 169, 185, 186	fmptco 7130	. . . . . . . 8 ⊢ (⊤ → (𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
188	187	mptru 1576	. . . . . . 7 ⊢ (𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))
189		f1oeq1 6812	. . . . . . 7 ⊢ ((𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) → ((𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)))
190	188, 189	ax-mp 5	. . . . . 6 ⊢ ((𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin))
191	168, 190	mpbi 233	. . . . 5 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
192		f1oco 6848	. . . . 5 ⊢ (((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)):(𝒫 (𝐽 × ℕ0) ∩ Fin)–1-1-onto→(𝒫 ℕ ∩ Fin) ∧ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)) → ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin))
193	45, 191, 192	mp2an 705	. . . 4 ⊢ ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)
194		simpr 490	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → 𝑜 ∈ (𝑇 ∩ 𝑅))
195		fvex 6898	. . . . . . . . 9 ⊢ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))) ∈ V
196		eqid 2760	. . . . . . . . . 10 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))
197	196	fvmpt2 7005	. . . . . . . . 9 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ∧ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))) ∈ V) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))‘𝑜) = (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))
198	194, 195, 197	sylancl 598	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))‘𝑜) = (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))
199		f1of 6824	. . . . . . . . . 10 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)⟶(𝒫 (𝐽 × ℕ0) ∩ Fin))
200	191, 199	mp1i 14	. . . . . . . . 9 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)⟶(𝒫 (𝐽 × ℕ0) ∩ Fin))
201	200	ffvelcdmda 7084	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))‘𝑜) ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin))
202	198, 201	eqeltrrd 2861	. . . . . . 7 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))) ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin))
203		eqidd 2761	. . . . . . 7 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
204		eqidd 2761	. . . . . . 7 ⊢ (⊤ → (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) = (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)))
205		imaeq2 6047	. . . . . . 7 ⊢ (𝑎 = (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))) → (𝐹 “ 𝑎) = (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
206	202, 203, 204, 205	fmptco 7130	. . . . . 6 ⊢ (⊤ → ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
207	206	mptru 1576	. . . . 5 ⊢ ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
208		f1oeq1 6812	. . . . 5 ⊢ (((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) → (((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)))
209	207, 208	ax-mp 5	. . . 4 ⊢ (((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin))
210	193, 209	mpbi 233	. . 3 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)
211		f1oco 6848	. . 3 ⊢ ((((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅) ∧ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)) → (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))):(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅))
212	40, 210, 211	mp2an 705	. 2 ⊢ (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))):(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅)
213		eulerpart.g	. . . 4 ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
214	42	mpoexg 8089	. . . . . . . . . 10 ⊢ ((𝐽 ∈ V ∧ ℕ0 ∈ V) → 𝐹 ∈ V)
215	54, 56, 214	mp2an 705	. . . . . . . . 9 ⊢ 𝐹 ∈ V
216		imaexg 7925	. . . . . . . . 9 ⊢ (𝐹 ∈ V → (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) ∈ V)
217	215, 216	ax-mp 5	. . . . . . . 8 ⊢ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) ∈ V
218		eqid 2760	. . . . . . . . 9 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
219	218	fvmpt2 7005	. . . . . . . 8 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ∧ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) ∈ V) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))‘𝑜) = (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
220	194, 217, 219	sylancl 598	. . . . . . 7 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))‘𝑜) = (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
221		f1of 6824	. . . . . . . . 9 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin) → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)⟶(𝒫 ℕ ∩ Fin))
222	210, 221	mp1i 14	. . . . . . . 8 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)⟶(𝒫 ℕ ∩ Fin))
223	222	ffvelcdmda 7084	. . . . . . 7 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))‘𝑜) ∈ (𝒫 ℕ ∩ Fin))
224	220, 223	eqeltrrd 2861	. . . . . 6 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) ∈ (𝒫 ℕ ∩ Fin))
225		eqidd 2761	. . . . . 6 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
226		indf1o 33477	. . . . . . . . . . 11 ⊢ (ℕ ∈ V → (𝟭‘ℕ):𝒫 ℕ–1-1-onto→({0, 1} ↑m ℕ))
227		f1ofn 6825	. . . . . . . . . . 11 ⊢ ((𝟭‘ℕ):𝒫 ℕ–1-1-onto→({0, 1} ↑m ℕ) → (𝟭‘ℕ) Fn 𝒫 ℕ)
228	1, 226, 227	mp2b 10	. . . . . . . . . 10 ⊢ (𝟭‘ℕ) Fn 𝒫 ℕ
229		dffn5 6943	. . . . . . . . . 10 ⊢ ((𝟭‘ℕ) Fn 𝒫 ℕ ↔ (𝟭‘ℕ) = (𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)))
230	228, 229	mpbi 233	. . . . . . . . 9 ⊢ (𝟭‘ℕ) = (𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏))
231	230	reseq1i 5965	. . . . . . . 8 ⊢ ((𝟭‘ℕ) ↾ Fin) = ((𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)) ↾ Fin)
232		resmpt3 6029	. . . . . . . 8 ⊢ ((𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏))
233	231, 232	eqtri 2783	. . . . . . 7 ⊢ ((𝟭‘ℕ) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏))
234	233	a1i 11	. . . . . 6 ⊢ (⊤ → ((𝟭‘ℕ) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏)))
235		fveq2 6885	. . . . . 6 ⊢ (𝑏 = (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) → ((𝟭‘ℕ)‘𝑏) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
236	224, 225, 234, 235	fmptco 7130	. . . . 5 ⊢ (⊤ → (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))))
237	236	mptru 1576	. . . 4 ⊢ (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
238	213, 237	eqtr4i 2786	. . 3 ⊢ 𝐺 = (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
239		f1oeq1 6812	. . 3 ⊢ (𝐺 = (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) → (𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅) ↔ (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))):(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅)))
240	238, 239	ax-mp 5	. 2 ⊢ (𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅) ↔ (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))):(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅))
241	212, 240	mpbir 234	1 ⊢ 𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1569  ⊤wtru 1570   ∈ wcel 2144  {cab 2738  ∀wral 3076  ∃wrex 3086  {crab 3412  Vcvv 3450   ⊆ wss 3895   ∖ cdif 4045   ∩ cin 4089   ∪ cun 4149  ∅c0 4278  𝒫 cpw 4556  {csn 4584  {cpr 4586   class class class wbr 5102  {copab 5166   ↦ cmpt 5185   × cxp 5648  ^◡ccnv 5649  ran crn 5651   ↾ cres 5652   “ cima 5653   ∘ ccom 5654  Fun wfun 6532   Fn wfn 6533  ⟶wf 6534  –1-1→wf1 6535  –1-1-onto→wf1o 6537  ‘cfv 6538  (class class class)co 7420   ∈ cmpo 7422   supp csupp 8179   ↑_m cmap 8850  Fincfn 8976   finSupp cfsupp 9356  0cc0 11203  1c1 11204   · cmul 11208   ≤ cle 11347  𝟭cind 12323  ℕcn 12338  2c2 12400  ℕ₀cn0 12609  ℤcz 12696  ↑cexp 14207  Σcsu 15858   ∥ cdvds 16427  bitscbits 16594

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-inf2 9645  ax-cnex 11259  ax-resscn 11260  ax-1cn 11261  ax-icn 11262  ax-addcl 11263  ax-addrcl 11264  ax-mulcl 11265  ax-mulrcl 11266  ax-mulcom 11267  ax-addass 11268  ax-mulass 11269  ax-distr 11270  ax-i2m1 11271  ax-1ne0 11272  ax-1rid 11273  ax-rnegex 11274  ax-rrecex 11275  ax-cnre 11276  ax-pre-lttri 11277  ax-pre-lttrn 11278  ax-pre-ltadd 11279  ax-pre-mulgt0 11280  ax-pre-sup 11281

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-int 4907  df-iun 4952  df-disj 5070  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-se 5604  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-isom 6547  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-1st 8001  df-2nd 8002  df-supp 8180  df-frecs 8302  df-wrecs 8333  df-recs 8382  df-rdg 8421  df-1o 8479  df-2o 8480  df-oadd 8483  df-er 8720  df-map 8852  df-pm 8853  df-en 8977  df-dom 8978  df-sdom 8979  df-fin 8980  df-fsupp 9357  df-sup 9437  df-inf 9438  df-oi 9507  df-dju 9985  df-card 10023  df-acn 10026  df-pnf 11348  df-mnf 11349  df-xr 11350  df-ltxr 11351  df-le 11352  df-sub 11546  df-neg 11547  df-div 11977  df-ind 12324  df-nn 12339  df-2 12408  df-3 12409  df-n0 12610  df-xnn0 12683  df-z 12697  df-uz 12969  df-rp 13124  df-fz 13643  df-fzo 13792  df-fl 13935  df-mod 14013  df-seq 14148  df-exp 14208  df-hash 14478  df-cj 15271  df-re 15272  df-im 15273  df-sqrt 15407  df-abs 15408  df-clim 15660  df-sum 15859  df-dvds 16428  df-bits 16597

This theorem is used by:  eulerpartlemgf  35057  eulerpartlemgs2  35058  eulerpartlemn  35059