Theorem eulerpartgbij 30434

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

Assertion

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

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 11026	. . . . 5 ⊢ ℕ ∈ V
2		indf1ofs 30088	. . . . 5 ⊢ (ℕ ∈ V → ((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑𝑚 ℕ) ∣ (◡𝑓 “ {1}) ∈ Fin})
3	1, 2	ax-mp 5	. . . 4 ⊢ ((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑𝑚 ℕ) ∣ (◡𝑓 “ {1}) ∈ Fin}
4		incom 3805	. . . . . . 7 ⊢ (({0, 1} ↑𝑚 ℕ) ∩ {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}) = ({𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} ∩ ({0, 1} ↑𝑚 ℕ))
5		eulerpart.r	. . . . . . . 8 ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}
6	5	ineq2i 3811	. . . . . . 7 ⊢ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) = (({0, 1} ↑𝑚 ℕ) ∩ {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin})
7		dfrab2 3903	. . . . . . 7 ⊢ {𝑓 ∈ ({0, 1} ↑𝑚 ℕ) ∣ (◡𝑓 “ ℕ) ∈ Fin} = ({𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} ∩ ({0, 1} ↑𝑚 ℕ))
8	4, 6, 7	3eqtr4i 2654	. . . . . 6 ⊢ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) = {𝑓 ∈ ({0, 1} ↑𝑚 ℕ) ∣ (◡𝑓 “ ℕ) ∈ Fin}
9		elmapfun 7881	. . . . . . . . 9 ⊢ (𝑓 ∈ ({0, 1} ↑𝑚 ℕ) → Fun 𝑓)
10		elmapi 7879	. . . . . . . . . 10 ⊢ (𝑓 ∈ ({0, 1} ↑𝑚 ℕ) → 𝑓:ℕ⟶{0, 1})
11		frn 6053	. . . . . . . . . 10 ⊢ (𝑓:ℕ⟶{0, 1} → ran 𝑓 ⊆ {0, 1})
12	10, 11	syl 17	. . . . . . . . 9 ⊢ (𝑓 ∈ ({0, 1} ↑𝑚 ℕ) → ran 𝑓 ⊆ {0, 1})
13		fimacnvinrn2 6349	. . . . . . . . . 10 ⊢ ((Fun 𝑓 ∧ ran 𝑓 ⊆ {0, 1}) → (◡𝑓 “ ℕ) = (◡𝑓 “ (ℕ ∩ {0, 1})))
14		df-pr 4180	. . . . . . . . . . . . . 14 ⊢ {0, 1} = ({0} ∪ {1})
15	14	ineq2i 3811	. . . . . . . . . . . . 13 ⊢ (ℕ ∩ {0, 1}) = (ℕ ∩ ({0} ∪ {1}))
16		indi 3873	. . . . . . . . . . . . 13 ⊢ (ℕ ∩ ({0} ∪ {1})) = ((ℕ ∩ {0}) ∪ (ℕ ∩ {1}))
17		0nnn 11052	. . . . . . . . . . . . . . 15 ⊢ ¬ 0 ∈ ℕ
18		disjsn 4246	. . . . . . . . . . . . . . 15 ⊢ ((ℕ ∩ {0}) = ∅ ↔ ¬ 0 ∈ ℕ)
19	17, 18	mpbir 221	. . . . . . . . . . . . . 14 ⊢ (ℕ ∩ {0}) = ∅
20		1nn 11031	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℕ
21		1ex 10035	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ V
22	21	snss 4316	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ ℕ ↔ {1} ⊆ ℕ)
23	20, 22	mpbi 220	. . . . . . . . . . . . . . . 16 ⊢ {1} ⊆ ℕ
24		dfss 3589	. . . . . . . . . . . . . . . 16 ⊢ ({1} ⊆ ℕ ↔ {1} = ({1} ∩ ℕ))
25	23, 24	mpbi 220	. . . . . . . . . . . . . . 15 ⊢ {1} = ({1} ∩ ℕ)
26		incom 3805	. . . . . . . . . . . . . . 15 ⊢ ({1} ∩ ℕ) = (ℕ ∩ {1})
27	25, 26	eqtr2i 2645	. . . . . . . . . . . . . 14 ⊢ (ℕ ∩ {1}) = {1}
28	19, 27	uneq12i 3765	. . . . . . . . . . . . 13 ⊢ ((ℕ ∩ {0}) ∪ (ℕ ∩ {1})) = (∅ ∪ {1})
29	15, 16, 28	3eqtri 2648	. . . . . . . . . . . 12 ⊢ (ℕ ∩ {0, 1}) = (∅ ∪ {1})
30		uncom 3757	. . . . . . . . . . . 12 ⊢ (∅ ∪ {1}) = ({1} ∪ ∅)
31		un0 3967	. . . . . . . . . . . 12 ⊢ ({1} ∪ ∅) = {1}
32	29, 30, 31	3eqtri 2648	. . . . . . . . . . 11 ⊢ (ℕ ∩ {0, 1}) = {1}
33	32	imaeq2i 5464	. . . . . . . . . 10 ⊢ (◡𝑓 “ (ℕ ∩ {0, 1})) = (◡𝑓 “ {1})
34	13, 33	syl6eq 2672	. . . . . . . . 9 ⊢ ((Fun 𝑓 ∧ ran 𝑓 ⊆ {0, 1}) → (◡𝑓 “ ℕ) = (◡𝑓 “ {1}))
35	9, 12, 34	syl2anc 693	. . . . . . . 8 ⊢ (𝑓 ∈ ({0, 1} ↑𝑚 ℕ) → (◡𝑓 “ ℕ) = (◡𝑓 “ {1}))
36	35	eleq1d 2686	. . . . . . 7 ⊢ (𝑓 ∈ ({0, 1} ↑𝑚 ℕ) → ((◡𝑓 “ ℕ) ∈ Fin ↔ (◡𝑓 “ {1}) ∈ Fin))
37	36	rabbiia 3185	. . . . . 6 ⊢ {𝑓 ∈ ({0, 1} ↑𝑚 ℕ) ∣ (◡𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ ({0, 1} ↑𝑚 ℕ) ∣ (◡𝑓 “ {1}) ∈ Fin}
38	8, 37	eqtr2i 2645	. . . . 5 ⊢ {𝑓 ∈ ({0, 1} ↑𝑚 ℕ) ∣ (◡𝑓 “ {1}) ∈ Fin} = (({0, 1} ↑𝑚 ℕ) ∩ 𝑅)
39		f1oeq3 6129	. . . . 5 ⊢ ({𝑓 ∈ ({0, 1} ↑𝑚 ℕ) ∣ (◡𝑓 “ {1}) ∈ Fin} = (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) → (((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑𝑚 ℕ) ∣ (◡𝑓 “ {1}) ∈ Fin} ↔ ((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅)))
40	38, 39	ax-mp 5	. . . 4 ⊢ (((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑𝑚 ℕ) ∣ (◡𝑓 “ {1}) ∈ Fin} ↔ ((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅))
41	3, 40	mpbi 220	. . 3 ⊢ ((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅)
42		eulerpart.j	. . . . . . 7 ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
43		eulerpart.f	. . . . . . 7 ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))
44	42, 43	oddpwdc 30416	. . . . . 6 ⊢ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ
45		f1opwfi 8270	. . . . . 6 ⊢ (𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ → (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)):(𝒫 (𝐽 × ℕ0) ∩ Fin)–1-1-onto→(𝒫 ℕ ∩ Fin))
46	44, 45	ax-mp 5	. . . . 5 ⊢ (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)):(𝒫 (𝐽 × ℕ0) ∩ Fin)–1-1-onto→(𝒫 ℕ ∩ Fin)
47		eulerpart.p	. . . . . . . 8 ⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑𝑚 ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}
48		eulerpart.o	. . . . . . . 8 ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}
49		eulerpart.d	. . . . . . . 8 ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}
50		eulerpart.h	. . . . . . . 8 ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
51		eulerpart.m	. . . . . . . 8 ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})
52	47, 48, 49, 42, 43, 50, 51	eulerpartlem1 30429	. . . . . . 7 ⊢ 𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
53		bitsf1o 15167	. . . . . . . . . . . . . 14 ⊢ (bits ↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
54	53	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (bits ↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin))
55	42, 1	rabex2 4815	. . . . . . . . . . . . . 14 ⊢ 𝐽 ∈ V
56	55	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → 𝐽 ∈ V)
57		nn0ex 11298	. . . . . . . . . . . . . 14 ⊢ ℕ0 ∈ V
58	57	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → ℕ0 ∈ V)
59	57	pwex 4848	. . . . . . . . . . . . . . 15 ⊢ 𝒫 ℕ0 ∈ V
60	59	inex1 4799	. . . . . . . . . . . . . 14 ⊢ (𝒫 ℕ0 ∩ Fin) ∈ V
61	60	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝒫 ℕ0 ∩ Fin) ∈ V)
62		0nn0 11307	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℕ0
63	62	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → 0 ∈ ℕ0)
64		fvres 6207	. . . . . . . . . . . . . . 15 ⊢ (0 ∈ ℕ0 → ((bits ↾ ℕ0)‘0) = (bits‘0))
65	62, 64	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((bits ↾ ℕ0)‘0) = (bits‘0)
66		0bits 15161	. . . . . . . . . . . . . 14 ⊢ (bits‘0) = ∅
67	65, 66	eqtr2i 2645	. . . . . . . . . . . . 13 ⊢ ∅ = ((bits ↾ ℕ0)‘0)
68		elmapi 7879	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ (ℕ0 ↑𝑚 𝐽) → 𝑓:𝐽⟶ℕ0)
69		frnnn0supp 11349	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ V ∧ 𝑓:𝐽⟶ℕ0) → (𝑓 supp 0) = (◡𝑓 “ ℕ))
70	55, 68, 69	sylancr 695	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ (ℕ0 ↑𝑚 𝐽) → (𝑓 supp 0) = (◡𝑓 “ ℕ))
71	70	eleq1d 2686	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ (ℕ0 ↑𝑚 𝐽) → ((𝑓 supp 0) ∈ Fin ↔ (◡𝑓 “ ℕ) ∈ Fin))
72	71	rabbiia 3185	. . . . . . . . . . . . . 14 ⊢ {𝑓 ∈ (ℕ0 ↑𝑚 𝐽) ∣ (𝑓 supp 0) ∈ Fin} = {𝑓 ∈ (ℕ0 ↑𝑚 𝐽) ∣ (◡𝑓 “ ℕ) ∈ Fin}
73		elmapfun 7881	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ (ℕ0 ↑𝑚 𝐽) → Fun 𝑓)
74		vex 3203	. . . . . . . . . . . . . . . . 17 ⊢ 𝑓 ∈ V
75		funisfsupp 8280	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝑓 ∧ 𝑓 ∈ V ∧ 0 ∈ ℕ0) → (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
76	74, 62, 75	mp3an23 1416	. . . . . . . . . . . . . . . 16 ⊢ (Fun 𝑓 → (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
77	73, 76	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ (ℕ0 ↑𝑚 𝐽) → (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
78	77	rabbiia 3185	. . . . . . . . . . . . . 14 ⊢ {𝑓 ∈ (ℕ0 ↑𝑚 𝐽) ∣ 𝑓 finSupp 0} = {𝑓 ∈ (ℕ0 ↑𝑚 𝐽) ∣ (𝑓 supp 0) ∈ Fin}
79		incom 3805	. . . . . . . . . . . . . . 15 ⊢ ({𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} ∩ (ℕ0 ↑𝑚 𝐽)) = ((ℕ0 ↑𝑚 𝐽) ∩ {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin})
80		dfrab2 3903	. . . . . . . . . . . . . . 15 ⊢ {𝑓 ∈ (ℕ0 ↑𝑚 𝐽) ∣ (◡𝑓 “ ℕ) ∈ Fin} = ({𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin} ∩ (ℕ0 ↑𝑚 𝐽))
81	5	ineq2i 3811	. . . . . . . . . . . . . . 15 ⊢ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) = ((ℕ0 ↑𝑚 𝐽) ∩ {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin})
82	79, 80, 81	3eqtr4ri 2655	. . . . . . . . . . . . . 14 ⊢ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) = {𝑓 ∈ (ℕ0 ↑𝑚 𝐽) ∣ (◡𝑓 “ ℕ) ∈ Fin}
83	72, 78, 82	3eqtr4ri 2655	. . . . . . . . . . . . 13 ⊢ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) = {𝑓 ∈ (ℕ0 ↑𝑚 𝐽) ∣ 𝑓 finSupp 0}
84		elmapfun 7881	. . . . . . . . . . . . . . 15 ⊢ (𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) → Fun 𝑟)
85		vex 3203	. . . . . . . . . . . . . . . . 17 ⊢ 𝑟 ∈ V
86		0ex 4790	. . . . . . . . . . . . . . . . 17 ⊢ ∅ ∈ V
87		funisfsupp 8280	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝑟 ∧ 𝑟 ∈ V ∧ ∅ ∈ V) → (𝑟 finSupp ∅ ↔ (𝑟 supp ∅) ∈ Fin))
88	85, 86, 87	mp3an23 1416	. . . . . . . . . . . . . . . 16 ⊢ (Fun 𝑟 → (𝑟 finSupp ∅ ↔ (𝑟 supp ∅) ∈ Fin))
89	88	bicomd 213	. . . . . . . . . . . . . . 15 ⊢ (Fun 𝑟 → ((𝑟 supp ∅) ∈ Fin ↔ 𝑟 finSupp ∅))
90	84, 89	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) → ((𝑟 supp ∅) ∈ Fin ↔ 𝑟 finSupp ∅))
91	90	rabbiia 3185	. . . . . . . . . . . . 13 ⊢ {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ 𝑟 finSupp ∅}
92	54, 56, 58, 61, 63, 67, 83, 91	fcobijfs 29501	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑓 ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)):((ℕ0 ↑𝑚 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
93		elinel1 3799	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) → 𝑓 ∈ (ℕ0 ↑𝑚 𝐽))
94		frn 6053	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓:𝐽⟶ℕ0 → ran 𝑓 ⊆ ℕ0)
95		cores 5638	. . . . . . . . . . . . . . . . 17 ⊢ (ran 𝑓 ⊆ ℕ0 → ((bits ↾ ℕ0) ∘ 𝑓) = (bits ∘ 𝑓))
96	68, 94, 95	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ (ℕ0 ↑𝑚 𝐽) → ((bits ↾ ℕ0) ∘ 𝑓) = (bits ∘ 𝑓))
97	93, 96	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) → ((bits ↾ ℕ0) ∘ 𝑓) = (bits ∘ 𝑓))
98	97	mpteq2ia 4740	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)) = (𝑓 ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓))
99	98	eqcomi 2631	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓))
100		f1oeq1 6127	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)) → ((𝑓 ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0 ↑𝑚 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} ↔ (𝑓 ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)):((ℕ0 ↑𝑚 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}))
101	99, 100	mp1i 13	. . . . . . . . . . . 12 ⊢ (⊤ → ((𝑓 ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0 ↑𝑚 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} ↔ (𝑓 ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)):((ℕ0 ↑𝑚 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}))
102	92, 101	mpbird 247	. . . . . . . . . . 11 ⊢ (⊤ → (𝑓 ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0 ↑𝑚 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
103	102	trud 1493	. . . . . . . . . 10 ⊢ (𝑓 ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0 ↑𝑚 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
104		ssrab2 3687	. . . . . . . . . . . . . . . 16 ⊢ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ⊆ ℕ
105	42, 104	eqsstri 3635	. . . . . . . . . . . . . . 15 ⊢ 𝐽 ⊆ ℕ
106	1, 57, 105	3pm3.2i 1239	. . . . . . . . . . . . . 14 ⊢ (ℕ ∈ V ∧ ℕ0 ∈ V ∧ 𝐽 ⊆ ℕ)
107		eulerpart.t	. . . . . . . . . . . . . . . 16 ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑𝑚 ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}
108		cnveq 5296	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = 𝑜 → ◡𝑓 = ◡𝑜)
109		dfn2 11305	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ = (ℕ0 ∖ {0})
110	109	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = 𝑜 → ℕ = (ℕ0 ∖ {0}))
111	108, 110	imaeq12d 5467	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = 𝑜 → (◡𝑓 “ ℕ) = (◡𝑜 “ (ℕ0 ∖ {0})))
112	111	sseq1d 3632	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑜 → ((◡𝑓 “ ℕ) ⊆ 𝐽 ↔ (◡𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽))
113	112	cbvrabv 3199	. . . . . . . . . . . . . . . 16 ⊢ {𝑓 ∈ (ℕ0 ↑𝑚 ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽} = {𝑜 ∈ (ℕ0 ↑𝑚 ℕ) ∣ (◡𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽}
114	107, 113	eqtri 2644	. . . . . . . . . . . . . . 15 ⊢ 𝑇 = {𝑜 ∈ (ℕ0 ↑𝑚 ℕ) ∣ (◡𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽}
115		eqid 2622	. . . . . . . . . . . . . . 15 ⊢ (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) = (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))
116	114, 115	resf1o 29505	. . . . . . . . . . . . . 14 ⊢ (((ℕ ∈ V ∧ ℕ0 ∈ V ∧ 𝐽 ⊆ ℕ) ∧ 0 ∈ ℕ0) → (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1-onto→(ℕ0 ↑𝑚 𝐽))
117	106, 62, 116	mp2an 708	. . . . . . . . . . . . 13 ⊢ (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1-onto→(ℕ0 ↑𝑚 𝐽)
118		f1of1 6136	. . . . . . . . . . . . 13 ⊢ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1-onto→(ℕ0 ↑𝑚 𝐽) → (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1→(ℕ0 ↑𝑚 𝐽))
119	117, 118	ax-mp 5	. . . . . . . . . . . 12 ⊢ (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1→(ℕ0 ↑𝑚 𝐽)
120		inss1 3833	. . . . . . . . . . . 12 ⊢ (𝑇 ∩ 𝑅) ⊆ 𝑇
121		f1ores 6151	. . . . . . . . . . . 12 ⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)):𝑇–1-1→(ℕ0 ↑𝑚 𝐽) ∧ (𝑇 ∩ 𝑅) ⊆ 𝑇) → ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)))
122	119, 120, 121	mp2an 708	. . . . . . . . . . 11 ⊢ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅))
123		vex 3203	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑜 ∈ V
124	123	resex 5443	. . . . . . . . . . . . . . . . 17 ⊢ (𝑜 ↾ 𝐽) ∈ V
125	124, 115	fnmpti 6022	. . . . . . . . . . . . . . . 16 ⊢ (𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) Fn 𝑇
126		fvelimab 6253	. . . . . . . . . . . . . . . 16 ⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) Fn 𝑇 ∧ (𝑇 ∩ 𝑅) ⊆ 𝑇) → (𝑓 ∈ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓))
127	125, 120, 126	mp2an 708	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓)
128		eqid 2622	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) = (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽))
129		vex 3203	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑚 ∈ V
130	129	resex 5443	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ↾ 𝐽) ∈ V
131	128, 130	elrnmpti 5376	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑓 = (𝑚 ↾ 𝐽))
132	47, 48, 49, 42, 43, 50, 51, 5, 107	eulerpartlemt 30433	. . . . . . . . . . . . . . . . 17 ⊢ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) = ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽))
133	132	eleq2i 2693	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↔ 𝑓 ∈ ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)))
134		elinel1 3799	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) → 𝑚 ∈ 𝑇)
135	115	fvtresfn 6284	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ 𝑇 → ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = (𝑚 ↾ 𝐽))
136	135	eqeq1d 2624	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ 𝑇 → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ (𝑚 ↾ 𝐽) = 𝑓))
137	134, 136	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ (𝑚 ↾ 𝐽) = 𝑓))
138		eqcom 2629	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 ↾ 𝐽) = 𝑓 ↔ 𝑓 = (𝑚 ↾ 𝐽))
139	137, 138	syl6bb 276	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ 𝑓 = (𝑚 ↾ 𝐽)))
140	139	rexbiia 3040	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑚 ∈ (𝑇 ∩ 𝑅)((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑓 = (𝑚 ↾ 𝐽))
141	131, 133, 140	3bitr4ri 293	. . . . . . . . . . . . . . 15 ⊢ (∃𝑚 ∈ (𝑇 ∩ 𝑅)((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽))‘𝑚) = 𝑓 ↔ 𝑓 ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅))
142	127, 141	bitri 264	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ 𝑓 ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅))
143	142	eqriv 2619	. . . . . . . . . . . . 13 ⊢ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) = ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅)
144		f1oeq3 6129	. . . . . . . . . . . . 13 ⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) = ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑𝑚 𝐽) ∩ 𝑅)))
145	143, 144	ax-mp 5	. . . . . . . . . . . 12 ⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑𝑚 𝐽) ∩ 𝑅))
146		resmpt 5449	. . . . . . . . . . . . 13 ⊢ ((𝑇 ∩ 𝑅) ⊆ 𝑇 → ((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)))
147		f1oeq1 6127	. . . . . . . . . . . . 13 ⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)) → (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑𝑚 𝐽) ∩ 𝑅)))
148	120, 146, 147	mp2b 10	. . . . . . . . . . . 12 ⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑𝑚 𝐽) ∩ 𝑅))
149	145, 148	bitri 264	. . . . . . . . . . 11 ⊢ (((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) ↾ (𝑇 ∩ 𝑅)):(𝑇 ∩ 𝑅)–1-1-onto→((𝑜 ∈ 𝑇 ↦ (𝑜 ↾ 𝐽)) “ (𝑇 ∩ 𝑅)) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑𝑚 𝐽) ∩ 𝑅))
150	122, 149	mpbi 220	. . . . . . . . . 10 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑𝑚 𝐽) ∩ 𝑅)
151		f1oco 6159	. . . . . . . . . 10 ⊢ (((𝑓 ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0 ↑𝑚 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} ∧ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑𝑚 𝐽) ∩ 𝑅)) → ((𝑓 ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
152	103, 150, 151	mp2an 708	. . . . . . . . 9 ⊢ ((𝑓 ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
153		f1of 6137	. . . . . . . . . . . . . 14 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)–1-1-onto→((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)⟶((ℕ0 ↑𝑚 𝐽) ∩ 𝑅))
154		eqid 2622	. . . . . . . . . . . . . . . 16 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))
155	154	fmpt 6381	. . . . . . . . . . . . . . 15 ⊢ (∀𝑜 ∈ (𝑇 ∩ 𝑅)(𝑜 ↾ 𝐽) ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)⟶((ℕ0 ↑𝑚 𝐽) ∩ 𝑅))
156	155	biimpri 218	. . . . . . . . . . . . . 14 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)):(𝑇 ∩ 𝑅)⟶((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) → ∀𝑜 ∈ (𝑇 ∩ 𝑅)(𝑜 ↾ 𝐽) ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅))
157	150, 153, 156	mp2b 10	. . . . . . . . . . . . 13 ⊢ ∀𝑜 ∈ (𝑇 ∩ 𝑅)(𝑜 ↾ 𝐽) ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅)
158	157	a1i 11	. . . . . . . . . . . 12 ⊢ (⊤ → ∀𝑜 ∈ (𝑇 ∩ 𝑅)(𝑜 ↾ 𝐽) ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅))
159		eqidd 2623	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽)))
160		eqidd 2623	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑓 ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)))
161		coeq2 5280	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑜 ↾ 𝐽) → (bits ∘ 𝑓) = (bits ∘ (𝑜 ↾ 𝐽)))
162	158, 159, 160, 161	fmptcof 6397	. . . . . . . . . . 11 ⊢ (⊤ → ((𝑓 ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))))
163	162	eqcomd 2628	. . . . . . . . . 10 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))) = ((𝑓 ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))))
164		eqidd 2623	. . . . . . . . . 10 ⊢ (⊤ → (𝑇 ∩ 𝑅) = (𝑇 ∩ 𝑅))
165	50	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
166	163, 164, 165	f1oeq123d 6133	. . . . . . . . 9 ⊢ (⊤ → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻 ↔ ((𝑓 ∈ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}))
167	152, 166	mpbiri 248	. . . . . . . 8 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻)
168	167	trud 1493	. . . . . . 7 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻
169		f1oco 6159	. . . . . . 7 ⊢ ((𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) ∧ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻) → (𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin))
170	52, 168, 169	mp2an 708	. . . . . 6 ⊢ (𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
171		eqidd 2623	. . . . . . . . . . 11 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))))
172		bitsf 15149	. . . . . . . . . . . . . 14 ⊢ bits:ℤ⟶𝒫 ℕ0
173		zex 11386	. . . . . . . . . . . . . 14 ⊢ ℤ ∈ V
174		fex 6490	. . . . . . . . . . . . . 14 ⊢ ((bits:ℤ⟶𝒫 ℕ0 ∧ ℤ ∈ V) → bits ∈ V)
175	172, 173, 174	mp2an 708	. . . . . . . . . . . . 13 ⊢ bits ∈ V
176	175, 124	coex 7118	. . . . . . . . . . . 12 ⊢ (bits ∘ (𝑜 ↾ 𝐽)) ∈ V
177	176	a1i 11	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → (bits ∘ (𝑜 ↾ 𝐽)) ∈ V)
178	171, 177	fvmpt2d 6293	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))‘𝑜) = (bits ∘ (𝑜 ↾ 𝐽)))
179		f1of 6137	. . . . . . . . . . . 12 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)–1-1-onto→𝐻 → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)⟶𝐻)
180	167, 179	syl 17	. . . . . . . . . . 11 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽))):(𝑇 ∩ 𝑅)⟶𝐻)
181	180	ffvelrnda 6359	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))‘𝑜) ∈ 𝐻)
182	178, 181	eqeltrrd 2702	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → (bits ∘ (𝑜 ↾ 𝐽)) ∈ 𝐻)
183		f1ofn 6138	. . . . . . . . . . . 12 ⊢ (𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) → 𝑀 Fn 𝐻)
184	52, 183	ax-mp 5	. . . . . . . . . . 11 ⊢ 𝑀 Fn 𝐻
185		dffn5 6241	. . . . . . . . . . 11 ⊢ (𝑀 Fn 𝐻 ↔ 𝑀 = (𝑟 ∈ 𝐻 ↦ (𝑀‘𝑟)))
186	184, 185	mpbi 220	. . . . . . . . . 10 ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ (𝑀‘𝑟))
187	186	a1i 11	. . . . . . . . 9 ⊢ (⊤ → 𝑀 = (𝑟 ∈ 𝐻 ↦ (𝑀‘𝑟)))
188		fveq2 6191	. . . . . . . . 9 ⊢ (𝑟 = (bits ∘ (𝑜 ↾ 𝐽)) → (𝑀‘𝑟) = (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))
189	182, 171, 187, 188	fmptco 6396	. . . . . . . 8 ⊢ (⊤ → (𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
190	189	trud 1493	. . . . . . 7 ⊢ (𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))
191		f1oeq1 6127	. . . . . . 7 ⊢ ((𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) → ((𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)))
192	190, 191	ax-mp 5	. . . . . 6 ⊢ ((𝑀 ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin))
193	170, 192	mpbi 220	. . . . 5 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
194		f1oco 6159	. . . . 5 ⊢ (((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)):(𝒫 (𝐽 × ℕ0) ∩ Fin)–1-1-onto→(𝒫 ℕ ∩ Fin) ∧ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)) → ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin))
195	46, 193, 194	mp2an 708	. . . 4 ⊢ ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)
196		simpr 477	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → 𝑜 ∈ (𝑇 ∩ 𝑅))
197		fvex 6201	. . . . . . . . 9 ⊢ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))) ∈ V
198		eqid 2622	. . . . . . . . . 10 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))
199	198	fvmpt2 6291	. . . . . . . . 9 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ∧ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))) ∈ V) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))‘𝑜) = (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))
200	196, 197, 199	sylancl 694	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))‘𝑜) = (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))
201		f1of 6137	. . . . . . . . . 10 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)⟶(𝒫 (𝐽 × ℕ0) ∩ Fin))
202	193, 201	mp1i 13	. . . . . . . . 9 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))):(𝑇 ∩ 𝑅)⟶(𝒫 (𝐽 × ℕ0) ∩ Fin))
203	202	ffvelrnda 6359	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))‘𝑜) ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin))
204	200, 203	eqeltrrd 2702	. . . . . . 7 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))) ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin))
205		eqidd 2623	. . . . . . 7 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
206		eqidd 2623	. . . . . . 7 ⊢ (⊤ → (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) = (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)))
207		imaeq2 5462	. . . . . . 7 ⊢ (𝑎 = (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))) → (𝐹 “ 𝑎) = (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
208	204, 205, 206, 207	fmptco 6396	. . . . . 6 ⊢ (⊤ → ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
209	208	trud 1493	. . . . 5 ⊢ ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
210		f1oeq1 6127	. . . . 5 ⊢ (((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) → (((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)))
211	209, 210	ax-mp 5	. . . 4 ⊢ (((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹 “ 𝑎)) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin) ↔ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin))
212	195, 211	mpbi 220	. . 3 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)
213		f1oco 6159	. . 3 ⊢ ((((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∧ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)) → (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))):(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅))
214	41, 212, 213	mp2an 708	. 2 ⊢ (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))):(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅)
215		eulerpart.g	. . . 4 ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
216	43	mpt2exg 7245	. . . . . . . . . 10 ⊢ ((𝐽 ∈ V ∧ ℕ0 ∈ V) → 𝐹 ∈ V)
217	55, 57, 216	mp2an 708	. . . . . . . . 9 ⊢ 𝐹 ∈ V
218		imaexg 7103	. . . . . . . . 9 ⊢ (𝐹 ∈ V → (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) ∈ V)
219	217, 218	ax-mp 5	. . . . . . . 8 ⊢ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) ∈ V
220		eqid 2622	. . . . . . . . 9 ⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
221	220	fvmpt2 6291	. . . . . . . 8 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ∧ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) ∈ V) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))‘𝑜) = (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
222	196, 219, 221	sylancl 694	. . . . . . 7 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))‘𝑜) = (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))
223		f1of 6137	. . . . . . . . 9 ⊢ ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin) → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)⟶(𝒫 ℕ ∩ Fin))
224	212, 223	mp1i 13	. . . . . . . 8 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))):(𝑇 ∩ 𝑅)⟶(𝒫 ℕ ∩ Fin))
225	224	ffvelrnda 6359	. . . . . . 7 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → ((𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))‘𝑜) ∈ (𝒫 ℕ ∩ Fin))
226	222, 225	eqeltrrd 2702	. . . . . 6 ⊢ ((⊤ ∧ 𝑜 ∈ (𝑇 ∩ 𝑅)) → (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) ∈ (𝒫 ℕ ∩ Fin))
227		eqidd 2623	. . . . . 6 ⊢ (⊤ → (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
228		indf1o 30086	. . . . . . . . . . 11 ⊢ (ℕ ∈ V → (𝟭‘ℕ):𝒫 ℕ–1-1-onto→({0, 1} ↑𝑚 ℕ))
229		f1ofn 6138	. . . . . . . . . . 11 ⊢ ((𝟭‘ℕ):𝒫 ℕ–1-1-onto→({0, 1} ↑𝑚 ℕ) → (𝟭‘ℕ) Fn 𝒫 ℕ)
230	1, 228, 229	mp2b 10	. . . . . . . . . 10 ⊢ (𝟭‘ℕ) Fn 𝒫 ℕ
231		dffn5 6241	. . . . . . . . . 10 ⊢ ((𝟭‘ℕ) Fn 𝒫 ℕ ↔ (𝟭‘ℕ) = (𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)))
232	230, 231	mpbi 220	. . . . . . . . 9 ⊢ (𝟭‘ℕ) = (𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏))
233	232	reseq1i 5392	. . . . . . . 8 ⊢ ((𝟭‘ℕ) ↾ Fin) = ((𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)) ↾ Fin)
234		resmpt3 5450	. . . . . . . 8 ⊢ ((𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏))
235	233, 234	eqtri 2644	. . . . . . 7 ⊢ ((𝟭‘ℕ) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏))
236	235	a1i 11	. . . . . 6 ⊢ (⊤ → ((𝟭‘ℕ) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏)))
237		fveq2 6191	. . . . . 6 ⊢ (𝑏 = (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) → ((𝟭‘ℕ)‘𝑏) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
238	226, 227, 236, 237	fmptco 6396	. . . . 5 ⊢ (⊤ → (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))))
239	238	trud 1493	. . . 4 ⊢ (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
240	215, 239	eqtr4i 2647	. . 3 ⊢ 𝐺 = (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
241		f1oeq1 6127	. . 3 ⊢ (𝐺 = (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) → (𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ↔ (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))):(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅)))
242	240, 241	ax-mp 5	. 2 ⊢ (𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ↔ (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))):(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅))
243	214, 242	mpbir 221	1 ⊢ 𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅)

