Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  eulerpartgbij Structured version   Visualization version   GIF version

Theorem eulerpartgbij 29567
Description: Lemma for eulerpart 29577: 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.
StepHypRef Expression
1 nnex 10873 . . . . 5 ℕ ∈ V
2 indf1ofs 29221 . . . . 5 (ℕ ∈ V → ((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑𝑚 ℕ) ∣ (𝑓 “ {1}) ∈ Fin})
31, 2ax-mp 5 . . . 4 ((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑𝑚 ℕ) ∣ (𝑓 “ {1}) ∈ Fin}
4 incom 3766 . . . . . . 7 (({0, 1} ↑𝑚 ℕ) ∩ {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin}) = ({𝑓 ∣ (𝑓 “ ℕ) ∈ Fin} ∩ ({0, 1} ↑𝑚 ℕ))
5 eulerpart.r . . . . . . . 8 𝑅 = {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin}
65ineq2i 3772 . . . . . . 7 (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) = (({0, 1} ↑𝑚 ℕ) ∩ {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin})
7 dfrab2 3861 . . . . . . 7 {𝑓 ∈ ({0, 1} ↑𝑚 ℕ) ∣ (𝑓 “ ℕ) ∈ Fin} = ({𝑓 ∣ (𝑓 “ ℕ) ∈ Fin} ∩ ({0, 1} ↑𝑚 ℕ))
84, 6, 73eqtr4i 2641 . . . . . 6 (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) = {𝑓 ∈ ({0, 1} ↑𝑚 ℕ) ∣ (𝑓 “ ℕ) ∈ Fin}
9 elmapfun 7744 . . . . . . . . 9 (𝑓 ∈ ({0, 1} ↑𝑚 ℕ) → Fun 𝑓)
10 elmapi 7742 . . . . . . . . . 10 (𝑓 ∈ ({0, 1} ↑𝑚 ℕ) → 𝑓:ℕ⟶{0, 1})
11 frn 5952 . . . . . . . . . 10 (𝑓:ℕ⟶{0, 1} → ran 𝑓 ⊆ {0, 1})
1210, 11syl 17 . . . . . . . . 9 (𝑓 ∈ ({0, 1} ↑𝑚 ℕ) → ran 𝑓 ⊆ {0, 1})
13 fimacnvinrn2 6242 . . . . . . . . . 10 ((Fun 𝑓 ∧ ran 𝑓 ⊆ {0, 1}) → (𝑓 “ ℕ) = (𝑓 “ (ℕ ∩ {0, 1})))
14 df-pr 4127 . . . . . . . . . . . . . 14 {0, 1} = ({0} ∪ {1})
1514ineq2i 3772 . . . . . . . . . . . . 13 (ℕ ∩ {0, 1}) = (ℕ ∩ ({0} ∪ {1}))
16 indi 3831 . . . . . . . . . . . . 13 (ℕ ∩ ({0} ∪ {1})) = ((ℕ ∩ {0}) ∪ (ℕ ∩ {1}))
17 0nnn 10899 . . . . . . . . . . . . . . 15 ¬ 0 ∈ ℕ
18 disjsn 4191 . . . . . . . . . . . . . . 15 ((ℕ ∩ {0}) = ∅ ↔ ¬ 0 ∈ ℕ)
1917, 18mpbir 219 . . . . . . . . . . . . . 14 (ℕ ∩ {0}) = ∅
20 1nn 10878 . . . . . . . . . . . . . . . . 17 1 ∈ ℕ
21 1ex 9891 . . . . . . . . . . . . . . . . . 18 1 ∈ V
2221snss 4258 . . . . . . . . . . . . . . . . 17 (1 ∈ ℕ ↔ {1} ⊆ ℕ)
2320, 22mpbi 218 . . . . . . . . . . . . . . . 16 {1} ⊆ ℕ
24 dfss 3554 . . . . . . . . . . . . . . . 16 ({1} ⊆ ℕ ↔ {1} = ({1} ∩ ℕ))
2523, 24mpbi 218 . . . . . . . . . . . . . . 15 {1} = ({1} ∩ ℕ)
26 incom 3766 . . . . . . . . . . . . . . 15 ({1} ∩ ℕ) = (ℕ ∩ {1})
2725, 26eqtr2i 2632 . . . . . . . . . . . . . 14 (ℕ ∩ {1}) = {1}
2819, 27uneq12i 3726 . . . . . . . . . . . . 13 ((ℕ ∩ {0}) ∪ (ℕ ∩ {1})) = (∅ ∪ {1})
2915, 16, 283eqtri 2635 . . . . . . . . . . . 12 (ℕ ∩ {0, 1}) = (∅ ∪ {1})
30 uncom 3718 . . . . . . . . . . . 12 (∅ ∪ {1}) = ({1} ∪ ∅)
31 un0 3918 . . . . . . . . . . . 12 ({1} ∪ ∅) = {1}
3229, 30, 313eqtri 2635 . . . . . . . . . . 11 (ℕ ∩ {0, 1}) = {1}
3332imaeq2i 5370 . . . . . . . . . 10 (𝑓 “ (ℕ ∩ {0, 1})) = (𝑓 “ {1})
3413, 33syl6eq 2659 . . . . . . . . 9 ((Fun 𝑓 ∧ ran 𝑓 ⊆ {0, 1}) → (𝑓 “ ℕ) = (𝑓 “ {1}))
359, 12, 34syl2anc 690 . . . . . . . 8 (𝑓 ∈ ({0, 1} ↑𝑚 ℕ) → (𝑓 “ ℕ) = (𝑓 “ {1}))
3635eleq1d 2671 . . . . . . 7 (𝑓 ∈ ({0, 1} ↑𝑚 ℕ) → ((𝑓 “ ℕ) ∈ Fin ↔ (𝑓 “ {1}) ∈ Fin))
3736rabbiia 3160 . . . . . 6 {𝑓 ∈ ({0, 1} ↑𝑚 ℕ) ∣ (𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ ({0, 1} ↑𝑚 ℕ) ∣ (𝑓 “ {1}) ∈ Fin}
388, 37eqtr2i 2632 . . . . 5 {𝑓 ∈ ({0, 1} ↑𝑚 ℕ) ∣ (𝑓 “ {1}) ∈ Fin} = (({0, 1} ↑𝑚 ℕ) ∩ 𝑅)
39 f1oeq3 6027 . . . . 5 ({𝑓 ∈ ({0, 1} ↑𝑚 ℕ) ∣ (𝑓 “ {1}) ∈ Fin} = (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) → (((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑𝑚 ℕ) ∣ (𝑓 “ {1}) ∈ Fin} ↔ ((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅)))
4038, 39ax-mp 5 . . . 4 (((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑𝑚 ℕ) ∣ (𝑓 “ {1}) ∈ Fin} ↔ ((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅))
413, 40mpbi 218 . . 3 ((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅)
42 eulerpart.j . . . . . . 7 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
43 eulerpart.f . . . . . . 7 𝐹 = (𝑥𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))
4442, 43oddpwdc 29549 . . . . . 6 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ
45 f1opwfi 8130 . . . . . 6 (𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ → (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)):(𝒫 (𝐽 × ℕ0) ∩ Fin)–1-1-onto→(𝒫 ℕ ∩ Fin))
4644, 45ax-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 𝑀 = (𝑟𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐽𝑦 ∈ (𝑟𝑥))})
5247, 48, 49, 42, 43, 50, 51eulerpartlem1 29562 . . . . . . 7 𝑀:𝐻1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
53 bitsf1o 14951 . . . . . . . . . . . . . 14 (bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin)
5453a1i 11 . . . . . . . . . . . . 13 (⊤ → (bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin))
5542, 1rabex2 4737 . . . . . . . . . . . . . 14 𝐽 ∈ V
5655a1i 11 . . . . . . . . . . . . 13 (⊤ → 𝐽 ∈ V)
57 nn0ex 11145 . . . . . . . . . . . . . 14 0 ∈ V
5857a1i 11 . . . . . . . . . . . . 13 (⊤ → ℕ0 ∈ V)
5957pwex 4769 . . . . . . . . . . . . . . 15 𝒫 ℕ0 ∈ V
6059inex1 4722 . . . . . . . . . . . . . 14 (𝒫 ℕ0 ∩ Fin) ∈ V
6160a1i 11 . . . . . . . . . . . . 13 (⊤ → (𝒫 ℕ0 ∩ Fin) ∈ V)
62 0nn0 11154 . . . . . . . . . . . . . 14 0 ∈ ℕ0
6362a1i 11 . . . . . . . . . . . . 13 (⊤ → 0 ∈ ℕ0)
64 fvres 6102 . . . . . . . . . . . . . . 15 (0 ∈ ℕ0 → ((bits ↾ ℕ0)‘0) = (bits‘0))
6562, 64ax-mp 5 . . . . . . . . . . . . . 14 ((bits ↾ ℕ0)‘0) = (bits‘0)
66 0bits 14945 . . . . . . . . . . . . . 14 (bits‘0) = ∅
6765, 66eqtr2i 2632 . . . . . . . . . . . . 13 ∅ = ((bits ↾ ℕ0)‘0)
68 elmapi 7742 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (ℕ0𝑚 𝐽) → 𝑓:𝐽⟶ℕ0)
69 frnnn0supp 11196 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ V ∧ 𝑓:𝐽⟶ℕ0) → (𝑓 supp 0) = (𝑓 “ ℕ))
7055, 68, 69sylancr 693 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (ℕ0𝑚 𝐽) → (𝑓 supp 0) = (𝑓 “ ℕ))
7170eleq1d 2671 . . . . . . . . . . . . . . 15 (𝑓 ∈ (ℕ0𝑚 𝐽) → ((𝑓 supp 0) ∈ Fin ↔ (𝑓 “ ℕ) ∈ Fin))
7271rabbiia 3160 . . . . . . . . . . . . . 14 {𝑓 ∈ (ℕ0𝑚 𝐽) ∣ (𝑓 supp 0) ∈ Fin} = {𝑓 ∈ (ℕ0𝑚 𝐽) ∣ (𝑓 “ ℕ) ∈ Fin}
73 elmapfun 7744 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (ℕ0𝑚 𝐽) → Fun 𝑓)
74 vex 3175 . . . . . . . . . . . . . . . . 17 𝑓 ∈ V
75 funisfsupp 8140 . . . . . . . . . . . . . . . . 17 ((Fun 𝑓𝑓 ∈ V ∧ 0 ∈ ℕ0) → (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
7674, 62, 75mp3an23 1407 . . . . . . . . . . . . . . . 16 (Fun 𝑓 → (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
7773, 76syl 17 . . . . . . . . . . . . . . 15 (𝑓 ∈ (ℕ0𝑚 𝐽) → (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
7877rabbiia 3160 . . . . . . . . . . . . . 14 {𝑓 ∈ (ℕ0𝑚 𝐽) ∣ 𝑓 finSupp 0} = {𝑓 ∈ (ℕ0𝑚 𝐽) ∣ (𝑓 supp 0) ∈ Fin}
79 incom 3766 . . . . . . . . . . . . . . 15 ({𝑓 ∣ (𝑓 “ ℕ) ∈ Fin} ∩ (ℕ0𝑚 𝐽)) = ((ℕ0𝑚 𝐽) ∩ {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin})
80 dfrab2 3861 . . . . . . . . . . . . . . 15 {𝑓 ∈ (ℕ0𝑚 𝐽) ∣ (𝑓 “ ℕ) ∈ Fin} = ({𝑓 ∣ (𝑓 “ ℕ) ∈ Fin} ∩ (ℕ0𝑚 𝐽))
815ineq2i 3772 . . . . . . . . . . . . . . 15 ((ℕ0𝑚 𝐽) ∩ 𝑅) = ((ℕ0𝑚 𝐽) ∩ {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin})
8279, 80, 813eqtr4ri 2642 . . . . . . . . . . . . . 14 ((ℕ0𝑚 𝐽) ∩ 𝑅) = {𝑓 ∈ (ℕ0𝑚 𝐽) ∣ (𝑓 “ ℕ) ∈ Fin}
8372, 78, 823eqtr4ri 2642 . . . . . . . . . . . . 13 ((ℕ0𝑚 𝐽) ∩ 𝑅) = {𝑓 ∈ (ℕ0𝑚 𝐽) ∣ 𝑓 finSupp 0}
84 elmapfun 7744 . . . . . . . . . . . . . . 15 (𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) → Fun 𝑟)
85 vex 3175 . . . . . . . . . . . . . . . . 17 𝑟 ∈ V
86 0ex 4713 . . . . . . . . . . . . . . . . 17 ∅ ∈ V
87 funisfsupp 8140 . . . . . . . . . . . . . . . . 17 ((Fun 𝑟𝑟 ∈ V ∧ ∅ ∈ V) → (𝑟 finSupp ∅ ↔ (𝑟 supp ∅) ∈ Fin))
8885, 86, 87mp3an23 1407 . . . . . . . . . . . . . . . 16 (Fun 𝑟 → (𝑟 finSupp ∅ ↔ (𝑟 supp ∅) ∈ Fin))
8988bicomd 211 . . . . . . . . . . . . . . 15 (Fun 𝑟 → ((𝑟 supp ∅) ∈ Fin ↔ 𝑟 finSupp ∅))
9084, 89syl 17 . . . . . . . . . . . . . 14 (𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) → ((𝑟 supp ∅) ∈ Fin ↔ 𝑟 finSupp ∅))
9190rabbiia 3160 . . . . . . . . . . . . 13 {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ 𝑟 finSupp ∅}
9254, 56, 58, 61, 63, 67, 83, 91fcobijfs 28695 . . . . . . . . . . . 12 (⊤ → (𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)):((ℕ0𝑚 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
93 elinel1 3760 . . . . . . . . . . . . . . . 16 (𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) → 𝑓 ∈ (ℕ0𝑚 𝐽))
94 frn 5952 . . . . . . . . . . . . . . . . 17 (𝑓:𝐽⟶ℕ0 → ran 𝑓 ⊆ ℕ0)
95 cores 5541 . . . . . . . . . . . . . . . . 17 (ran 𝑓 ⊆ ℕ0 → ((bits ↾ ℕ0) ∘ 𝑓) = (bits ∘ 𝑓))
9668, 94, 953syl 18 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (ℕ0𝑚 𝐽) → ((bits ↾ ℕ0) ∘ 𝑓) = (bits ∘ 𝑓))
9793, 96syl 17 . . . . . . . . . . . . . . 15 (𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) → ((bits ↾ ℕ0) ∘ 𝑓) = (bits ∘ 𝑓))
9897mpteq2ia 4662 . . . . . . . . . . . . . 14 (𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)) = (𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓))
9998eqcomi 2618 . . . . . . . . . . . . 13 (𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓))
100 f1oeq1 6025 . . . . . . . . . . . . 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}))
10199, 100mp1i 13 . . . . . . . . . . . 12 (⊤ → ((𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0𝑚 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} ↔ (𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)):((ℕ0𝑚 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}))
10292, 101mpbird 245 . . . . . . . . . . 11 (⊤ → (𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0𝑚 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
103102trud 1483 . . . . . . . . . 10 (𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0𝑚 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
104 ssrab2 3649 . . . . . . . . . . . . . . . 16 {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ⊆ ℕ
10542, 104eqsstri 3597 . . . . . . . . . . . . . . 15 𝐽 ⊆ ℕ
1061, 57, 1053pm3.2i 1231 . . . . . . . . . . . . . 14 (ℕ ∈ V ∧ ℕ0 ∈ V ∧ 𝐽 ⊆ ℕ)
107 eulerpart.t . . . . . . . . . . . . . . . 16 𝑇 = {𝑓 ∈ (ℕ0𝑚 ℕ) ∣ (𝑓 “ ℕ) ⊆ 𝐽}
108 cnveq 5206 . . . . . . . . . . . . . . . . . . 19 (𝑓 = 𝑜𝑓 = 𝑜)
109 dfn2 11152 . . . . . . . . . . . . . . . . . . . 20 ℕ = (ℕ0 ∖ {0})
110109a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑓 = 𝑜 → ℕ = (ℕ0 ∖ {0}))
111108, 110imaeq12d 5373 . . . . . . . . . . . . . . . . . 18 (𝑓 = 𝑜 → (𝑓 “ ℕ) = (𝑜 “ (ℕ0 ∖ {0})))
112111sseq1d 3594 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝑜 → ((𝑓 “ ℕ) ⊆ 𝐽 ↔ (𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽))
113112cbvrabv 3171 . . . . . . . . . . . . . . . 16 {𝑓 ∈ (ℕ0𝑚 ℕ) ∣ (𝑓 “ ℕ) ⊆ 𝐽} = {𝑜 ∈ (ℕ0𝑚 ℕ) ∣ (𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽}
114107, 113eqtri 2631 . . . . . . . . . . . . . . 15 𝑇 = {𝑜 ∈ (ℕ0𝑚 ℕ) ∣ (𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽}
115 eqid 2609 . . . . . . . . . . . . . . 15 (𝑜𝑇 ↦ (𝑜𝐽)) = (𝑜𝑇 ↦ (𝑜𝐽))
116114, 115resf1o 28699 . . . . . . . . . . . . . 14 (((ℕ ∈ V ∧ ℕ0 ∈ V ∧ 𝐽 ⊆ ℕ) ∧ 0 ∈ ℕ0) → (𝑜𝑇 ↦ (𝑜𝐽)):𝑇1-1-onto→(ℕ0𝑚 𝐽))
117106, 62, 116mp2an 703 . . . . . . . . . . . . 13 (𝑜𝑇 ↦ (𝑜𝐽)):𝑇1-1-onto→(ℕ0𝑚 𝐽)
118 f1of1 6034 . . . . . . . . . . . . 13 ((𝑜𝑇 ↦ (𝑜𝐽)):𝑇1-1-onto→(ℕ0𝑚 𝐽) → (𝑜𝑇 ↦ (𝑜𝐽)):𝑇1-1→(ℕ0𝑚 𝐽))
119117, 118ax-mp 5 . . . . . . . . . . . 12 (𝑜𝑇 ↦ (𝑜𝐽)):𝑇1-1→(ℕ0𝑚 𝐽)
120 inss1 3794 . . . . . . . . . . . 12 (𝑇𝑅) ⊆ 𝑇
121 f1ores 6049 . . . . . . . . . . . 12 (((𝑜𝑇 ↦ (𝑜𝐽)):𝑇1-1→(ℕ0𝑚 𝐽) ∧ (𝑇𝑅) ⊆ 𝑇) → ((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)))
122119, 120, 121mp2an 703 . . . . . . . . . . 11 ((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅))
123 vex 3175 . . . . . . . . . . . . . . . . . 18 𝑜 ∈ V
124123resex 5350 . . . . . . . . . . . . . . . . 17 (𝑜𝐽) ∈ V
125124, 115fnmpti 5921 . . . . . . . . . . . . . . . 16 (𝑜𝑇 ↦ (𝑜𝐽)) Fn 𝑇
126 fvelimab 6148 . . . . . . . . . . . . . . . 16 (((𝑜𝑇 ↦ (𝑜𝐽)) Fn 𝑇 ∧ (𝑇𝑅) ⊆ 𝑇) → (𝑓 ∈ ((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) ↔ ∃𝑚 ∈ (𝑇𝑅)((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓))
127125, 120, 126mp2an 703 . . . . . . . . . . . . . . 15 (𝑓 ∈ ((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) ↔ ∃𝑚 ∈ (𝑇𝑅)((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓)
128 eqid 2609 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽)) = (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽))
129 vex 3175 . . . . . . . . . . . . . . . . . 18 𝑚 ∈ V
130129resex 5350 . . . . . . . . . . . . . . . . 17 (𝑚𝐽) ∈ V
131128, 130elrnmpti 5284 . . . . . . . . . . . . . . . 16 (𝑓 ∈ ran (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽)) ↔ ∃𝑚 ∈ (𝑇𝑅)𝑓 = (𝑚𝐽))
13247, 48, 49, 42, 43, 50, 51, 5, 107eulerpartlemt 29566 . . . . . . . . . . . . . . . . 17 ((ℕ0𝑚 𝐽) ∩ 𝑅) = ran (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽))
133132eleq2i 2679 . . . . . . . . . . . . . . . 16 (𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↔ 𝑓 ∈ ran (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽)))
134 elinel1 3760 . . . . . . . . . . . . . . . . . . 19 (𝑚 ∈ (𝑇𝑅) → 𝑚𝑇)
135115fvtresfn 6178 . . . . . . . . . . . . . . . . . . . 20 (𝑚𝑇 → ((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = (𝑚𝐽))
136135eqeq1d 2611 . . . . . . . . . . . . . . . . . . 19 (𝑚𝑇 → (((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓 ↔ (𝑚𝐽) = 𝑓))
137134, 136syl 17 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ (𝑇𝑅) → (((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓 ↔ (𝑚𝐽) = 𝑓))
138 eqcom 2616 . . . . . . . . . . . . . . . . . 18 ((𝑚𝐽) = 𝑓𝑓 = (𝑚𝐽))
139137, 138syl6bb 274 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ (𝑇𝑅) → (((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓𝑓 = (𝑚𝐽)))
140139rexbiia 3021 . . . . . . . . . . . . . . . 16 (∃𝑚 ∈ (𝑇𝑅)((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓 ↔ ∃𝑚 ∈ (𝑇𝑅)𝑓 = (𝑚𝐽))
141131, 133, 1403bitr4ri 291 . . . . . . . . . . . . . . 15 (∃𝑚 ∈ (𝑇𝑅)((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅))
142127, 141bitri 262 . . . . . . . . . . . . . 14 (𝑓 ∈ ((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) ↔ 𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅))
143142eqriv 2606 . . . . . . . . . . . . 13 ((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) = ((ℕ0𝑚 𝐽) ∩ 𝑅)
144 f1oeq3 6027 . . . . . . . . . . . . 13 (((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) = ((ℕ0𝑚 𝐽) ∩ 𝑅) → (((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) ↔ ((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((ℕ0𝑚 𝐽) ∩ 𝑅)))
145143, 144ax-mp 5 . . . . . . . . . . . 12 (((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) ↔ ((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((ℕ0𝑚 𝐽) ∩ 𝑅))
146 resmpt 5356 . . . . . . . . . . . . 13 ((𝑇𝑅) ⊆ 𝑇 → ((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)))
147 f1oeq1 6025 . . . . . . . . . . . . 13 (((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)) → (((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((ℕ0𝑚 𝐽) ∩ 𝑅) ↔ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)–1-1-onto→((ℕ0𝑚 𝐽) ∩ 𝑅)))
148120, 146, 147mp2b 10 . . . . . . . . . . . 12 (((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((ℕ0𝑚 𝐽) ∩ 𝑅) ↔ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)–1-1-onto→((ℕ0𝑚 𝐽) ∩ 𝑅))
149145, 148bitri 262 . . . . . . . . . . 11 (((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) ↔ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)–1-1-onto→((ℕ0𝑚 𝐽) ∩ 𝑅))
150122, 149mpbi 218 . . . . . . . . . 10 (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)–1-1-onto→((ℕ0𝑚 𝐽) ∩ 𝑅)
151 f1oco 6057 . . . . . . . . . 10 (((𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0𝑚 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} ∧ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)–1-1-onto→((ℕ0𝑚 𝐽) ∩ 𝑅)) → ((𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽))):(𝑇𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
152103, 150, 151mp2an 703 . . . . . . . . 9 ((𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽))):(𝑇𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
153 f1of 6035 . . . . . . . . . . . . . 14 ((𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)–1-1-onto→((ℕ0𝑚 𝐽) ∩ 𝑅) → (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)⟶((ℕ0𝑚 𝐽) ∩ 𝑅))
154 eqid 2609 . . . . . . . . . . . . . . . 16 (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽))
155154fmpt 6274 . . . . . . . . . . . . . . 15 (∀𝑜 ∈ (𝑇𝑅)(𝑜𝐽) ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↔ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)⟶((ℕ0𝑚 𝐽) ∩ 𝑅))
156155biimpri 216 . . . . . . . . . . . . . 14 ((𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)⟶((ℕ0𝑚 𝐽) ∩ 𝑅) → ∀𝑜 ∈ (𝑇𝑅)(𝑜𝐽) ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅))
157150, 153, 156mp2b 10 . . . . . . . . . . . . 13 𝑜 ∈ (𝑇𝑅)(𝑜𝐽) ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅)
158157a1i 11 . . . . . . . . . . . 12 (⊤ → ∀𝑜 ∈ (𝑇𝑅)(𝑜𝐽) ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅))
159 eqidd 2610 . . . . . . . . . . . 12 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)))
160 eqidd 2610 . . . . . . . . . . . 12 (⊤ → (𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)))
161 coeq2 5190 . . . . . . . . . . . 12 (𝑓 = (𝑜𝐽) → (bits ∘ 𝑓) = (bits ∘ (𝑜𝐽)))
162158, 159, 160, 161fmptcof 6289 . . . . . . . . . . 11 (⊤ → ((𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽))) = (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))))
163162eqcomd 2615 . . . . . . . . . 10 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))) = ((𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽))))
164 eqidd 2610 . . . . . . . . . 10 (⊤ → (𝑇𝑅) = (𝑇𝑅))
16550a1i 11 . . . . . . . . . 10 (⊤ → 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
166163, 164, 165f1oeq123d 6031 . . . . . . . . 9 (⊤ → ((𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)–1-1-onto𝐻 ↔ ((𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽))):(𝑇𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}))
167152, 166mpbiri 246 . . . . . . . 8 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)–1-1-onto𝐻)
168167trud 1483 . . . . . . 7 (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)–1-1-onto𝐻
169 f1oco 6057 . . . . . . 7 ((𝑀:𝐻1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) ∧ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)–1-1-onto𝐻) → (𝑀 ∘ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin))
17052, 168, 169mp2an 703 . . . . . 6 (𝑀 ∘ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
171 eqidd 2610 . . . . . . . . . . 11 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))) = (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))))
172 bitsf 14933 . . . . . . . . . . . . . 14 bits:ℤ⟶𝒫 ℕ0
173 zex 11219 . . . . . . . . . . . . . 14 ℤ ∈ V
174 fex 6372 . . . . . . . . . . . . . 14 ((bits:ℤ⟶𝒫 ℕ0 ∧ ℤ ∈ V) → bits ∈ V)
175172, 173, 174mp2an 703 . . . . . . . . . . . . 13 bits ∈ V
176175, 124coex 6988 . . . . . . . . . . . 12 (bits ∘ (𝑜𝐽)) ∈ V
177176a1i 11 . . . . . . . . . . 11 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → (bits ∘ (𝑜𝐽)) ∈ V)
178171, 177fvmpt2d 6187 . . . . . . . . . 10 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → ((𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))‘𝑜) = (bits ∘ (𝑜𝐽)))
179 f1of 6035 . . . . . . . . . . . 12 ((𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)–1-1-onto𝐻 → (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)⟶𝐻)
180167, 179syl 17 . . . . . . . . . . 11 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)⟶𝐻)
181180ffvelrnda 6252 . . . . . . . . . 10 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → ((𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))‘𝑜) ∈ 𝐻)
182178, 181eqeltrrd 2688 . . . . . . . . 9 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → (bits ∘ (𝑜𝐽)) ∈ 𝐻)
183 f1ofn 6036 . . . . . . . . . . . 12 (𝑀:𝐻1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) → 𝑀 Fn 𝐻)
18452, 183ax-mp 5 . . . . . . . . . . 11 𝑀 Fn 𝐻
185 dffn5 6136 . . . . . . . . . . 11 (𝑀 Fn 𝐻𝑀 = (𝑟𝐻 ↦ (𝑀𝑟)))
186184, 185mpbi 218 . . . . . . . . . 10 𝑀 = (𝑟𝐻 ↦ (𝑀𝑟))
187186a1i 11 . . . . . . . . 9 (⊤ → 𝑀 = (𝑟𝐻 ↦ (𝑀𝑟)))
188 fveq2 6088 . . . . . . . . 9 (𝑟 = (bits ∘ (𝑜𝐽)) → (𝑀𝑟) = (𝑀‘(bits ∘ (𝑜𝐽))))
189182, 171, 187, 188fmptco 6288 . . . . . . . 8 (⊤ → (𝑀 ∘ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))))
190189trud 1483 . . . . . . 7 (𝑀 ∘ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))
191 f1oeq1 6025 . . . . . . 7 ((𝑀 ∘ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))) → ((𝑀 ∘ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) ↔ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)))
192190, 191ax-mp 5 . . . . . 6 ((𝑀 ∘ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) ↔ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin))
193170, 192mpbi 218 . . . . 5 (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
194 f1oco 6057 . . . . 5 (((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)):(𝒫 (𝐽 × ℕ0) ∩ Fin)–1-1-onto→(𝒫 ℕ ∩ Fin) ∧ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)) → ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin))
19546, 193, 194mp2an 703 . . . 4 ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)
196 simpr 475 . . . . . . . . 9 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → 𝑜 ∈ (𝑇𝑅))
197 fvex 6098 . . . . . . . . 9 (𝑀‘(bits ∘ (𝑜𝐽))) ∈ V
198 eqid 2609 . . . . . . . . . 10 (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))
199198fvmpt2 6185 . . . . . . . . 9 ((𝑜 ∈ (𝑇𝑅) ∧ (𝑀‘(bits ∘ (𝑜𝐽))) ∈ V) → ((𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))‘𝑜) = (𝑀‘(bits ∘ (𝑜𝐽))))
200196, 197, 199sylancl 692 . . . . . . . 8 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → ((𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))‘𝑜) = (𝑀‘(bits ∘ (𝑜𝐽))))
201 f1of 6035 . . . . . . . . . 10 ((𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) → (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))):(𝑇𝑅)⟶(𝒫 (𝐽 × ℕ0) ∩ Fin))
202193, 201mp1i 13 . . . . . . . . 9 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))):(𝑇𝑅)⟶(𝒫 (𝐽 × ℕ0) ∩ Fin))
203202ffvelrnda 6252 . . . . . . . 8 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → ((𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))‘𝑜) ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin))
204200, 203eqeltrrd 2688 . . . . . . 7 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → (𝑀‘(bits ∘ (𝑜𝐽))) ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin))
205 eqidd 2610 . . . . . . 7 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))))
206 eqidd 2610 . . . . . . 7 (⊤ → (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) = (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)))
207 imaeq2 5368 . . . . . . 7 (𝑎 = (𝑀‘(bits ∘ (𝑜𝐽))) → (𝐹𝑎) = (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))
208204, 205, 206, 207fmptco 6288 . . . . . 6 (⊤ → ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
209208trud 1483 . . . . 5 ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))
210 f1oeq1 6025 . . . . 5 (((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))) → (((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin) ↔ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)))
211209, 210ax-mp 5 . . . 4 (((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin) ↔ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin))
212195, 211mpbi 218 . . 3 (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)
213 f1oco 6057 . . 3 ((((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∧ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)) → (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))):(𝑇𝑅)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅))
21441, 212, 213mp2an 703 . 2 (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))):(𝑇𝑅)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅)
215 eulerpart.g . . . 4 𝐺 = (𝑜 ∈ (𝑇𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
21643mpt2exg 7111 . . . . . . . . . 10 ((𝐽 ∈ V ∧ ℕ0 ∈ V) → 𝐹 ∈ V)
21755, 57, 216mp2an 703 . . . . . . . . 9 𝐹 ∈ V
218 imaexg 6972 . . . . . . . . 9 (𝐹 ∈ V → (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))) ∈ V)
219217, 218ax-mp 5 . . . . . . . 8 (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))) ∈ V
220 eqid 2609 . . . . . . . . 9 (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))
221220fvmpt2 6185 . . . . . . . 8 ((𝑜 ∈ (𝑇𝑅) ∧ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))) ∈ V) → ((𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))‘𝑜) = (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))
222196, 219, 221sylancl 692 . . . . . . 7 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → ((𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))‘𝑜) = (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))
223 f1of 6035 . . . . . . . . 9 ((𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin) → (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)⟶(𝒫 ℕ ∩ Fin))
224212, 223mp1i 13 . . . . . . . 8 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)⟶(𝒫 ℕ ∩ Fin))
225224ffvelrnda 6252 . . . . . . 7 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → ((𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))‘𝑜) ∈ (𝒫 ℕ ∩ Fin))
226222, 225eqeltrrd 2688 . . . . . 6 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))) ∈ (𝒫 ℕ ∩ Fin))
227 eqidd 2610 . . . . . 6 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
228 indf1o 29219 . . . . . . . . . . 11 (ℕ ∈ V → (𝟭‘ℕ):𝒫 ℕ–1-1-onto→({0, 1} ↑𝑚 ℕ))
229 f1ofn 6036 . . . . . . . . . . 11 ((𝟭‘ℕ):𝒫 ℕ–1-1-onto→({0, 1} ↑𝑚 ℕ) → (𝟭‘ℕ) Fn 𝒫 ℕ)
2301, 228, 229mp2b 10 . . . . . . . . . 10 (𝟭‘ℕ) Fn 𝒫 ℕ
231 dffn5 6136 . . . . . . . . . 10 ((𝟭‘ℕ) Fn 𝒫 ℕ ↔ (𝟭‘ℕ) = (𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)))
232230, 231mpbi 218 . . . . . . . . 9 (𝟭‘ℕ) = (𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏))
233232reseq1i 5300 . . . . . . . 8 ((𝟭‘ℕ) ↾ Fin) = ((𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)) ↾ Fin)
234 resmpt3 5357 . . . . . . . 8 ((𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏))
235233, 234eqtri 2631 . . . . . . 7 ((𝟭‘ℕ) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏))
236235a1i 11 . . . . . 6 (⊤ → ((𝟭‘ℕ) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏)))
237 fveq2 6088 . . . . . 6 (𝑏 = (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))) → ((𝟭‘ℕ)‘𝑏) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
238226, 227, 236, 237fmptco 6288 . . . . 5 (⊤ → (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) = (𝑜 ∈ (𝑇𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))))
239238trud 1483 . . . 4 (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) = (𝑜 ∈ (𝑇𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
240215, 239eqtr4i 2634 . . 3 𝐺 = (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
241 f1oeq1 6025 . . 3 (𝐺 = (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → (𝐺:(𝑇𝑅)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ↔ (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))):(𝑇𝑅)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅)))
242240, 241ax-mp 5 . 2 (𝐺:(𝑇𝑅)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ↔ (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))):(𝑇𝑅)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅))
243214, 242mpbir 219 1 𝐺:(𝑇𝑅)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 194  wa 382  w3a 1030   = wceq 1474  wtru 1475  wcel 1976  {cab 2595  wral 2895  wrex 2896  {crab 2899  Vcvv 3172  cdif 3536  cun 3537  cin 3538  wss 3539  c0 3873  𝒫 cpw 4107  {csn 4124  {cpr 4126   class class class wbr 4577  {copab 4636  cmpt 4637   × cxp 5026  ccnv 5027  ran crn 5029  cres 5030  cima 5031  ccom 5032  Fun wfun 5784   Fn wfn 5785  wf 5786  1-1wf1 5787  1-1-ontowf1o 5789  cfv 5790  (class class class)co 6527  cmpt2 6529   supp csupp 7159  𝑚 cmap 7721  Fincfn 7818   finSupp cfsupp 8135  0cc0 9792  1c1 9793   · cmul 9797  cle 9931  cn 10867  2c2 10917  0cn0 11139  cz 11210  cexp 12677  Σcsu 14210  cdvds 14767  bitscbits 14925  𝟭cind 29206
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-inf2 8398  ax-ac2 9145  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869  ax-pre-sup 9870
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-disj 4548  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6935  df-1st 7036  df-2nd 7037  df-supp 7160  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-2o 7425  df-oadd 7428  df-er 7606  df-map 7723  df-pm 7724  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-fsupp 8136  df-sup 8208  df-inf 8209  df-oi 8275  df-card 8625  df-acn 8628  df-ac 8799  df-cda 8850  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10534  df-nn 10868  df-2 10926  df-3 10927  df-n0 11140  df-z 11211  df-uz 11520  df-rp 11665  df-fz 12153  df-fzo 12290  df-fl 12410  df-mod 12486  df-seq 12619  df-exp 12678  df-hash 12935  df-cj 13633  df-re 13634  df-im 13635  df-sqrt 13769  df-abs 13770  df-clim 14013  df-sum 14211  df-dvds 14768  df-bits 14928  df-ind 29207
This theorem is referenced by:  eulerpartlemgf  29574  eulerpartlemgs2  29575  eulerpartlemn  29576
  Copyright terms: Public domain W3C validator