Theorem eulerpartgbij 31740

Description: Lemma for eulerpart 31750: 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 11631	. . . . 5 ⊢ ℕ ∈ V
2		indf1ofs 31395	. . . . 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 4128	. . . . . . 7 ⊢ (({0, 1} ↑m ℕ) ∩ {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}) = ({𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} ∩ ({0, 1} ↑m ℕ))
5		eulerpart.r	. . . . . . . 8 ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}
6	5	ineq2i 4136	. . . . . . 7 ⊢ (({0, 1} ↑m ℕ) ∩ 𝑅) = (({0, 1} ↑m ℕ) ∩ {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin})
7		dfrab2 4231	. . . . . . 7 ⊢ {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (◡𝑓 “ ℕ) ∈ Fin} = ({𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} ∩ ({0, 1} ↑m ℕ))
8	4, 6, 7	3eqtr4i 2831	. . . . . 6 ⊢ (({0, 1} ↑m ℕ) ∩ 𝑅) = {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (◡𝑓 “ ℕ) ∈ Fin}
9		elmapfun 8413	. . . . . . . . 9 ⊢ (𝑓 ∈ ({0, 1} ↑m ℕ) → Fun 𝑓)
10		elmapi 8411	. . . . . . . . . 10 ⊢ (𝑓 ∈ ({0, 1} ↑m ℕ) → 𝑓:ℕ⟶{0, 1})
11	10	frnd 6494	. . . . . . . . 9 ⊢ (𝑓 ∈ ({0, 1} ↑m ℕ) → ran 𝑓 ⊆ {0, 1})
12		fimacnvinrn2 6818	. . . . . . . . . 10 ⊢ ((Fun 𝑓 ∧ ran 𝑓 ⊆ {0, 1}) → (◡𝑓 “ ℕ) = (◡𝑓 “ (ℕ ∩ {0, 1})))
13		df-pr 4528	. . . . . . . . . . . . . 14 ⊢ {0, 1} = ({0} ∪ {1})
14	13	ineq2i 4136	. . . . . . . . . . . . 13 ⊢ (ℕ ∩ {0, 1}) = (ℕ ∩ ({0} ∪ {1}))
15		indi 4200	. . . . . . . . . . . . 13 ⊢ (ℕ ∩ ({0} ∪ {1})) = ((ℕ ∩ {0}) ∪ (ℕ ∩ {1}))
16		0nnn 11661	. . . . . . . . . . . . . . 15 ⊢ ¬ 0 ∈ ℕ
17		disjsn 4607	. . . . . . . . . . . . . . 15 ⊢ ((ℕ ∩ {0}) = ∅ ↔ ¬ 0 ∈ ℕ)
18	16, 17	mpbir 234	. . . . . . . . . . . . . 14 ⊢ (ℕ ∩ {0}) = ∅
19		1nn 11636	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℕ
20		1ex 10626	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ V
21	20	snss 4679	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ ℕ ↔ {1} ⊆ ℕ)
22	19, 21	mpbi 233	. . . . . . . . . . . . . . . 16 ⊢ {1} ⊆ ℕ
23		dfss 3899	. . . . . . . . . . . . . . . 16 ⊢ ({1} ⊆ ℕ ↔ {1} = ({1} ∩ ℕ))
24	22, 23	mpbi 233	. . . . . . . . . . . . . . 15 ⊢ {1} = ({1} ∩ ℕ)
25		incom 4128	. . . . . . . . . . . . . . 15 ⊢ ({1} ∩ ℕ) = (ℕ ∩ {1})
26	24, 25	eqtr2i 2822	. . . . . . . . . . . . . 14 ⊢ (ℕ ∩ {1}) = {1}
27	18, 26	uneq12i 4088	. . . . . . . . . . . . 13 ⊢ ((ℕ ∩ {0}) ∪ (ℕ ∩ {1})) = (∅ ∪ {1})
28	14, 15, 27	3eqtri 2825	. . . . . . . . . . . 12 ⊢ (ℕ ∩ {0, 1}) = (∅ ∪ {1})
29		uncom 4080	. . . . . . . . . . . 12 ⊢ (∅ ∪ {1}) = ({1} ∪ ∅)
30		un0 4298	. . . . . . . . . . . 12 ⊢ ({1} ∪ ∅) = {1}
31	28, 29, 30	3eqtri 2825	. . . . . . . . . . 11 ⊢ (ℕ ∩ {0, 1}) = {1}
32	31	imaeq2i 5894	. . . . . . . . . 10 ⊢ (◡𝑓 “ (ℕ ∩ {0, 1})) = (◡𝑓 “ {1})
33	12, 32	eqtrdi 2849	. . . . . . . . 9 ⊢ ((Fun 𝑓 ∧ ran 𝑓 ⊆ {0, 1}) → (◡𝑓 “ ℕ) = (◡𝑓 “ {1}))
34	9, 11, 33	syl2anc 587	. . . . . . . 8 ⊢ (𝑓 ∈ ({0, 1} ↑m ℕ) → (◡𝑓 “ ℕ) = (◡𝑓 “ {1}))
35	34	eleq1d 2874	. . . . . . 7 ⊢ (𝑓 ∈ ({0, 1} ↑m ℕ) → ((◡𝑓 “ ℕ) ∈ Fin ↔ (◡𝑓 “ {1}) ∈ Fin))
36	35	rabbiia 3419	. . . . . 6 ⊢ {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (◡𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (◡𝑓 “ {1}) ∈ Fin}
37	8, 36	eqtr2i 2822	. . . . 5 ⊢ {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (◡𝑓 “ {1}) ∈ Fin} = (({0, 1} ↑m ℕ) ∩ 𝑅)
38		f1oeq3 6581	. . . . 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 31722	. . . . . 6 ⊢ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ
44		f1opwfi 8812	. . . . . 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 31735	. . . . . . 7 ⊢ 𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
52		bitsf1o 15784	. . . . . . . . . . . . . 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 5201	. . . . . . . . . . . . . 14 ⊢ 𝐽 ∈ V
55	54	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → 𝐽 ∈ V)
56		nn0ex 11891	. . . . . . . . . . . . . 14 ⊢ ℕ0 ∈ V
57	56	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → ℕ0 ∈ V)
58	56	pwex 5246	. . . . . . . . . . . . . . 15 ⊢ 𝒫 ℕ0 ∈ V
59	58	inex1 5185	. . . . . . . . . . . . . 14 ⊢ (𝒫 ℕ0 ∩ Fin) ∈ V
60	59	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝒫 ℕ0 ∩ Fin) ∈ V)
61		0nn0 11900	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℕ0
62	61	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → 0 ∈ ℕ0)
63		fvres 6664	. . . . . . . . . . . . . . 15 ⊢ (0 ∈ ℕ0 → ((bits ↾ ℕ0)‘0) = (bits‘0))
64	61, 63	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((bits ↾ ℕ0)‘0) = (bits‘0)
65		0bits 15778	. . . . . . . . . . . . . 14 ⊢ (bits‘0) = ∅
66	64, 65	eqtr2i 2822	. . . . . . . . . . . . 13 ⊢ ∅ = ((bits ↾ ℕ0)‘0)
67		elmapi 8411	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ (ℕ0 ↑m 𝐽) → 𝑓:𝐽⟶ℕ0)
68		frnnn0supp 11941	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ V ∧ 𝑓:𝐽⟶ℕ0) → (𝑓 supp 0) = (◡𝑓 “ ℕ))
69	54, 67, 68	sylancr 590	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ (ℕ0 ↑m 𝐽) → (𝑓 supp 0) = (◡𝑓 “ ℕ))
70	69	eleq1d 2874	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ (ℕ0 ↑m 𝐽) → ((𝑓 supp 0) ∈ Fin ↔ (◡𝑓 “ ℕ) ∈ Fin))
71	70	rabbiia 3419	. . . . . . . . . . . . . 14 ⊢ {𝑓 ∈ (ℕ0 ↑m 𝐽) ∣ (𝑓 supp 0) ∈ Fin} = {𝑓 ∈ (ℕ0 ↑m 𝐽) ∣ (◡𝑓 “ ℕ) ∈ Fin}
72		elmapfun 8413	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ (ℕ0 ↑m 𝐽) → Fun 𝑓)
73		vex 3444	. . . . . . . . . . . . . . . . 17 ⊢ 𝑓 ∈ V
74		funisfsupp 8822	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝑓 ∧ 𝑓 ∈ V ∧ 0 ∈ ℕ0) → (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
75	73, 61, 74	mp3an23 1450	. . . . . . . . . . . . . . . 16 ⊢ (Fun 𝑓 → (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
76	72, 75	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ (ℕ0 ↑m 𝐽) → (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
77	76	rabbiia 3419	. . . . . . . . . . . . . 14 ⊢ {𝑓 ∈ (ℕ0 ↑m 𝐽) ∣ 𝑓 finSupp 0} = {𝑓 ∈ (ℕ0 ↑m 𝐽) ∣ (𝑓 supp 0) ∈ Fin}
78		incom 4128	. . . . . . . . . . . . . . 15 ⊢ ({𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} ∩ (ℕ0 ↑m 𝐽)) = ((ℕ0 ↑m 𝐽) ∩ {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin})
79		dfrab2 4231	. . . . . . . . . . . . . . 15 ⊢ {𝑓 ∈ (ℕ0 ↑m 𝐽) ∣ (◡𝑓 “ ℕ) ∈ Fin} = ({𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} ∩ (ℕ0 ↑m 𝐽))
80	5	ineq2i 4136	. . . . . . . . . . . . . . 15 ⊢ ((ℕ0 ↑m 𝐽) ∩ 𝑅) = ((ℕ0 ↑m 𝐽) ∩ {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin})
81	78, 79, 80	3eqtr4ri 2832	. . . . . . . . . . . . . 14 ⊢ ((ℕ0 ↑m 𝐽) ∩ 𝑅) = {𝑓 ∈ (ℕ0 ↑m 𝐽) ∣ (◡𝑓 “ ℕ) ∈ Fin}
82	71, 77, 81	3eqtr4ri 2832	. . . . . . . . . . . . 13 ⊢ ((ℕ0 ↑m 𝐽) ∩ 𝑅) = {𝑓 ∈ (ℕ0 ↑m 𝐽) ∣ 𝑓 finSupp 0}
83		elmapfun 8413	. . . . . . . . . . . . . . 15 ⊢ (𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) → Fun 𝑟)
84		vex 3444	. . . . . . . . . . . . . . . . 17 ⊢ 𝑟 ∈ V
85		0ex 5175	. . . . . . . . . . . . . . . . 17 ⊢ ∅ ∈ V
86		funisfsupp 8822	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝑟 ∧ 𝑟 ∈ V ∧ ∅ ∈ V) → (𝑟 finSupp ∅ ↔ (𝑟 supp ∅) ∈ Fin))
87	84, 85, 86	mp3an23 1450	. . . . . . . . . . . . . . . 16 ⊢ (Fun 𝑟 → (𝑟 finSupp ∅ ↔ (𝑟 supp ∅) ∈ Fin))
88	87	bicomd 226	. . . . . . . . . . . . . . 15 ⊢ (Fun 𝑟 → ((𝑟 supp ∅) ∈ Fin ↔ 𝑟 finSupp ∅))
89	83, 88	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) → ((𝑟 supp ∅) ∈ Fin ↔ 𝑟 finSupp ∅))
90	89	rabbiia 3419	. . . . . . . . . . . . 13 ⊢ {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ 𝑟 finSupp ∅}
91	53, 55, 57, 60, 62, 66, 82, 90	fcobijfs 30485	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)):((ℕ0 ↑m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
92		elinel1 4122	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) → 𝑓 ∈ (ℕ0 ↑m 𝐽))
93		frn 6493	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓:𝐽⟶ℕ0 → ran 𝑓 ⊆ ℕ0)
94		cores 6069	. . . . . . . . . . . . . . . . 17 ⊢ (ran 𝑓 ⊆ ℕ0 → ((bits ↾ ℕ0) ∘ 𝑓) = (bits ∘ 𝑓))
95	67, 93, 94	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ (ℕ0 ↑m 𝐽) → ((bits ↾ ℕ0) ∘ 𝑓) = (bits ∘ 𝑓))
96	92, 95	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) → ((bits ↾ ℕ0) ∘ 𝑓) = (bits ∘ 𝑓))
97	96	mpteq2ia 5121	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)) = (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓))
98	97	eqcomi 2807	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓))
99		f1oeq1 6579	. . . . . . . . . . . . 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}))
100	98, 99	mp1i 13	. . . . . . . . . . . 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}))
101	91, 100	mpbird 260	. . . . . . . . . . 11 ⊢ (⊤ → (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0 ↑m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
102	101	mptru 1545	. . . . . . . . . 10 ⊢ (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0 ↑m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
103		ssrab2 4007	. . . . . . . . . . . . . . . 16 ⊢ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ⊆ ℕ
104	41, 103	eqsstri 3949	. . . . . . . . . . . . . . 15 ⊢ 𝐽 ⊆ ℕ
105	1, 56, 104	3pm3.2i 1336	. . . . . . . . . . . . . 14 ⊢ (ℕ ∈ V ∧ ℕ0 ∈ V ∧ 𝐽 ⊆ ℕ)
106		eulerpart.t	. . . . . . . . . . . . . . . 16 ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}
107		cnveq 5708	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = 𝑜 → ◡𝑓 = ◡𝑜)
108		dfn2 11898	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ = (ℕ0 ∖ {0})
109	108	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = 𝑜 → ℕ = (ℕ0 ∖ {0}))
110	107, 109	imaeq12d 5897	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = 𝑜 → (◡𝑓 “ ℕ) = (◡𝑜 “ (ℕ0 ∖ {0})))
111	110	sseq1d 3946	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑜 → ((◡𝑓 “ ℕ) ⊆ 𝐽 ↔ (◡𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽))
112	111	cbvrabv 3439	. . . . . . . . . . . . . . . 16 ⊢ {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽} = {𝑜 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽}
113	106, 112	eqtri 2821	. . . . . . . . . . . . . . 15 ⊢ 𝑇 = {𝑜 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽}
114		eqid 2798	. . . . . . . . . . . . . . 15 ⊢ (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) = (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))
115	113, 114	resf1o 30492	. . . . . . . . . . . . . 14 ⊢ (((ℕ ∈ V ∧ ℕ0 ∈ V ∧ 𝐽 ⊆ ℕ) ∧ 0 ∈ ℕ0) → (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1-onto→(ℕ0 ↑m 𝐽))
116	105, 61, 115	mp2an 691	. . . . . . . . . . . . 13 ⊢ (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1-onto→(ℕ0 ↑m 𝐽)
117		f1of1 6589	. . . . . . . . . . . . 13 ⊢ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1-onto→(ℕ0 ↑m 𝐽) → (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1→(ℕ0 ↑m 𝐽))
118	116, 117	ax-mp 5	. . . . . . . . . . . 12 ⊢ (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1→(ℕ0 ↑m 𝐽)
119		inss1 4155	. . . . . . . . . . . 12 ⊢ (𝑇 ∩ 𝑅) ⊆ 𝑇
120		f1ores 6604	. . . . . . . . . . . 12 ⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1→(ℕ0 ↑m 𝐽) ∧ (𝑇 ∩ 𝑅) ⊆ 𝑇) → ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)))
121	118, 119, 120	mp2an 691	. . . . . . . . . . 11 ⊢ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅))
122		vex 3444	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑜 ∈ V
123	122	resex 5866	. . . . . . . . . . . . . . . . 17 ⊢ (𝑜 ↾ 𝐽) ∈ V
124	123, 114	fnmpti 6463	. . . . . . . . . . . . . . . 16 ⊢ (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) Fn 𝑇
125		fvelimab 6712	. . . . . . . . . . . . . . . 16 ⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) Fn 𝑇 ∧ (𝑇 ∩ 𝑅) ⊆ 𝑇) → (𝑓 ∈ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓))
126	124, 119, 125	mp2an 691	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓)
127		eqid 2798	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) = (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽))
128		vex 3444	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑚 ∈ V
129	128	resex 5866	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ↾ 𝐽) ∈ V
130	127, 129	elrnmpti 5796	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑓 = (𝑚 ↾ 𝐽))
131	46, 47, 48, 41, 42, 49, 50, 5, 106	eulerpartlemt 31739	. . . . . . . . . . . . . . . . 17 ⊢ ((ℕ0 ↑m 𝐽) ∩ 𝑅) = ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽))
132	131	eleq2i 2881	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↔ 𝑓 ∈ ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)))
133		elinel1 4122	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) → 𝑚 ∈ 𝑇)
134	114	fvtresfn 6747	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ 𝑇 → ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = (𝑚 ↾ 𝐽))
135	134	eqeq1d 2800	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ 𝑇 → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ (𝑚 ↾ 𝐽) = 𝑓))
136	133, 135	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ (𝑚 ↾ 𝐽) = 𝑓))
137		eqcom 2805	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 ↾ 𝐽) = 𝑓 ↔ 𝑓 = (𝑚 ↾ 𝐽))
138	136, 137	syl6bb 290	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ 𝑓 = (𝑚 ↾ 𝐽)))
139	138	rexbiia 3209	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑚 ∈ (𝑇 ∩ 𝑅)((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑓 = (𝑚 ↾ 𝐽))
140	130, 132, 139	3bitr4ri 307	. . . . . . . . . . . . . . 15 ⊢ (∃𝑚 ∈ (𝑇 ∩ 𝑅)((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ 𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅))
141	126, 140	bitri 278	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ 𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅))
142	141	eqriv 2795	. . . . . . . . . . . . 13 ⊢ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) = ((ℕ0 ↑m 𝐽) ∩ 𝑅)
143		f1oeq3 6581	. . . . . . . . . . . . 13 ⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) = ((ℕ0 ↑m 𝐽) ∩ 𝑅) → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅)))
144	142, 143	ax-mp 5	. . . . . . . . . . . 12 ⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅))
145		resmpt 5872	. . . . . . . . . . . . 13 ⊢ ((𝑇 ∩ 𝑅) ⊆ 𝑇 → ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)))
146		f1oeq1 6579	. . . . . . . . . . . . 13 ⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)) → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅)))
147	119, 145, 146	mp2b 10	. . . . . . . . . . . 12 ⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅))
148	144, 147	bitri 278	. . . . . . . . . . 11 ⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅))
149	121, 148	mpbi 233	. . . . . . . . . 10 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅)
150		f1oco 6612	. . . . . . . . . 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})
151	102, 149, 150	mp2an 691	. . . . . . . . 9 ⊢ ((𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
152		f1of 6590	. . . . . . . . . . . . . 14 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅) → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)⟶((ℕ0 ↑m 𝐽) ∩ 𝑅))
153		eqid 2798	. . . . . . . . . . . . . . . 16 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))
154	153	fmpt 6851	. . . . . . . . . . . . . . 15 ⊢ (∀𝑜 ∈ (𝑇 ∩ 𝑅)(𝑜 ↾ 𝐽) ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)⟶((ℕ0 ↑m 𝐽) ∩ 𝑅))
155	154	biimpri 231	. . . . . . . . . . . . . 14 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)⟶((ℕ0 ↑m 𝐽) ∩ 𝑅) → ∀𝑜 ∈ (𝑇 ∩ 𝑅)(𝑜 ↾ 𝐽) ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅))
156	149, 152, 155	mp2b 10	. . . . . . . . . . . . 13 ⊢ ∀𝑜 ∈ (𝑇 ∩ 𝑅)(𝑜 ↾ 𝐽) ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅)
157	156	a1i 11	. . . . . . . . . . . 12 ⊢ (⊤ → ∀𝑜 ∈ (𝑇 ∩ 𝑅)(𝑜 ↾ 𝐽) ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅))
158		eqidd 2799	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)))
159		eqidd 2799	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)))
160		coeq2 5693	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑜 ↾ 𝐽) → (bits ∘ 𝑓) = (bits ∘ (𝑜 ↾ 𝐽)))
161	157, 158, 159, 160	fmptcof 6869	. . . . . . . . . . 11 ⊢ (⊤ → ((𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))))
162	161	eqcomd 2804	. . . . . . . . . 10 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))) = ((𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))))
163		eqidd 2799	. . . . . . . . . 10 ⊢ (⊤ → (𝑇 ∩ 𝑅) = (𝑇 ∩ 𝑅))
164	49	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
165	162, 163, 164	f1oeq123d 6585	. . . . . . . . 9 ⊢ (⊤ → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻 ↔ ((𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}))
166	151, 165	mpbiri 261	. . . . . . . 8 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻)
167	166	mptru 1545	. . . . . . 7 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻
168		f1oco 6612	. . . . . . 7 ⊢ ((𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) ∧ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻) → (𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin))
169	51, 167, 168	mp2an 691	. . . . . 6 ⊢ (𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
170		eqidd 2799	. . . . . . . . . . 11 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))))
171		bitsf 15766	. . . . . . . . . . . . . 14 ⊢ bits:ℤ⟶𝒫 ℕ0
172		zex 11978	. . . . . . . . . . . . . 14 ⊢ ℤ ∈ V
173		fex 6966	. . . . . . . . . . . . . 14 ⊢ ((bits:ℤ⟶𝒫 ℕ0 ∧ ℤ ∈ V) → bits ∈ V)
174	171, 172, 173	mp2an 691	. . . . . . . . . . . . 13 ⊢ bits ∈ V
175	174, 123	coex 7617	. . . . . . . . . . . 12 ⊢ (bits ∘ (𝑜 ↾ 𝐽)) ∈ V
176	175	a1i 11	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → (bits ∘ (𝑜 ↾ 𝐽)) ∈ V)
177	170, 176	fvmpt2d 6758	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))‘𝑜) = (bits ∘ (𝑜 ↾ 𝐽)))
178		f1of 6590	. . . . . . . . . . . 12 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻 → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)⟶𝐻)
179	166, 178	syl 17	. . . . . . . . . . 11 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)⟶𝐻)
180	179	ffvelrnda 6828	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))‘𝑜) ∈ 𝐻)
181	177, 180	eqeltrrd 2891	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → (bits ∘ (𝑜 ↾ 𝐽)) ∈ 𝐻)
182		f1ofn 6591	. . . . . . . . . . . 12 ⊢ (𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) → 𝑀 Fn 𝐻)
183	51, 182	ax-mp 5	. . . . . . . . . . 11 ⊢ 𝑀 Fn 𝐻
184		dffn5 6699	. . . . . . . . . . 11 ⊢ (𝑀 Fn 𝐻 ↔ 𝑀 = (𝑟 ∈ 𝐻 ↦ (𝑀‘𝑟)))
185	183, 184	mpbi 233	. . . . . . . . . 10 ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ (𝑀‘𝑟))
186	185	a1i 11	. . . . . . . . 9 ⊢ (⊤ → 𝑀 = (𝑟 ∈ 𝐻 ↦ (𝑀‘𝑟)))
187		fveq2 6645	. . . . . . . . 9 ⊢ (𝑟 = (bits ∘ (𝑜 ↾ 𝐽)) → (𝑀‘𝑟) = (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))
188	181, 170, 186, 187	fmptco 6868	. . . . . . . 8 ⊢ (⊤ → (𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
189	188	mptru 1545	. . . . . . 7 ⊢ (𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))
190		f1oeq1 6579	. . . . . . 7 ⊢ ((𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) → ((𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)))
191	189, 190	ax-mp 5	. . . . . 6 ⊢ ((𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin))
192	169, 191	mpbi 233	. . . . 5 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
193		f1oco 6612	. . . . 5 ⊢ (((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)):(𝒫 (𝐽 × ℕ0) ∩ Fin)–1-1-onto→(𝒫 ℕ ∩ Fin) ∧ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)) → ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin))
194	45, 192, 193	mp2an 691	. . . 4 ⊢ ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)
195		simpr 488	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → 𝑜 ∈ (𝑇 ∩ 𝑅))
196		fvex 6658	. . . . . . . . 9 ⊢ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))) ∈ V
197		eqid 2798	. . . . . . . . . 10 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))
198	197	fvmpt2 6756	. . . . . . . . 9 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ∧ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))) ∈ V) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))‘𝑜) = (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))
199	195, 196, 198	sylancl 589	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))‘𝑜) = (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))
200		f1of 6590	. . . . . . . . . 10 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)⟶(𝒫 (𝐽 × ℕ0) ∩ Fin))
201	192, 200	mp1i 13	. . . . . . . . 9 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)⟶(𝒫 (𝐽 × ℕ0) ∩ Fin))
202	201	ffvelrnda 6828	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))‘𝑜) ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin))
203	199, 202	eqeltrrd 2891	. . . . . . 7 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))) ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin))
204		eqidd 2799	. . . . . . 7 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
205		eqidd 2799	. . . . . . 7 ⊢ (⊤ → (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) = (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)))
206		imaeq2 5892	. . . . . . 7 ⊢ (𝑎 = (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))) → (𝐹 “ 𝑎) = (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
207	203, 204, 205, 206	fmptco 6868	. . . . . 6 ⊢ (⊤ → ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
208	207	mptru 1545	. . . . 5 ⊢ ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
209		f1oeq1 6579	. . . . 5 ⊢ (((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) → (((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)))
210	208, 209	ax-mp 5	. . . 4 ⊢ (((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin))
211	194, 210	mpbi 233	. . 3 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)
212		f1oco 6612	. . 3 ⊢ ((((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅) ∧ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)) → (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))):(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅))
213	40, 211, 212	mp2an 691	. 2 ⊢ (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))):(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅)
214		eulerpart.g	. . . 4 ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
215	42	mpoexg 7757	. . . . . . . . . 10 ⊢ ((𝐽 ∈ V ∧ ℕ0 ∈ V) → 𝐹 ∈ V)
216	54, 56, 215	mp2an 691	. . . . . . . . 9 ⊢ 𝐹 ∈ V
217		imaexg 7602	. . . . . . . . 9 ⊢ (𝐹 ∈ V → (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) ∈ V)
218	216, 217	ax-mp 5	. . . . . . . 8 ⊢ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) ∈ V
219		eqid 2798	. . . . . . . . 9 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
220	219	fvmpt2 6756	. . . . . . . 8 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ∧ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) ∈ V) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))‘𝑜) = (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
221	195, 218, 220	sylancl 589	. . . . . . 7 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))‘𝑜) = (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
222		f1of 6590	. . . . . . . . 9 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin) → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)⟶(𝒫 ℕ ∩ Fin))
223	211, 222	mp1i 13	. . . . . . . 8 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)⟶(𝒫 ℕ ∩ Fin))
224	223	ffvelrnda 6828	. . . . . . 7 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))‘𝑜) ∈ (𝒫 ℕ ∩ Fin))
225	221, 224	eqeltrrd 2891	. . . . . 6 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) ∈ (𝒫 ℕ ∩ Fin))
226		eqidd 2799	. . . . . 6 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
227		indf1o 31393	. . . . . . . . . . 11 ⊢ (ℕ ∈ V → (𝟭‘ℕ):𝒫 ℕ–1-1-onto→({0, 1} ↑m ℕ))
228		f1ofn 6591	. . . . . . . . . . 11 ⊢ ((𝟭‘ℕ):𝒫 ℕ–1-1-onto→({0, 1} ↑m ℕ) → (𝟭‘ℕ) Fn 𝒫 ℕ)
229	1, 227, 228	mp2b 10	. . . . . . . . . 10 ⊢ (𝟭‘ℕ) Fn 𝒫 ℕ
230		dffn5 6699	. . . . . . . . . 10 ⊢ ((𝟭‘ℕ) Fn 𝒫 ℕ ↔ (𝟭‘ℕ) = (𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)))
231	229, 230	mpbi 233	. . . . . . . . 9 ⊢ (𝟭‘ℕ) = (𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏))
232	231	reseq1i 5814	. . . . . . . 8 ⊢ ((𝟭‘ℕ) ↾ Fin) = ((𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)) ↾ Fin)
233		resmpt3 5873	. . . . . . . 8 ⊢ ((𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏))
234	232, 233	eqtri 2821	. . . . . . 7 ⊢ ((𝟭‘ℕ) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏))
235	234	a1i 11	. . . . . 6 ⊢ (⊤ → ((𝟭‘ℕ) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏)))
236		fveq2 6645	. . . . . 6 ⊢ (𝑏 = (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) → ((𝟭‘ℕ)‘𝑏) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
237	225, 226, 235, 236	fmptco 6868	. . . . 5 ⊢ (⊤ → (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))))
238	237	mptru 1545	. . . 4 ⊢ (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
239	214, 238	eqtr4i 2824	. . 3 ⊢ 𝐺 = (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
240		f1oeq1 6579	. . 3 ⊢ (𝐺 = (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) → (𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅) ↔ (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))):(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅)))
241	239, 240	ax-mp 5	. 2 ⊢ (𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅) ↔ (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))):(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅))
242	213, 241	mpbir 234	1 ⊢ 𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅)

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ⊤wtru 1539   ∈ wcel 2111  {cab 2776  ∀wral 3106  ∃wrex 3107  {crab 3110  Vcvv 3441   ∖ cdif 3878   ∪ cun 3879   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  𝒫 cpw 4497  {csn 4525  {cpr 4527   class class class wbr 5030  {copab 5092   ↦ cmpt 5110   × cxp 5517  ^◡ccnv 5518  ran crn 5520   ↾ cres 5521   “ cima 5522   ∘ ccom 5523  Fun wfun 6318   Fn wfn 6319  ⟶wf 6320  –1-1→wf1 6321  –1-1-onto→wf1o 6323  ‘cfv 6324  (class class class)co 7135   ∈ cmpo 7137   supp csupp 7813   ↑_m cmap 8389  Fincfn 8492   finSupp cfsupp 8817  0cc0 10526  1c1 10527   · cmul 10531   ≤ cle 10665  ℕcn 11625  2c2 11680  ℕ₀cn0 11885  ℤcz 11969  ↑cexp 13425  Σcsu 15034   ∥ cdvds 15599  bitscbits 15758  𝟭cind 31379

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-inf2 9088  ax-ac2 9874  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-disj 4996  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7561  df-1st 7671  df-2nd 7672  df-supp 7814  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-2o 8086  df-oadd 8089  df-er 8272  df-map 8391  df-pm 8392  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496  df-fsupp 8818  df-sup 8890  df-inf 8891  df-oi 8958  df-dju 9314  df-card 9352  df-acn 9355  df-ac 9527  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-3 11689  df-n0 11886  df-xnn0 11956  df-z 11970  df-uz 12232  df-rp 12378  df-fz 12886  df-fzo 13029  df-fl 13157  df-mod 13233  df-seq 13365  df-exp 13426  df-hash 13687  df-cj 14450  df-re 14451  df-im 14452  df-sqrt 14586  df-abs 14587  df-clim 14837  df-sum 15035  df-dvds 15600  df-bits 15761  df-ind 31380

This theorem is referenced by:  eulerpartlemgf  31747  eulerpartlemgs2  31748  eulerpartlemn  31749