Theorem eulerpartgbij 31630

Description: Lemma for eulerpart 31640: 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 11644	. . . . 5 ⊢ ℕ ∈ V
2		indf1ofs 31285	. . . . 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 4178	. . . . . . 7 ⊢ (({0, 1} ↑m ℕ) ∩ {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}) = ({𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} ∩ ({0, 1} ↑m ℕ))
5		eulerpart.r	. . . . . . . 8 ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}
6	5	ineq2i 4186	. . . . . . 7 ⊢ (({0, 1} ↑m ℕ) ∩ 𝑅) = (({0, 1} ↑m ℕ) ∩ {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin})
7		dfrab2 4279	. . . . . . 7 ⊢ {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (◡𝑓 “ ℕ) ∈ Fin} = ({𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} ∩ ({0, 1} ↑m ℕ))
8	4, 6, 7	3eqtr4i 2854	. . . . . 6 ⊢ (({0, 1} ↑m ℕ) ∩ 𝑅) = {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (◡𝑓 “ ℕ) ∈ Fin}
9		elmapfun 8430	. . . . . . . . 9 ⊢ (𝑓 ∈ ({0, 1} ↑m ℕ) → Fun 𝑓)
10		elmapi 8428	. . . . . . . . . 10 ⊢ (𝑓 ∈ ({0, 1} ↑m ℕ) → 𝑓:ℕ⟶{0, 1})
11	10	frnd 6521	. . . . . . . . 9 ⊢ (𝑓 ∈ ({0, 1} ↑m ℕ) → ran 𝑓 ⊆ {0, 1})
12		fimacnvinrn2 6841	. . . . . . . . . 10 ⊢ ((Fun 𝑓 ∧ ran 𝑓 ⊆ {0, 1}) → (◡𝑓 “ ℕ) = (◡𝑓 “ (ℕ ∩ {0, 1})))
13		df-pr 4570	. . . . . . . . . . . . . 14 ⊢ {0, 1} = ({0} ∪ {1})
14	13	ineq2i 4186	. . . . . . . . . . . . 13 ⊢ (ℕ ∩ {0, 1}) = (ℕ ∩ ({0} ∪ {1}))
15		indi 4250	. . . . . . . . . . . . 13 ⊢ (ℕ ∩ ({0} ∪ {1})) = ((ℕ ∩ {0}) ∪ (ℕ ∩ {1}))
16		0nnn 11674	. . . . . . . . . . . . . . 15 ⊢ ¬ 0 ∈ ℕ
17		disjsn 4647	. . . . . . . . . . . . . . 15 ⊢ ((ℕ ∩ {0}) = ∅ ↔ ¬ 0 ∈ ℕ)
18	16, 17	mpbir 233	. . . . . . . . . . . . . 14 ⊢ (ℕ ∩ {0}) = ∅
19		1nn 11649	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℕ
20		1ex 10637	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ V
21	20	snss 4718	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ ℕ ↔ {1} ⊆ ℕ)
22	19, 21	mpbi 232	. . . . . . . . . . . . . . . 16 ⊢ {1} ⊆ ℕ
23		dfss 3953	. . . . . . . . . . . . . . . 16 ⊢ ({1} ⊆ ℕ ↔ {1} = ({1} ∩ ℕ))
24	22, 23	mpbi 232	. . . . . . . . . . . . . . 15 ⊢ {1} = ({1} ∩ ℕ)
25		incom 4178	. . . . . . . . . . . . . . 15 ⊢ ({1} ∩ ℕ) = (ℕ ∩ {1})
26	24, 25	eqtr2i 2845	. . . . . . . . . . . . . 14 ⊢ (ℕ ∩ {1}) = {1}
27	18, 26	uneq12i 4137	. . . . . . . . . . . . 13 ⊢ ((ℕ ∩ {0}) ∪ (ℕ ∩ {1})) = (∅ ∪ {1})
28	14, 15, 27	3eqtri 2848	. . . . . . . . . . . 12 ⊢ (ℕ ∩ {0, 1}) = (∅ ∪ {1})
29		uncom 4129	. . . . . . . . . . . 12 ⊢ (∅ ∪ {1}) = ({1} ∪ ∅)
30		un0 4344	. . . . . . . . . . . 12 ⊢ ({1} ∪ ∅) = {1}
31	28, 29, 30	3eqtri 2848	. . . . . . . . . . 11 ⊢ (ℕ ∩ {0, 1}) = {1}
32	31	imaeq2i 5927	. . . . . . . . . 10 ⊢ (◡𝑓 “ (ℕ ∩ {0, 1})) = (◡𝑓 “ {1})
33	12, 32	syl6eq 2872	. . . . . . . . 9 ⊢ ((Fun 𝑓 ∧ ran 𝑓 ⊆ {0, 1}) → (◡𝑓 “ ℕ) = (◡𝑓 “ {1}))
34	9, 11, 33	syl2anc 586	. . . . . . . 8 ⊢ (𝑓 ∈ ({0, 1} ↑m ℕ) → (◡𝑓 “ ℕ) = (◡𝑓 “ {1}))
35	34	eleq1d 2897	. . . . . . 7 ⊢ (𝑓 ∈ ({0, 1} ↑m ℕ) → ((◡𝑓 “ ℕ) ∈ Fin ↔ (◡𝑓 “ {1}) ∈ Fin))
36	35	rabbiia 3472	. . . . . 6 ⊢ {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (◡𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (◡𝑓 “ {1}) ∈ Fin}
37	8, 36	eqtr2i 2845	. . . . 5 ⊢ {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (◡𝑓 “ {1}) ∈ Fin} = (({0, 1} ↑m ℕ) ∩ 𝑅)
38		f1oeq3 6606	. . . . 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 232	. . 3 ⊢ ((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅)
41		eulerpart.j	. . . . . . 7 ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
42		eulerpart.f	. . . . . . 7 ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))
43	41, 42	oddpwdc 31612	. . . . . 6 ⊢ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ
44		f1opwfi 8828	. . . . . 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 31625	. . . . . . 7 ⊢ 𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
52		bitsf1o 15794	. . . . . . . . . . . . . 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 5237	. . . . . . . . . . . . . 14 ⊢ 𝐽 ∈ V
55	54	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → 𝐽 ∈ V)
56		nn0ex 11904	. . . . . . . . . . . . . 14 ⊢ ℕ0 ∈ V
57	56	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → ℕ0 ∈ V)
58	56	pwex 5281	. . . . . . . . . . . . . . 15 ⊢ 𝒫 ℕ0 ∈ V
59	58	inex1 5221	. . . . . . . . . . . . . 14 ⊢ (𝒫 ℕ0 ∩ Fin) ∈ V
60	59	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝒫 ℕ0 ∩ Fin) ∈ V)
61		0nn0 11913	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℕ0
62	61	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → 0 ∈ ℕ0)
63		fvres 6689	. . . . . . . . . . . . . . 15 ⊢ (0 ∈ ℕ0 → ((bits ↾ ℕ0)‘0) = (bits‘0))
64	61, 63	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((bits ↾ ℕ0)‘0) = (bits‘0)
65		0bits 15788	. . . . . . . . . . . . . 14 ⊢ (bits‘0) = ∅
66	64, 65	eqtr2i 2845	. . . . . . . . . . . . 13 ⊢ ∅ = ((bits ↾ ℕ0)‘0)
67		elmapi 8428	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ (ℕ0 ↑m 𝐽) → 𝑓:𝐽⟶ℕ0)
68		frnnn0supp 11954	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ V ∧ 𝑓:𝐽⟶ℕ0) → (𝑓 supp 0) = (◡𝑓 “ ℕ))
69	54, 67, 68	sylancr 589	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ (ℕ0 ↑m 𝐽) → (𝑓 supp 0) = (◡𝑓 “ ℕ))
70	69	eleq1d 2897	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ (ℕ0 ↑m 𝐽) → ((𝑓 supp 0) ∈ Fin ↔ (◡𝑓 “ ℕ) ∈ Fin))
71	70	rabbiia 3472	. . . . . . . . . . . . . 14 ⊢ {𝑓 ∈ (ℕ0 ↑m 𝐽) ∣ (𝑓 supp 0) ∈ Fin} = {𝑓 ∈ (ℕ0 ↑m 𝐽) ∣ (◡𝑓 “ ℕ) ∈ Fin}
72		elmapfun 8430	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ (ℕ0 ↑m 𝐽) → Fun 𝑓)
73		vex 3497	. . . . . . . . . . . . . . . . 17 ⊢ 𝑓 ∈ V
74		funisfsupp 8838	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝑓 ∧ 𝑓 ∈ V ∧ 0 ∈ ℕ0) → (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
75	73, 61, 74	mp3an23 1449	. . . . . . . . . . . . . . . 16 ⊢ (Fun 𝑓 → (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
76	72, 75	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ (ℕ0 ↑m 𝐽) → (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
77	76	rabbiia 3472	. . . . . . . . . . . . . 14 ⊢ {𝑓 ∈ (ℕ0 ↑m 𝐽) ∣ 𝑓 finSupp 0} = {𝑓 ∈ (ℕ0 ↑m 𝐽) ∣ (𝑓 supp 0) ∈ Fin}
78		incom 4178	. . . . . . . . . . . . . . 15 ⊢ ({𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} ∩ (ℕ0 ↑m 𝐽)) = ((ℕ0 ↑m 𝐽) ∩ {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin})
79		dfrab2 4279	. . . . . . . . . . . . . . 15 ⊢ {𝑓 ∈ (ℕ0 ↑m 𝐽) ∣ (◡𝑓 “ ℕ) ∈ Fin} = ({𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} ∩ (ℕ0 ↑m 𝐽))
80	5	ineq2i 4186	. . . . . . . . . . . . . . 15 ⊢ ((ℕ0 ↑m 𝐽) ∩ 𝑅) = ((ℕ0 ↑m 𝐽) ∩ {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin})
81	78, 79, 80	3eqtr4ri 2855	. . . . . . . . . . . . . 14 ⊢ ((ℕ0 ↑m 𝐽) ∩ 𝑅) = {𝑓 ∈ (ℕ0 ↑m 𝐽) ∣ (◡𝑓 “ ℕ) ∈ Fin}
82	71, 77, 81	3eqtr4ri 2855	. . . . . . . . . . . . 13 ⊢ ((ℕ0 ↑m 𝐽) ∩ 𝑅) = {𝑓 ∈ (ℕ0 ↑m 𝐽) ∣ 𝑓 finSupp 0}
83		elmapfun 8430	. . . . . . . . . . . . . . 15 ⊢ (𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) → Fun 𝑟)
84		vex 3497	. . . . . . . . . . . . . . . . 17 ⊢ 𝑟 ∈ V
85		0ex 5211	. . . . . . . . . . . . . . . . 17 ⊢ ∅ ∈ V
86		funisfsupp 8838	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝑟 ∧ 𝑟 ∈ V ∧ ∅ ∈ V) → (𝑟 finSupp ∅ ↔ (𝑟 supp ∅) ∈ Fin))
87	84, 85, 86	mp3an23 1449	. . . . . . . . . . . . . . . 16 ⊢ (Fun 𝑟 → (𝑟 finSupp ∅ ↔ (𝑟 supp ∅) ∈ Fin))
88	87	bicomd 225	. . . . . . . . . . . . . . 15 ⊢ (Fun 𝑟 → ((𝑟 supp ∅) ∈ Fin ↔ 𝑟 finSupp ∅))
89	83, 88	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) → ((𝑟 supp ∅) ∈ Fin ↔ 𝑟 finSupp ∅))
90	89	rabbiia 3472	. . . . . . . . . . . . 13 ⊢ {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ 𝑟 finSupp ∅}
91	53, 55, 57, 60, 62, 66, 82, 90	fcobijfs 30459	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)):((ℕ0 ↑m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
92		elinel1 4172	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) → 𝑓 ∈ (ℕ0 ↑m 𝐽))
93		frn 6520	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓:𝐽⟶ℕ0 → ran 𝑓 ⊆ ℕ0)
94		cores 6102	. . . . . . . . . . . . . . . . 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 5157	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)) = (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓))
98	97	eqcomi 2830	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓))
99		f1oeq1 6604	. . . . . . . . . . . . 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 259	. . . . . . . . . . 11 ⊢ (⊤ → (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0 ↑m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
102	101	mptru 1544	. . . . . . . . . 10 ⊢ (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0 ↑m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
103		ssrab2 4056	. . . . . . . . . . . . . . . 16 ⊢ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ⊆ ℕ
104	41, 103	eqsstri 4001	. . . . . . . . . . . . . . 15 ⊢ 𝐽 ⊆ ℕ
105	1, 56, 104	3pm3.2i 1335	. . . . . . . . . . . . . 14 ⊢ (ℕ ∈ V ∧ ℕ0 ∈ V ∧ 𝐽 ⊆ ℕ)
106		eulerpart.t	. . . . . . . . . . . . . . . 16 ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}
107		cnveq 5744	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = 𝑜 → ◡𝑓 = ◡𝑜)
108		dfn2 11911	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ = (ℕ0 ∖ {0})
109	108	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = 𝑜 → ℕ = (ℕ0 ∖ {0}))
110	107, 109	imaeq12d 5930	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = 𝑜 → (◡𝑓 “ ℕ) = (◡𝑜 “ (ℕ0 ∖ {0})))
111	110	sseq1d 3998	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑜 → ((◡𝑓 “ ℕ) ⊆ 𝐽 ↔ (◡𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽))
112	111	cbvrabv 3491	. . . . . . . . . . . . . . . 16 ⊢ {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽} = {𝑜 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽}
113	106, 112	eqtri 2844	. . . . . . . . . . . . . . 15 ⊢ 𝑇 = {𝑜 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽}
114		eqid 2821	. . . . . . . . . . . . . . 15 ⊢ (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) = (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))
115	113, 114	resf1o 30466	. . . . . . . . . . . . . 14 ⊢ (((ℕ ∈ V ∧ ℕ0 ∈ V ∧ 𝐽 ⊆ ℕ) ∧ 0 ∈ ℕ0) → (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1-onto→(ℕ0 ↑m 𝐽))
116	105, 61, 115	mp2an 690	. . . . . . . . . . . . 13 ⊢ (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1-onto→(ℕ0 ↑m 𝐽)
117		f1of1 6614	. . . . . . . . . . . . 13 ⊢ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1-onto→(ℕ0 ↑m 𝐽) → (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1→(ℕ0 ↑m 𝐽))
118	116, 117	ax-mp 5	. . . . . . . . . . . 12 ⊢ (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1→(ℕ0 ↑m 𝐽)
119		inss1 4205	. . . . . . . . . . . 12 ⊢ (𝑇 ∩ 𝑅) ⊆ 𝑇
120		f1ores 6629	. . . . . . . . . . . 12 ⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1→(ℕ0 ↑m 𝐽) ∧ (𝑇 ∩ 𝑅) ⊆ 𝑇) → ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)))
121	118, 119, 120	mp2an 690	. . . . . . . . . . 11 ⊢ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅))
122		vex 3497	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑜 ∈ V
123	122	resex 5899	. . . . . . . . . . . . . . . . 17 ⊢ (𝑜 ↾ 𝐽) ∈ V
124	123, 114	fnmpti 6491	. . . . . . . . . . . . . . . 16 ⊢ (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) Fn 𝑇
125		fvelimab 6737	. . . . . . . . . . . . . . . 16 ⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) Fn 𝑇 ∧ (𝑇 ∩ 𝑅) ⊆ 𝑇) → (𝑓 ∈ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓))
126	124, 119, 125	mp2an 690	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓)
127		eqid 2821	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) = (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽))
128		vex 3497	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑚 ∈ V
129	128	resex 5899	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ↾ 𝐽) ∈ V
130	127, 129	elrnmpti 5832	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑓 = (𝑚 ↾ 𝐽))
131	46, 47, 48, 41, 42, 49, 50, 5, 106	eulerpartlemt 31629	. . . . . . . . . . . . . . . . 17 ⊢ ((ℕ0 ↑m 𝐽) ∩ 𝑅) = ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽))
132	131	eleq2i 2904	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↔ 𝑓 ∈ ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)))
133		elinel1 4172	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) → 𝑚 ∈ 𝑇)
134	114	fvtresfn 6770	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ 𝑇 → ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = (𝑚 ↾ 𝐽))
135	134	eqeq1d 2823	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ 𝑇 → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ (𝑚 ↾ 𝐽) = 𝑓))
136	133, 135	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ (𝑚 ↾ 𝐽) = 𝑓))
137		eqcom 2828	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 ↾ 𝐽) = 𝑓 ↔ 𝑓 = (𝑚 ↾ 𝐽))
138	136, 137	syl6bb 289	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ 𝑓 = (𝑚 ↾ 𝐽)))
139	138	rexbiia 3246	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑚 ∈ (𝑇 ∩ 𝑅)((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑓 = (𝑚 ↾ 𝐽))
140	130, 132, 139	3bitr4ri 306	. . . . . . . . . . . . . . 15 ⊢ (∃𝑚 ∈ (𝑇 ∩ 𝑅)((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ 𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅))
141	126, 140	bitri 277	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ 𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅))
142	141	eqriv 2818	. . . . . . . . . . . . 13 ⊢ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) = ((ℕ0 ↑m 𝐽) ∩ 𝑅)
143		f1oeq3 6606	. . . . . . . . . . . . 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 5905	. . . . . . . . . . . . 13 ⊢ ((𝑇 ∩ 𝑅) ⊆ 𝑇 → ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)))
146		f1oeq1 6604	. . . . . . . . . . . . 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 277	. . . . . . . . . . 11 ⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅))
149	121, 148	mpbi 232	. . . . . . . . . 10 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅)
150		f1oco 6637	. . . . . . . . . 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 690	. . . . . . . . 9 ⊢ ((𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
152		f1of 6615	. . . . . . . . . . . . . 14 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑m 𝐽) ∩ 𝑅) → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)⟶((ℕ0 ↑m 𝐽) ∩ 𝑅))
153		eqid 2821	. . . . . . . . . . . . . . . 16 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))
154	153	fmpt 6874	. . . . . . . . . . . . . . 15 ⊢ (∀𝑜 ∈ (𝑇 ∩ 𝑅)(𝑜 ↾ 𝐽) ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)⟶((ℕ0 ↑m 𝐽) ∩ 𝑅))
155	154	biimpri 230	. . . . . . . . . . . . . 14 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)⟶((ℕ0 ↑m 𝐽) ∩ 𝑅) → ∀𝑜 ∈ (𝑇 ∩ 𝑅)(𝑜 ↾ 𝐽) ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅))
156	149, 152, 155	mp2b 10	. . . . . . . . . . . . 13 ⊢ ∀𝑜 ∈ (𝑇 ∩ 𝑅)(𝑜 ↾ 𝐽) ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅)
157	156	a1i 11	. . . . . . . . . . . 12 ⊢ (⊤ → ∀𝑜 ∈ (𝑇 ∩ 𝑅)(𝑜 ↾ 𝐽) ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅))
158		eqidd 2822	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)))
159		eqidd 2822	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)))
160		coeq2 5729	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑜 ↾ 𝐽) → (bits ∘ 𝑓) = (bits ∘ (𝑜 ↾ 𝐽)))
161	157, 158, 159, 160	fmptcof 6892	. . . . . . . . . . 11 ⊢ (⊤ → ((𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))))
162	161	eqcomd 2827	. . . . . . . . . 10 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))) = ((𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))))
163		eqidd 2822	. . . . . . . . . 10 ⊢ (⊤ → (𝑇 ∩ 𝑅) = (𝑇 ∩ 𝑅))
164	49	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
165	162, 163, 164	f1oeq123d 6610	. . . . . . . . 9 ⊢ (⊤ → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻 ↔ ((𝑓 ∈ ((ℕ0 ↑m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}))
166	151, 165	mpbiri 260	. . . . . . . 8 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻)
167	166	mptru 1544	. . . . . . 7 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻
168		f1oco 6637	. . . . . . 7 ⊢ ((𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) ∧ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻) → (𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin))
169	51, 167, 168	mp2an 690	. . . . . 6 ⊢ (𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
170		eqidd 2822	. . . . . . . . . . 11 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))))
171		bitsf 15776	. . . . . . . . . . . . . 14 ⊢ bits:ℤ⟶𝒫 ℕ0
172		zex 11991	. . . . . . . . . . . . . 14 ⊢ ℤ ∈ V
173		fex 6989	. . . . . . . . . . . . . 14 ⊢ ((bits:ℤ⟶𝒫 ℕ0 ∧ ℤ ∈ V) → bits ∈ V)
174	171, 172, 173	mp2an 690	. . . . . . . . . . . . 13 ⊢ bits ∈ V
175	174, 123	coex 7635	. . . . . . . . . . . 12 ⊢ (bits ∘ (𝑜 ↾ 𝐽)) ∈ V
176	175	a1i 11	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → (bits ∘ (𝑜 ↾ 𝐽)) ∈ V)
177	170, 176	fvmpt2d 6781	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))‘𝑜) = (bits ∘ (𝑜 ↾ 𝐽)))
178		f1of 6615	. . . . . . . . . . . 12 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻 → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)⟶𝐻)
179	166, 178	syl 17	. . . . . . . . . . 11 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)⟶𝐻)
180	179	ffvelrnda 6851	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))‘𝑜) ∈ 𝐻)
181	177, 180	eqeltrrd 2914	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → (bits ∘ (𝑜 ↾ 𝐽)) ∈ 𝐻)
182		f1ofn 6616	. . . . . . . . . . . 12 ⊢ (𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) → 𝑀 Fn 𝐻)
183	51, 182	ax-mp 5	. . . . . . . . . . 11 ⊢ 𝑀 Fn 𝐻
184		dffn5 6724	. . . . . . . . . . 11 ⊢ (𝑀 Fn 𝐻 ↔ 𝑀 = (𝑟 ∈ 𝐻 ↦ (𝑀‘𝑟)))
185	183, 184	mpbi 232	. . . . . . . . . 10 ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ (𝑀‘𝑟))
186	185	a1i 11	. . . . . . . . 9 ⊢ (⊤ → 𝑀 = (𝑟 ∈ 𝐻 ↦ (𝑀‘𝑟)))
187		fveq2 6670	. . . . . . . . 9 ⊢ (𝑟 = (bits ∘ (𝑜 ↾ 𝐽)) → (𝑀‘𝑟) = (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))
188	181, 170, 186, 187	fmptco 6891	. . . . . . . 8 ⊢ (⊤ → (𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
189	188	mptru 1544	. . . . . . 7 ⊢ (𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))
190		f1oeq1 6604	. . . . . . 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 232	. . . . 5 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
193		f1oco 6637	. . . . 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 690	. . . 4 ⊢ ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)
195		simpr 487	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → 𝑜 ∈ (𝑇 ∩ 𝑅))
196		fvex 6683	. . . . . . . . 9 ⊢ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))) ∈ V
197		eqid 2821	. . . . . . . . . 10 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))
198	197	fvmpt2 6779	. . . . . . . . 9 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ∧ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))) ∈ V) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))‘𝑜) = (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))
199	195, 196, 198	sylancl 588	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))‘𝑜) = (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))
200		f1of 6615	. . . . . . . . . 10 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)⟶(𝒫 (𝐽 × ℕ0) ∩ Fin))
201	192, 200	mp1i 13	. . . . . . . . 9 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)⟶(𝒫 (𝐽 × ℕ0) ∩ Fin))
202	201	ffvelrnda 6851	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))‘𝑜) ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin))
203	199, 202	eqeltrrd 2914	. . . . . . 7 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))) ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin))
204		eqidd 2822	. . . . . . 7 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
205		eqidd 2822	. . . . . . 7 ⊢ (⊤ → (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) = (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)))
206		imaeq2 5925	. . . . . . 7 ⊢ (𝑎 = (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))) → (𝐹 “ 𝑎) = (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
207	203, 204, 205, 206	fmptco 6891	. . . . . 6 ⊢ (⊤ → ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
208	207	mptru 1544	. . . . 5 ⊢ ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
209		f1oeq1 6604	. . . . 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 232	. . 3 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)
212		f1oco 6637	. . 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 690	. 2 ⊢ (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))):(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅)
214		eulerpart.g	. . . 4 ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
215	42	mpoexg 7774	. . . . . . . . . 10 ⊢ ((𝐽 ∈ V ∧ ℕ0 ∈ V) → 𝐹 ∈ V)
216	54, 56, 215	mp2an 690	. . . . . . . . 9 ⊢ 𝐹 ∈ V
217		imaexg 7620	. . . . . . . . 9 ⊢ (𝐹 ∈ V → (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) ∈ V)
218	216, 217	ax-mp 5	. . . . . . . 8 ⊢ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) ∈ V
219		eqid 2821	. . . . . . . . 9 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
220	219	fvmpt2 6779	. . . . . . . 8 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ∧ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) ∈ V) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))‘𝑜) = (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
221	195, 218, 220	sylancl 588	. . . . . . 7 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))‘𝑜) = (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
222		f1of 6615	. . . . . . . . 9 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin) → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)⟶(𝒫 ℕ ∩ Fin))
223	211, 222	mp1i 13	. . . . . . . 8 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)⟶(𝒫 ℕ ∩ Fin))
224	223	ffvelrnda 6851	. . . . . . 7 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))‘𝑜) ∈ (𝒫 ℕ ∩ Fin))
225	221, 224	eqeltrrd 2914	. . . . . 6 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) ∈ (𝒫 ℕ ∩ Fin))
226		eqidd 2822	. . . . . 6 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
227		indf1o 31283	. . . . . . . . . . 11 ⊢ (ℕ ∈ V → (𝟭‘ℕ):𝒫 ℕ–1-1-onto→({0, 1} ↑m ℕ))
228		f1ofn 6616	. . . . . . . . . . 11 ⊢ ((𝟭‘ℕ):𝒫 ℕ–1-1-onto→({0, 1} ↑m ℕ) → (𝟭‘ℕ) Fn 𝒫 ℕ)
229	1, 227, 228	mp2b 10	. . . . . . . . . 10 ⊢ (𝟭‘ℕ) Fn 𝒫 ℕ
230		dffn5 6724	. . . . . . . . . 10 ⊢ ((𝟭‘ℕ) Fn 𝒫 ℕ ↔ (𝟭‘ℕ) = (𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)))
231	229, 230	mpbi 232	. . . . . . . . 9 ⊢ (𝟭‘ℕ) = (𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏))
232	231	reseq1i 5849	. . . . . . . 8 ⊢ ((𝟭‘ℕ) ↾ Fin) = ((𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)) ↾ Fin)
233		resmpt3 5906	. . . . . . . 8 ⊢ ((𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏))
234	232, 233	eqtri 2844	. . . . . . 7 ⊢ ((𝟭‘ℕ) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏))
235	234	a1i 11	. . . . . 6 ⊢ (⊤ → ((𝟭‘ℕ) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏)))
236		fveq2 6670	. . . . . 6 ⊢ (𝑏 = (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) → ((𝟭‘ℕ)‘𝑏) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
237	225, 226, 235, 236	fmptco 6891	. . . . 5 ⊢ (⊤ → (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))))
238	237	mptru 1544	. . . 4 ⊢ (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
239	214, 238	eqtr4i 2847	. . 3 ⊢ 𝐺 = (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
240		f1oeq1 6604	. . 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 233	1 ⊢ 𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅)

Syntax hints:  ¬ wn 3   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1537  ⊤wtru 1538   ∈ wcel 2114  {cab 2799  ∀wral 3138  ∃wrex 3139  {crab 3142  Vcvv 3494   ∖ cdif 3933   ∪ cun 3934   ∩ cin 3935   ⊆ wss 3936  ∅c0 4291  𝒫 cpw 4539  {csn 4567  {cpr 4569   class class class wbr 5066  {copab 5128   ↦ cmpt 5146   × cxp 5553  ^◡ccnv 5554  ran crn 5556   ↾ cres 5557   “ cima 5558   ∘ ccom 5559  Fun wfun 6349   Fn wfn 6350  ⟶wf 6351  –1-1→wf1 6352  –1-1-onto→wf1o 6354  ‘cfv 6355  (class class class)co 7156   ∈ cmpo 7158   supp csupp 7830   ↑_m cmap 8406  Fincfn 8509   finSupp cfsupp 8833  0cc0 10537  1c1 10538   · cmul 10542   ≤ cle 10676  ℕcn 11638  2c2 11693  ℕ₀cn0 11898  ℤcz 11982  ↑cexp 13430  Σcsu 15042   ∥ cdvds 15607  bitscbits 15768  𝟭cind 31269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5190  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-inf2 9104  ax-ac2 9885  ax-cnex 10593  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614  ax-pre-sup 10615

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-int 4877  df-iun 4921  df-disj 5032  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-se 5515  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-isom 6364  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7581  df-1st 7689  df-2nd 7690  df-supp 7831  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-1o 8102  df-2o 8103  df-oadd 8106  df-er 8289  df-map 8408  df-pm 8409  df-en 8510  df-dom 8511  df-sdom 8512  df-fin 8513  df-fsupp 8834  df-sup 8906  df-inf 8907  df-oi 8974  df-dju 9330  df-card 9368  df-acn 9371  df-ac 9542  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-div 11298  df-nn 11639  df-2 11701  df-3 11702  df-n0 11899  df-xnn0 11969  df-z 11983  df-uz 12245  df-rp 12391  df-fz 12894  df-fzo 13035  df-fl 13163  df-mod 13239  df-seq 13371  df-exp 13431  df-hash 13692  df-cj 14458  df-re 14459  df-im 14460  df-sqrt 14594  df-abs 14595  df-clim 14845  df-sum 15043  df-dvds 15608  df-bits 15771  df-ind 31270

This theorem is referenced by:  eulerpartlemgf  31637  eulerpartlemgs2  31638  eulerpartlemn  31639