Syntax hints:  ¬ wn 3   ↔ wb 196   ∧ wa 384   ∧ w3a 1037   = wceq 1483  ⊤wtru 1484   ∈ wcel 1990  {cab 2608  ∀wral 2912  ∃wrex 2913  {crab 2916  Vcvv 3200   ∖ cdif 3571   ∪ cun 3572   ∩ cin 3573   ⊆ wss 3574  ∅c0 3915  𝒫 cpw 4158  {csn 4177  {cpr 4179   class class class wbr 4653  {copab 4712   ↦ cmpt 4729   × cxp 5112  ^◡ccnv 5113  ran crn 5115   ↾ cres 5116   “ cima 5117   ∘ ccom 5118  Fun wfun 5882   Fn wfn 5883  ⟶wf 5884  –1-1→wf1 5885  –1-1-onto→wf1o 5887  ‘cfv 5888  (class class class)co 6650   ↦ cmpt2 6652   supp csupp 7295   ↑_𝑚 cmap 7857  Fincfn 7955   finSupp cfsupp 8275  0cc0 9936  1c1 9937   · cmul 9941   ≤ cle 10075  ℕcn 11020  2c2 11070  ℕ₀cn0 11292  ℤcz 11377  ↑cexp 12860  Σcsu 14416   ∥ cdvds 14983  bitscbits 15141  𝟭cind 30072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-ac2 9285  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-disj 4621  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-acn 8768  df-ac 8939  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-xnn0 11364  df-z 11378  df-uz 11688  df-rp 11833  df-fz 12327  df-fzo 12466  df-fl 12593  df-mod 12669  df-seq 12802  df-exp 12861  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-clim 14219  df-sum 14417  df-dvds 14984  df-bits 15144  df-ind 30073

This theorem is referenced by:  eulerpartlemgf  30441  eulerpartlemgs2  30442  eulerpartlemn  30443