Theorem eulerpartgbij 34793

Description: Lemma for eulerpart 34803: 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 12257	. . . . 5 ⊢ ℕ ∈ V
2		indf1ofs 33223	. . . . 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 4165	. . . . . . 7 ⊢ (({0, 1} ↑m ℕ) ∩ {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}) = ({𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} ∩ ({0, 1} ↑m ℕ))
5		eulerpart.r	. . . . . . . 8 ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}
6	5	ineq2i 4173	. . . . . . 7 ⊢ (({0, 1} ↑m ℕ) ∩ 𝑅) = (({0, 1} ↑m ℕ) ∩ {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin})
7		dfrab2 4276	. . . . . . 7 ⊢ {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (◡𝑓 “ ℕ) ∈ Fin} = ({𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} ∩ ({0, 1} ↑m ℕ))
8	4, 6, 7	3eqtr4i 2799	. . . . . 6 ⊢ (({0, 1} ↑m ℕ) ∩ 𝑅) = {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (◡𝑓 “ ℕ) ∈ Fin}
9		elmapfun 8872	. . . . . . . . 9 ⊢ (𝑓 ∈ ({0, 1} ↑m ℕ) → Fun 𝑓)
10		elmapi 8855	. . . . . . . . . 10 ⊢ (𝑓 ∈ ({0, 1} ↑m ℕ) → 𝑓:ℕ⟶{0, 1})
11	10	frnd 6721	. . . . . . . . 9 ⊢ (𝑓 ∈ ({0, 1} ↑m ℕ) → ran 𝑓 ⊆ {0, 1})
12		fimacnvinrn2 7074	. . . . . . . . . 10 ⊢ ((Fun 𝑓 ∧ ran 𝑓 ⊆ {0, 1}) → (◡𝑓 “ ℕ) = (◡𝑓 “ (ℕ ∩ {0, 1})))
13		df-pr 4597	. . . . . . . . . . . . . 14 ⊢ {0, 1} = ({0} ∪ {1})
14	13	ineq2i 4173	. . . . . . . . . . . . 13 ⊢ (ℕ ∩ {0, 1}) = (ℕ ∩ ({0} ∪ {1}))
15		indi 4240	. . . . . . . . . . . . 13 ⊢ (ℕ ∩ ({0} ∪ {1})) = ((ℕ ∩ {0}) ∪ (ℕ ∩ {1}))
16		0nnn 12290	. . . . . . . . . . . . . . 15 ⊢ ¬ 0 ∈ ℕ
17		disjsn 4682	. . . . . . . . . . . . . . 15 ⊢ ((ℕ ∩ {0}) = ∅ ↔ ¬ 0 ∈ ℕ)
18	16, 17	mpbir 234	. . . . . . . . . . . . . 14 ⊢ (ℕ ∩ {0}) = ∅
19		1nn 12262	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℕ
20		1ex 11221	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ V
21	20	snss 4755	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ ℕ ↔ {1} ⊆ ℕ)
22	19, 21	mpbi 233	. . . . . . . . . . . . . . . 16 ⊢ {1} ⊆ ℕ
23		dfss 3927	. . . . . . . . . . . . . . . 16 ⊢ ({1} ⊆ ℕ ↔ {1} = ({1} ∩ ℕ))
24	22, 23	mpbi 233	. . . . . . . . . . . . . . 15 ⊢ {1} = ({1} ∩ ℕ)
25		incom 4165	. . . . . . . . . . . . . . 15 ⊢ ({1} ∩ ℕ) = (ℕ ∩ {1})
26	24, 25	eqtr2i 2790	. . . . . . . . . . . . . 14 ⊢ (ℕ ∩ {1}) = {1}
27	18, 26	uneq12i 4123	. . . . . . . . . . . . 13 ⊢ ((ℕ ∩ {0}) ∪ (ℕ ∩ {1})) = (∅ ∪ {1})
28	14, 15, 27	3eqtri 2793	. . . . . . . . . . . 12 ⊢ (ℕ ∩ {0, 1}) = (∅ ∪ {1})
29		uncom 4115	. . . . . . . . . . . 12 ⊢ (∅ ∪ {1}) = ({1} ∪ ∅)
30		un0 4354	. . . . . . . . . . . 12 ⊢ ({1} ∪ ∅) = {1}
31	28, 29, 30	3eqtri 2793	. . . . . . . . . . 11 ⊢ (ℕ ∩ {0, 1}) = {1}
32	31	imaeq2i 6065	. . . . . . . . . 10 ⊢ (◡𝑓 “ (ℕ ∩ {0, 1})) = (◡𝑓 “ {1})
33	12, 32	eqtrdi 2817	. . . . . . . . 9 ⊢ ((Fun 𝑓 ∧ ran 𝑓 ⊆ {0, 1}) → (◡𝑓 “ ℕ) = (◡𝑓 “ {1}))
34	9, 11, 33	syl2anc 596	. . . . . . . 8 ⊢ (𝑓 ∈ ({0, 1} ↑m ℕ) → (◡𝑓 “ ℕ) = (◡𝑓 “ {1}))
35	34	eleq1d 2851	. . . . . . 7 ⊢ (𝑓 ∈ ({0, 1} ↑m ℕ) → ((◡𝑓 “ ℕ) ∈ Fin ↔ (◡𝑓 “ {1}) ∈ Fin))
36	35	rabbiia 3423	. . . . . 6 ⊢ {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (◡𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (◡𝑓 “ {1}) ∈ Fin}
37	8, 36	eqtr2i 2790	. . . . 5 ⊢ {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (◡𝑓 “ {1}) ∈ Fin} = (({0, 1} ↑m ℕ) ∩ 𝑅)
38		f1oeq3 6817	. . . . 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 34775	. . . . . 6 ⊢ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ
44		f1opwfi 9323	. . . . . 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 34788	. . . . . . 7 ⊢ 𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
52		bitsf1o 16528	. . . . . . . . . . . . . 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 5316	. . . . . . . . . . . . . 14 ⊢ 𝐽 ∈ V
55	54	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → 𝐽 ∈ V)
56		nn0ex 12528	. . . . . . . . . . . . . 14 ⊢ ℕ0 ∈ V
57	56	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → ℕ0 ∈ V)
58	56	pwex 5356	. . . . . . . . . . . . . . 15 ⊢ 𝒫 ℕ0 ∈ V
59	58	inex1 5291	. . . . . . . . . . . . . 14 ⊢ (𝒫 ℕ0 ∩ Fin) ∈ V
60	59	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝒫 ℕ0 ∩ Fin) ∈ V)
61		0nn0 12537	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℕ0
62	61	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → 0 ∈ ℕ0)
63		fvres 6907	. . . . . . . . . . . . . . 15 ⊢ (0 ∈ ℕ0 → ((bits ↾ ℕ0)‘0) = (bits‘0))
64	61, 63	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((bits ↾ ℕ0)‘0) = (bits‘0)
65		0bits 16522	. . . . . . . . . . . . . 14 ⊢ (bits‘0) = ∅
66	64, 65	eqtr2i 2790	. . . . . . . . . . . . 13 ⊢ ∅ = ((bits ↾ ℕ0)‘0)
67		elmapi 8855	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ (ℕ0 ↑m 𝐽) → 𝑓:𝐽⟶ℕ0)
68		fcdmnn0supp 12579	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ V ∧ 𝑓:𝐽⟶ℕ0) → (𝑓 supp 0) = (◡𝑓 “ ℕ))
69	54, 67, 68	sylancr 599	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ (ℕ0 ↑m 𝐽) → (𝑓 supp 0) = (◡𝑓 “ ℕ))
70	69	eleq1d 2851	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ (ℕ0 ↑m 𝐽) → ((𝑓 supp 0) ∈ Fin ↔ (◡𝑓 “ ℕ) ∈ Fin))
71	70	rabbiia 3423	. . . . . . . . . . . . . 14 ⊢ {𝑓 ∈ (ℕ0 ↑m 𝐽) ∣ (𝑓 supp 0) ∈ Fin} = {𝑓 ∈ (ℕ0 ↑m 𝐽) ∣ (◡𝑓 “ ℕ) ∈ Fin}
72		elmapfun 8872	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ (ℕ0 ↑m 𝐽) → Fun 𝑓)
73		vex 3462	. . . . . . . . . . . . . . . . 17 ⊢ 𝑓 ∈ V
74		funisfsupp 9337	. . . . . . . . . . . . . . . . 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 3423	. . . . . . . . . . . . . 14 ⊢ {𝑓 ∈ (ℕ0 ↑m 𝐽) ∣ 𝑓 finSupp 0} = {𝑓 ∈ (ℕ0 ↑m 𝐽) ∣ (𝑓 supp 0) ∈ Fin}
78		incom 4165	. . . . . . . . . . . . . . 15 ⊢ ({𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} ∩ (ℕ0 ↑m 𝐽)) = ((ℕ0 ↑m 𝐽) ∩ {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin})
79		dfrab2 4276	. . . . . . . . . . . . . . 15 ⊢ {𝑓 ∈ (ℕ0 ↑m 𝐽) ∣ (◡𝑓 “ ℕ) ∈ Fin} = ({𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} ∩ (ℕ0 ↑m 𝐽))
80	5	ineq2i 4173	. . . . . . . . . . . . . . 15 ⊢ ((ℕ0 ↑m 𝐽) ∩ 𝑅) = ((ℕ0 ↑m 𝐽) ∩ {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin})
81	78, 79, 80	3eqtr4ri 2800	. . . . . . . . . . . . . 14 ⊢ ((ℕ0 ↑m 𝐽) ∩ 𝑅) = {𝑓 ∈ (ℕ0 ↑m 𝐽) ∣ (◡𝑓 “ ℕ) ∈ Fin}
82	71, 77, 81	3eqtr4ri 2800	. . . . . . . . . . . . 13 ⊢ ((ℕ0 ↑m 𝐽) ∩ 𝑅) = {𝑓 ∈ (ℕ0 ↑m 𝐽) ∣ 𝑓 finSupp 0}
83		elmapfun 8872	. . . . . . . . . . . . . . 15 ⊢ (𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) → Fun 𝑟)
84		vex 3462	. . . . . . . . . . . . . . . . 17 ⊢ 𝑟 ∈ V
85		0ex 5275	. . . . . . . . . . . . . . . . 17 ⊢ ∅ ∈ V
86		funisfsupp 9337	. . . . . . . . . . . . . . . . 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 3423	. . . . . . . . . . . . 13 ⊢ {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ 𝑟 finSupp ∅}
91	53, 55, 57, 60, 62, 66, 82, 90	fcobijfs 33103	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)):((ℕ0 ↑m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
92		elinel1 4157	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) → 𝑓 ∈ (ℕ0 ↑m 𝐽))
93		frn 6720	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:𝐽⟶ℕ0 → ran 𝑓 ⊆ ℕ0)
94		cores 6255	. . . . . . . . . . . . . . . 16 ⊢ (ran 𝑓 ⊆ ℕ0 → ((bits ↾ ℕ0) ∘ 𝑓) = (bits ∘ 𝑓))
95	92, 67, 93, 94	4syl 20	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) → ((bits ↾ ℕ0) ∘ 𝑓) = (bits ∘ 𝑓))
96	95	mpteq2ia 5211	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)) = (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓))
97	96	eqcomi 2775	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓))
98		f1oeq1 6815	. . . . . . . . . . . . 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 1577	. . . . . . . . . 10 ⊢ (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0 ↑m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
102		ssrab2 4037	. . . . . . . . . . . . . . . 16 ⊢ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ⊆ ℕ
103	41, 102	eqsstri 3986	. . . . . . . . . . . . . . 15 ⊢ 𝐽 ⊆ ℕ
104	1, 56, 103	3pm3.2i 1358	. . . . . . . . . . . . . 14 ⊢ (ℕ ∈ V ∧ ℕ0 ∈ V ∧ 𝐽 ⊆ ℕ)
105		eulerpart.t	. . . . . . . . . . . . . . . 16 ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}
106		cnveq 5864	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = 𝑜 → ◡𝑓 = ◡𝑜)
107		dfn2 12535	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ = (ℕ0 ∖ {0})
108	107	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = 𝑜 → ℕ = (ℕ0 ∖ {0}))
109	106, 108	imaeq12d 6068	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = 𝑜 → (◡𝑓 “ ℕ) = (◡𝑜 “ (ℕ0 ∖ {0})))
110	109	sseq1d 3971	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑜 → ((◡𝑓 “ ℕ) ⊆ 𝐽 ↔ (◡𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽))
111	110	cbvrabv 3429	. . . . . . . . . . . . . . . 16 ⊢ {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽} = {𝑜 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽}
112	105, 111	eqtri 2789	. . . . . . . . . . . . . . 15 ⊢ 𝑇 = {𝑜 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽}
113		eqid 2766	. . . . . . . . . . . . . . 15 ⊢ (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) = (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))
114	112, 113	resf1o 33112	. . . . . . . . . . . . . 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 6826	. . . . . . . . . . . . 13 ⊢ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1-onto→(ℕ0 ↑m 𝐽) → (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1→(ℕ0 ↑m 𝐽))
117	115, 116	ax-mp 5	. . . . . . . . . . . 12 ⊢ (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1→(ℕ0 ↑m 𝐽)
118		inss1 4192	. . . . . . . . . . . 12 ⊢ (𝑇 ∩ 𝑅) ⊆ 𝑇
119		f1ores 6842	. . . . . . . . . . . 12 ⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1→(ℕ0 ↑m 𝐽) ∧ (𝑇 ∩ 𝑅) ⊆ 𝑇) → ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)))
120	117, 118, 119	mp2an 705	. . . . . . . . . . 11 ⊢ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅))
121		vex 3462	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑜 ∈ V
122	121	resex 6033	. . . . . . . . . . . . . . . . 17 ⊢ (𝑜 ↾ 𝐽) ∈ V
123	122, 113	fnmpti 6685	. . . . . . . . . . . . . . . 16 ⊢ (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) Fn 𝑇
124		fvelimab 6960	. . . . . . . . . . . . . . . 16 ⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) Fn 𝑇 ∧ (𝑇 ∩ 𝑅) ⊆ 𝑇) → (𝑓 ∈ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓))
125	123, 118, 124	mp2an 705	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓)
126		eqid 2766	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) = (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽))
127		vex 3462	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑚 ∈ V
128	127	resex 6033	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ↾ 𝐽) ∈ V
129	126, 128	elrnmpti 5957	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑓 = (𝑚 ↾ 𝐽))
130	46, 47, 48, 41, 42, 49, 50, 5, 105	eulerpartlemt 34792	. . . . . . . . . . . . . . . . 17 ⊢ ((ℕ0 ↑m 𝐽) ∩ 𝑅) = ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽))
131	130	eleq2i 2858	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↔ 𝑓 ∈ ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)))
132		elinel1 4157	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) → 𝑚 ∈ 𝑇)
133	113	fvtresfn 6999	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ 𝑇 → ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = (𝑚 ↾ 𝐽))
134	133	eqeq1d 2768	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ 𝑇 → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ (𝑚 ↾ 𝐽) = 𝑓))
135	132, 134	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ (𝑚 ↾ 𝐽) = 𝑓))
136		eqcom 2773	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 ↾ 𝐽) = 𝑓 ↔ 𝑓 = (𝑚 ↾ 𝐽))
137	135, 136	bitrdi 290	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ 𝑓 = (𝑚 ↾ 𝐽)))
138	137	rexbiia 3113	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑚 ∈ (𝑇 ∩ 𝑅)((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑓 = (𝑚 ↾ 𝐽))
139	129, 131, 138	3bitr4ri 307	. . . . . . . . . . . . . . 15 ⊢ (∃𝑚 ∈ (𝑇 ∩ 𝑅)((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ 𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅))
140	125, 139	bitri 278	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ 𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅))
141	140	eqriv 2763	. . . . . . . . . . . . 13 ⊢ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) = ((ℕ0 ↑m 𝐽) ∩ 𝑅)
142		f1oeq3 6817	. . . . . . . . . . . . 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 6044	. . . . . . . . . . . . 13 ⊢ ((𝑇 ∩ 𝑅) ⊆ 𝑇 → ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)))
145		f1oeq1 6815	. . . . . . . . . . . . 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 6851	. . . . . . . . . 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 6827	. . . . . . . . . . . . . 14 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅) → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)⟶((ℕ0 ↑m 𝐽) ∩ 𝑅))
152		eqid 2766	. . . . . . . . . . . . . . . 16 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))
153	152	fmpt 7112	. . . . . . . . . . . . . . 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 2767	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)))
158		eqidd 2767	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)))
159		coeq2 5849	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑜 ↾ 𝐽) → (bits ∘ 𝑓) = (bits ∘ (𝑜 ↾ 𝐽)))
160	156, 157, 158, 159	fmptcof 7133	. . . . . . . . . . 11 ⊢ (⊤ → ((𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))))
161	160	eqcomd 2772	. . . . . . . . . 10 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))) = ((𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))))
162		eqidd 2767	. . . . . . . . . 10 ⊢ (⊤ → (𝑇 ∩ 𝑅) = (𝑇 ∩ 𝑅))
163	49	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
164	161, 162, 163	f1oeq123d 6821	. . . . . . . . 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 1577	. . . . . . 7 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻
167		f1oco 6851	. . . . . . 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 2767	. . . . . . . . . . 11 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))))
170		bitsf 16510	. . . . . . . . . . . . . 14 ⊢ bits:ℤ⟶𝒫 ℕ0
171		zex 12618	. . . . . . . . . . . . . 14 ⊢ ℤ ∈ V
172		fex 7231	. . . . . . . . . . . . . 14 ⊢ ((bits:ℤ⟶𝒫 ℕ0 ∧ ℤ ∈ V) → bits ∈ V)
173	170, 171, 172	mp2an 705	. . . . . . . . . . . . 13 ⊢ bits ∈ V
174	173, 122	coex 7936	. . . . . . . . . . . 12 ⊢ (bits ∘ (𝑜 ↾ 𝐽)) ∈ V
175	174	a1i 11	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → (bits ∘ (𝑜 ↾ 𝐽)) ∈ V)
176	169, 175	fvmpt2d 7010	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))‘𝑜) = (bits ∘ (𝑜 ↾ 𝐽)))
177		f1of 6827	. . . . . . . . . . . 12 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻 → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)⟶𝐻)
178	165, 177	syl 18	. . . . . . . . . . 11 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)⟶𝐻)
179	178	ffvelcdmda 7086	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))‘𝑜) ∈ 𝐻)
180	176, 179	eqeltrrd 2867	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → (bits ∘ (𝑜 ↾ 𝐽)) ∈ 𝐻)
181		f1ofn 6828	. . . . . . . . . . . 12 ⊢ (𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) → 𝑀 Fn 𝐻)
182	51, 181	ax-mp 5	. . . . . . . . . . 11 ⊢ 𝑀 Fn 𝐻
183		dffn5 6946	. . . . . . . . . . 11 ⊢ (𝑀 Fn 𝐻 ↔ 𝑀 = (𝑟 ∈ 𝐻 ↦ (𝑀‘𝑟)))
184	182, 183	mpbi 233	. . . . . . . . . 10 ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ (𝑀‘𝑟))
185	184	a1i 11	. . . . . . . . 9 ⊢ (⊤ → 𝑀 = (𝑟 ∈ 𝐻 ↦ (𝑀‘𝑟)))
186		fveq2 6888	. . . . . . . . 9 ⊢ (𝑟 = (bits ∘ (𝑜 ↾ 𝐽)) → (𝑀‘𝑟) = (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))
187	180, 169, 185, 186	fmptco 7132	. . . . . . . 8 ⊢ (⊤ → (𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
188	187	mptru 1577	. . . . . . 7 ⊢ (𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))
189		f1oeq1 6815	. . . . . . 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 6851	. . . . 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 6901	. . . . . . . . 9 ⊢ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))) ∈ V
196		eqid 2766	. . . . . . . . . 10 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))
197	196	fvmpt2 7008	. . . . . . . . 9 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ∧ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))) ∈ V) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))‘𝑜) = (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))
198	194, 195, 197	sylancl 598	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))‘𝑜) = (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))
199		f1of 6827	. . . . . . . . . 10 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)⟶(𝒫 (𝐽 × ℕ0) ∩ Fin))
200	191, 199	mp1i 14	. . . . . . . . 9 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)⟶(𝒫 (𝐽 × ℕ0) ∩ Fin))
201	200	ffvelcdmda 7086	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))‘𝑜) ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin))
202	198, 201	eqeltrrd 2867	. . . . . . 7 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))) ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin))
203		eqidd 2767	. . . . . . 7 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
204		eqidd 2767	. . . . . . 7 ⊢ (⊤ → (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) = (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)))
205		imaeq2 6063	. . . . . . 7 ⊢ (𝑎 = (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))) → (𝐹 “ 𝑎) = (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
206	202, 203, 204, 205	fmptco 7132	. . . . . 6 ⊢ (⊤ → ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
207	206	mptru 1577	. . . . 5 ⊢ ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
208		f1oeq1 6815	. . . . 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 6851	. . 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 8082	. . . . . . . . . 10 ⊢ ((𝐽 ∈ V ∧ ℕ0 ∈ V) → 𝐹 ∈ V)
215	54, 56, 214	mp2an 705	. . . . . . . . 9 ⊢ 𝐹 ∈ V
216		imaexg 7919	. . . . . . . . 9 ⊢ (𝐹 ∈ V → (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) ∈ V)
217	215, 216	ax-mp 5	. . . . . . . 8 ⊢ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) ∈ V
218		eqid 2766	. . . . . . . . 9 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
219	218	fvmpt2 7008	. . . . . . . 8 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ∧ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) ∈ V) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))‘𝑜) = (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
220	194, 217, 219	sylancl 598	. . . . . . 7 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))‘𝑜) = (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
221		f1of 6827	. . . . . . . . 9 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin) → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)⟶(𝒫 ℕ ∩ Fin))
222	210, 221	mp1i 14	. . . . . . . 8 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)⟶(𝒫 ℕ ∩ Fin))
223	222	ffvelcdmda 7086	. . . . . . 7 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))‘𝑜) ∈ (𝒫 ℕ ∩ Fin))
224	220, 223	eqeltrrd 2867	. . . . . 6 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) ∈ (𝒫 ℕ ∩ Fin))
225		eqidd 2767	. . . . . 6 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
226		indf1o 33221	. . . . . . . . . . 11 ⊢ (ℕ ∈ V → (𝟭‘ℕ):𝒫 ℕ–1-1-onto→({0, 1} ↑m ℕ))
227		f1ofn 6828	. . . . . . . . . . 11 ⊢ ((𝟭‘ℕ):𝒫 ℕ–1-1-onto→({0, 1} ↑m ℕ) → (𝟭‘ℕ) Fn 𝒫 ℕ)
228	1, 226, 227	mp2b 10	. . . . . . . . . 10 ⊢ (𝟭‘ℕ) Fn 𝒫 ℕ
229		dffn5 6946	. . . . . . . . . 10 ⊢ ((𝟭‘ℕ) Fn 𝒫 ℕ ↔ (𝟭‘ℕ) = (𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)))
230	228, 229	mpbi 233	. . . . . . . . 9 ⊢ (𝟭‘ℕ) = (𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏))
231	230	reseq1i 5979	. . . . . . . 8 ⊢ ((𝟭‘ℕ) ↾ Fin) = ((𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)) ↾ Fin)
232		resmpt3 6045	. . . . . . . 8 ⊢ ((𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏))
233	231, 232	eqtri 2789	. . . . . . 7 ⊢ ((𝟭‘ℕ) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏))
234	233	a1i 11	. . . . . 6 ⊢ (⊤ → ((𝟭‘ℕ) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏)))
235		fveq2 6888	. . . . . 6 ⊢ (𝑏 = (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) → ((𝟭‘ℕ)‘𝑏) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
236	224, 225, 234, 235	fmptco 7132	. . . . 5 ⊢ (⊤ → (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))))
237	236	mptru 1577	. . . 4 ⊢ (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
238	213, 237	eqtr4i 2792	. . 3 ⊢ 𝐺 = (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
239		f1oeq1 6815	. . 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 1570  ⊤wtru 1571   ∈ wcel 2146  {cab 2744  ∀wral 3082  ∃wrex 3092  {crab 3419  Vcvv 3458   ∖ cdif 3905   ∪ cun 3906   ∩ cin 3907   ⊆ wss 3908  ∅c0 4289  𝒫 cpw 4567  {csn 4594  {cpr 4596   class class class wbr 5114  {copab 5178   ↦ cmpt 5197   × cxp 5664  ^◡ccnv 5665  ran crn 5667   ↾ cres 5668   “ cima 5669   ∘ ccom 5670  Fun wfun 6537   Fn wfn 6538  ⟶wf 6539  –1-1→wf1 6540  –1-1-onto→wf1o 6542  ‘cfv 6543  (class class class)co 7423   ∈ cmpo 7425   supp csupp 8165   ↑_m cmap 8833  Fincfn 8952   finSupp cfsupp 9331  0cc0 11118  1c1 11119   · cmul 11123   ≤ cle 11262  𝟭cind 12236  ℕcn 12251  2c2 12313  ℕ₀cn0 12522  ℤcz 12609  ↑cexp 14117  Σcsu 15763   ∥ cdvds 16335  bitscbits 16502

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-rep 5243  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-inf2 9620  ax-ac2 10465  ax-cnex 11174  ax-resscn 11175  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-addrcl 11179  ax-mulcl 11180  ax-mulrcl 11181  ax-mulcom 11182  ax-addass 11183  ax-mulass 11184  ax-distr 11185  ax-i2m1 11186  ax-1ne0 11187  ax-1rid 11188  ax-rnegex 11189  ax-rrecex 11190  ax-cnre 11191  ax-pre-lttri 11192  ax-pre-lttrn 11193  ax-pre-ltadd 11194  ax-pre-mulgt0 11195  ax-pre-sup 11196

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-nel 3068  df-ral 3083  df-rex 3093  df-rmo 3372  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-int 4918  df-iun 4963  df-disj 5082  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-se 5620  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6309  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7380  df-ov 7426  df-oprab 7427  df-mpo 7428  df-om 7872  df-1st 7995  df-2nd 7996  df-supp 8166  df-frecs 8287  df-wrecs 8318  df-recs 8367  df-rdg 8406  df-1o 8462  df-2o 8463  df-oadd 8466  df-er 8703  df-map 8835  df-pm 8836  df-en 8953  df-dom 8954  df-sdom 8955  df-fin 8956  df-fsupp 9332  df-sup 9412  df-inf 9413  df-oi 9482  df-dju 9906  df-card 9944  df-acn 9947  df-ac 10119  df-pnf 11263  df-mnf 11264  df-xr 11265  df-ltxr 11266  df-le 11267  df-sub 11461  df-neg 11462  df-div 11890  df-ind 12237  df-nn 12252  df-2 12321  df-3 12322  df-n0 12523  df-xnn0 12596  df-z 12610  df-uz 12881  df-rp 13035  df-fz 13554  df-fzo 13702  df-fl 13845  df-mod 13923  df-seq 14058  df-exp 14118  df-hash 14387  df-cj 15176  df-re 15177  df-im 15178  df-sqrt 15312  df-abs 15313  df-clim 15565  df-sum 15764  df-dvds 16336  df-bits 16505

This theorem is used by:  eulerpartlemgf  34800  eulerpartlemgs2  34801  eulerpartlemn  34802