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 30741
Description: Lemma for eulerpart 30751: 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 11216 . . . . 5 ℕ ∈ V
2 indf1ofs 30395 . . . . 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 3946 . . . . . . 7 (({0, 1} ↑𝑚 ℕ) ∩ {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin}) = ({𝑓 ∣ (𝑓 “ ℕ) ∈ Fin} ∩ ({0, 1} ↑𝑚 ℕ))
5 eulerpart.r . . . . . . . 8 𝑅 = {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin}
65ineq2i 3952 . . . . . . 7 (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) = (({0, 1} ↑𝑚 ℕ) ∩ {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin})
7 dfrab2 4044 . . . . . . 7 {𝑓 ∈ ({0, 1} ↑𝑚 ℕ) ∣ (𝑓 “ ℕ) ∈ Fin} = ({𝑓 ∣ (𝑓 “ ℕ) ∈ Fin} ∩ ({0, 1} ↑𝑚 ℕ))
84, 6, 73eqtr4i 2790 . . . . . 6 (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) = {𝑓 ∈ ({0, 1} ↑𝑚 ℕ) ∣ (𝑓 “ ℕ) ∈ Fin}
9 elmapfun 8045 . . . . . . . . 9 (𝑓 ∈ ({0, 1} ↑𝑚 ℕ) → Fun 𝑓)
10 elmapi 8043 . . . . . . . . . 10 (𝑓 ∈ ({0, 1} ↑𝑚 ℕ) → 𝑓:ℕ⟶{0, 1})
11 frn 6212 . . . . . . . . . 10 (𝑓:ℕ⟶{0, 1} → ran 𝑓 ⊆ {0, 1})
1210, 11syl 17 . . . . . . . . 9 (𝑓 ∈ ({0, 1} ↑𝑚 ℕ) → ran 𝑓 ⊆ {0, 1})
13 fimacnvinrn2 6510 . . . . . . . . . 10 ((Fun 𝑓 ∧ ran 𝑓 ⊆ {0, 1}) → (𝑓 “ ℕ) = (𝑓 “ (ℕ ∩ {0, 1})))
14 df-pr 4322 . . . . . . . . . . . . . 14 {0, 1} = ({0} ∪ {1})
1514ineq2i 3952 . . . . . . . . . . . . 13 (ℕ ∩ {0, 1}) = (ℕ ∩ ({0} ∪ {1}))
16 indi 4014 . . . . . . . . . . . . 13 (ℕ ∩ ({0} ∪ {1})) = ((ℕ ∩ {0}) ∪ (ℕ ∩ {1}))
17 0nnn 11242 . . . . . . . . . . . . . . 15 ¬ 0 ∈ ℕ
18 disjsn 4388 . . . . . . . . . . . . . . 15 ((ℕ ∩ {0}) = ∅ ↔ ¬ 0 ∈ ℕ)
1917, 18mpbir 221 . . . . . . . . . . . . . 14 (ℕ ∩ {0}) = ∅
20 1nn 11221 . . . . . . . . . . . . . . . . 17 1 ∈ ℕ
21 1ex 10225 . . . . . . . . . . . . . . . . . 18 1 ∈ V
2221snss 4458 . . . . . . . . . . . . . . . . 17 (1 ∈ ℕ ↔ {1} ⊆ ℕ)
2320, 22mpbi 220 . . . . . . . . . . . . . . . 16 {1} ⊆ ℕ
24 dfss 3728 . . . . . . . . . . . . . . . 16 ({1} ⊆ ℕ ↔ {1} = ({1} ∩ ℕ))
2523, 24mpbi 220 . . . . . . . . . . . . . . 15 {1} = ({1} ∩ ℕ)
26 incom 3946 . . . . . . . . . . . . . . 15 ({1} ∩ ℕ) = (ℕ ∩ {1})
2725, 26eqtr2i 2781 . . . . . . . . . . . . . 14 (ℕ ∩ {1}) = {1}
2819, 27uneq12i 3906 . . . . . . . . . . . . 13 ((ℕ ∩ {0}) ∪ (ℕ ∩ {1})) = (∅ ∪ {1})
2915, 16, 283eqtri 2784 . . . . . . . . . . . 12 (ℕ ∩ {0, 1}) = (∅ ∪ {1})
30 uncom 3898 . . . . . . . . . . . 12 (∅ ∪ {1}) = ({1} ∪ ∅)
31 un0 4108 . . . . . . . . . . . 12 ({1} ∪ ∅) = {1}
3229, 30, 313eqtri 2784 . . . . . . . . . . 11 (ℕ ∩ {0, 1}) = {1}
3332imaeq2i 5620 . . . . . . . . . 10 (𝑓 “ (ℕ ∩ {0, 1})) = (𝑓 “ {1})
3413, 33syl6eq 2808 . . . . . . . . 9 ((Fun 𝑓 ∧ ran 𝑓 ⊆ {0, 1}) → (𝑓 “ ℕ) = (𝑓 “ {1}))
359, 12, 34syl2anc 696 . . . . . . . 8 (𝑓 ∈ ({0, 1} ↑𝑚 ℕ) → (𝑓 “ ℕ) = (𝑓 “ {1}))
3635eleq1d 2822 . . . . . . 7 (𝑓 ∈ ({0, 1} ↑𝑚 ℕ) → ((𝑓 “ ℕ) ∈ Fin ↔ (𝑓 “ {1}) ∈ Fin))
3736rabbiia 3322 . . . . . 6 {𝑓 ∈ ({0, 1} ↑𝑚 ℕ) ∣ (𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ ({0, 1} ↑𝑚 ℕ) ∣ (𝑓 “ {1}) ∈ Fin}
388, 37eqtr2i 2781 . . . . 5 {𝑓 ∈ ({0, 1} ↑𝑚 ℕ) ∣ (𝑓 “ {1}) ∈ Fin} = (({0, 1} ↑𝑚 ℕ) ∩ 𝑅)
39 f1oeq3 6288 . . . . 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 220 . . 3 ((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅)
42 eulerpart.j . . . . . . 7 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
43 eulerpart.f . . . . . . 7 𝐹 = (𝑥𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))
4442, 43oddpwdc 30723 . . . . . 6 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ
45 f1opwfi 8433 . . . . . 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 30736 . . . . . . 7 𝑀:𝐻1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
53 bitsf1o 15367 . . . . . . . . . . . . . 14 (bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin)
5453a1i 11 . . . . . . . . . . . . 13 (⊤ → (bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin))
5542, 1rabex2 4964 . . . . . . . . . . . . . 14 𝐽 ∈ V
5655a1i 11 . . . . . . . . . . . . 13 (⊤ → 𝐽 ∈ V)
57 nn0ex 11488 . . . . . . . . . . . . . 14 0 ∈ V
5857a1i 11 . . . . . . . . . . . . 13 (⊤ → ℕ0 ∈ V)
5957pwex 4995 . . . . . . . . . . . . . . 15 𝒫 ℕ0 ∈ V
6059inex1 4949 . . . . . . . . . . . . . 14 (𝒫 ℕ0 ∩ Fin) ∈ V
6160a1i 11 . . . . . . . . . . . . 13 (⊤ → (𝒫 ℕ0 ∩ Fin) ∈ V)
62 0nn0 11497 . . . . . . . . . . . . . 14 0 ∈ ℕ0
6362a1i 11 . . . . . . . . . . . . 13 (⊤ → 0 ∈ ℕ0)
64 fvres 6366 . . . . . . . . . . . . . . 15 (0 ∈ ℕ0 → ((bits ↾ ℕ0)‘0) = (bits‘0))
6562, 64ax-mp 5 . . . . . . . . . . . . . 14 ((bits ↾ ℕ0)‘0) = (bits‘0)
66 0bits 15361 . . . . . . . . . . . . . 14 (bits‘0) = ∅
6765, 66eqtr2i 2781 . . . . . . . . . . . . 13 ∅ = ((bits ↾ ℕ0)‘0)
68 elmapi 8043 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (ℕ0𝑚 𝐽) → 𝑓:𝐽⟶ℕ0)
69 frnnn0supp 11539 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ V ∧ 𝑓:𝐽⟶ℕ0) → (𝑓 supp 0) = (𝑓 “ ℕ))
7055, 68, 69sylancr 698 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (ℕ0𝑚 𝐽) → (𝑓 supp 0) = (𝑓 “ ℕ))
7170eleq1d 2822 . . . . . . . . . . . . . . 15 (𝑓 ∈ (ℕ0𝑚 𝐽) → ((𝑓 supp 0) ∈ Fin ↔ (𝑓 “ ℕ) ∈ Fin))
7271rabbiia 3322 . . . . . . . . . . . . . 14 {𝑓 ∈ (ℕ0𝑚 𝐽) ∣ (𝑓 supp 0) ∈ Fin} = {𝑓 ∈ (ℕ0𝑚 𝐽) ∣ (𝑓 “ ℕ) ∈ Fin}
73 elmapfun 8045 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (ℕ0𝑚 𝐽) → Fun 𝑓)
74 vex 3341 . . . . . . . . . . . . . . . . 17 𝑓 ∈ V
75 funisfsupp 8443 . . . . . . . . . . . . . . . . 17 ((Fun 𝑓𝑓 ∈ V ∧ 0 ∈ ℕ0) → (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
7674, 62, 75mp3an23 1563 . . . . . . . . . . . . . . . 16 (Fun 𝑓 → (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
7773, 76syl 17 . . . . . . . . . . . . . . 15 (𝑓 ∈ (ℕ0𝑚 𝐽) → (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
7877rabbiia 3322 . . . . . . . . . . . . . 14 {𝑓 ∈ (ℕ0𝑚 𝐽) ∣ 𝑓 finSupp 0} = {𝑓 ∈ (ℕ0𝑚 𝐽) ∣ (𝑓 supp 0) ∈ Fin}
79 incom 3946 . . . . . . . . . . . . . . 15 ({𝑓 ∣ (𝑓 “ ℕ) ∈ Fin} ∩ (ℕ0𝑚 𝐽)) = ((ℕ0𝑚 𝐽) ∩ {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin})
80 dfrab2 4044 . . . . . . . . . . . . . . 15 {𝑓 ∈ (ℕ0𝑚 𝐽) ∣ (𝑓 “ ℕ) ∈ Fin} = ({𝑓 ∣ (𝑓 “ ℕ) ∈ Fin} ∩ (ℕ0𝑚 𝐽))
815ineq2i 3952 . . . . . . . . . . . . . . 15 ((ℕ0𝑚 𝐽) ∩ 𝑅) = ((ℕ0𝑚 𝐽) ∩ {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin})
8279, 80, 813eqtr4ri 2791 . . . . . . . . . . . . . 14 ((ℕ0𝑚 𝐽) ∩ 𝑅) = {𝑓 ∈ (ℕ0𝑚 𝐽) ∣ (𝑓 “ ℕ) ∈ Fin}
8372, 78, 823eqtr4ri 2791 . . . . . . . . . . . . 13 ((ℕ0𝑚 𝐽) ∩ 𝑅) = {𝑓 ∈ (ℕ0𝑚 𝐽) ∣ 𝑓 finSupp 0}
84 elmapfun 8045 . . . . . . . . . . . . . . 15 (𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) → Fun 𝑟)
85 vex 3341 . . . . . . . . . . . . . . . . 17 𝑟 ∈ V
86 0ex 4940 . . . . . . . . . . . . . . . . 17 ∅ ∈ V
87 funisfsupp 8443 . . . . . . . . . . . . . . . . 17 ((Fun 𝑟𝑟 ∈ V ∧ ∅ ∈ V) → (𝑟 finSupp ∅ ↔ (𝑟 supp ∅) ∈ Fin))
8885, 86, 87mp3an23 1563 . . . . . . . . . . . . . . . 16 (Fun 𝑟 → (𝑟 finSupp ∅ ↔ (𝑟 supp ∅) ∈ Fin))
8988bicomd 213 . . . . . . . . . . . . . . 15 (Fun 𝑟 → ((𝑟 supp ∅) ∈ Fin ↔ 𝑟 finSupp ∅))
9084, 89syl 17 . . . . . . . . . . . . . 14 (𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) → ((𝑟 supp ∅) ∈ Fin ↔ 𝑟 finSupp ∅))
9190rabbiia 3322 . . . . . . . . . . . . 13 {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ 𝑟 finSupp ∅}
9254, 56, 58, 61, 63, 67, 83, 91fcobijfs 29808 . . . . . . . . . . . 12 (⊤ → (𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)):((ℕ0𝑚 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
93 elinel1 3940 . . . . . . . . . . . . . . . 16 (𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) → 𝑓 ∈ (ℕ0𝑚 𝐽))
94 frn 6212 . . . . . . . . . . . . . . . . 17 (𝑓:𝐽⟶ℕ0 → ran 𝑓 ⊆ ℕ0)
95 cores 5797 . . . . . . . . . . . . . . . . 17 (ran 𝑓 ⊆ ℕ0 → ((bits ↾ ℕ0) ∘ 𝑓) = (bits ∘ 𝑓))
9668, 94, 953syl 18 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (ℕ0𝑚 𝐽) → ((bits ↾ ℕ0) ∘ 𝑓) = (bits ∘ 𝑓))
9793, 96syl 17 . . . . . . . . . . . . . . 15 (𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) → ((bits ↾ ℕ0) ∘ 𝑓) = (bits ∘ 𝑓))
9897mpteq2ia 4890 . . . . . . . . . . . . . 14 (𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)) = (𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓))
9998eqcomi 2767 . . . . . . . . . . . . 13 (𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓))
100 f1oeq1 6286 . . . . . . . . . . . . 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 247 . . . . . . . . . . 11 (⊤ → (𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0𝑚 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
103102trud 1640 . . . . . . . . . 10 (𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0𝑚 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
104 ssrab2 3826 . . . . . . . . . . . . . . . 16 {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ⊆ ℕ
10542, 104eqsstri 3774 . . . . . . . . . . . . . . 15 𝐽 ⊆ ℕ
1061, 57, 1053pm3.2i 1424 . . . . . . . . . . . . . 14 (ℕ ∈ V ∧ ℕ0 ∈ V ∧ 𝐽 ⊆ ℕ)
107 eulerpart.t . . . . . . . . . . . . . . . 16 𝑇 = {𝑓 ∈ (ℕ0𝑚 ℕ) ∣ (𝑓 “ ℕ) ⊆ 𝐽}
108 cnveq 5449 . . . . . . . . . . . . . . . . . . 19 (𝑓 = 𝑜𝑓 = 𝑜)
109 dfn2 11495 . . . . . . . . . . . . . . . . . . . 20 ℕ = (ℕ0 ∖ {0})
110109a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑓 = 𝑜 → ℕ = (ℕ0 ∖ {0}))
111108, 110imaeq12d 5623 . . . . . . . . . . . . . . . . . 18 (𝑓 = 𝑜 → (𝑓 “ ℕ) = (𝑜 “ (ℕ0 ∖ {0})))
112111sseq1d 3771 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝑜 → ((𝑓 “ ℕ) ⊆ 𝐽 ↔ (𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽))
113112cbvrabv 3337 . . . . . . . . . . . . . . . 16 {𝑓 ∈ (ℕ0𝑚 ℕ) ∣ (𝑓 “ ℕ) ⊆ 𝐽} = {𝑜 ∈ (ℕ0𝑚 ℕ) ∣ (𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽}
114107, 113eqtri 2780 . . . . . . . . . . . . . . 15 𝑇 = {𝑜 ∈ (ℕ0𝑚 ℕ) ∣ (𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽}
115 eqid 2758 . . . . . . . . . . . . . . 15 (𝑜𝑇 ↦ (𝑜𝐽)) = (𝑜𝑇 ↦ (𝑜𝐽))
116114, 115resf1o 29812 . . . . . . . . . . . . . 14 (((ℕ ∈ V ∧ ℕ0 ∈ V ∧ 𝐽 ⊆ ℕ) ∧ 0 ∈ ℕ0) → (𝑜𝑇 ↦ (𝑜𝐽)):𝑇1-1-onto→(ℕ0𝑚 𝐽))
117106, 62, 116mp2an 710 . . . . . . . . . . . . 13 (𝑜𝑇 ↦ (𝑜𝐽)):𝑇1-1-onto→(ℕ0𝑚 𝐽)
118 f1of1 6295 . . . . . . . . . . . . 13 ((𝑜𝑇 ↦ (𝑜𝐽)):𝑇1-1-onto→(ℕ0𝑚 𝐽) → (𝑜𝑇 ↦ (𝑜𝐽)):𝑇1-1→(ℕ0𝑚 𝐽))
119117, 118ax-mp 5 . . . . . . . . . . . 12 (𝑜𝑇 ↦ (𝑜𝐽)):𝑇1-1→(ℕ0𝑚 𝐽)
120 inss1 3974 . . . . . . . . . . . 12 (𝑇𝑅) ⊆ 𝑇
121 f1ores 6310 . . . . . . . . . . . 12 (((𝑜𝑇 ↦ (𝑜𝐽)):𝑇1-1→(ℕ0𝑚 𝐽) ∧ (𝑇𝑅) ⊆ 𝑇) → ((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)))
122119, 120, 121mp2an 710 . . . . . . . . . . 11 ((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅))
123 vex 3341 . . . . . . . . . . . . . . . . . 18 𝑜 ∈ V
124123resex 5599 . . . . . . . . . . . . . . . . 17 (𝑜𝐽) ∈ V
125124, 115fnmpti 6181 . . . . . . . . . . . . . . . 16 (𝑜𝑇 ↦ (𝑜𝐽)) Fn 𝑇
126 fvelimab 6413 . . . . . . . . . . . . . . . 16 (((𝑜𝑇 ↦ (𝑜𝐽)) Fn 𝑇 ∧ (𝑇𝑅) ⊆ 𝑇) → (𝑓 ∈ ((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) ↔ ∃𝑚 ∈ (𝑇𝑅)((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓))
127125, 120, 126mp2an 710 . . . . . . . . . . . . . . 15 (𝑓 ∈ ((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) ↔ ∃𝑚 ∈ (𝑇𝑅)((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓)
128 eqid 2758 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽)) = (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽))
129 vex 3341 . . . . . . . . . . . . . . . . . 18 𝑚 ∈ V
130129resex 5599 . . . . . . . . . . . . . . . . 17 (𝑚𝐽) ∈ V
131128, 130elrnmpti 5529 . . . . . . . . . . . . . . . 16 (𝑓 ∈ ran (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽)) ↔ ∃𝑚 ∈ (𝑇𝑅)𝑓 = (𝑚𝐽))
13247, 48, 49, 42, 43, 50, 51, 5, 107eulerpartlemt 30740 . . . . . . . . . . . . . . . . 17 ((ℕ0𝑚 𝐽) ∩ 𝑅) = ran (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽))
133132eleq2i 2829 . . . . . . . . . . . . . . . 16 (𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↔ 𝑓 ∈ ran (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽)))
134 elinel1 3940 . . . . . . . . . . . . . . . . . . 19 (𝑚 ∈ (𝑇𝑅) → 𝑚𝑇)
135115fvtresfn 6444 . . . . . . . . . . . . . . . . . . . 20 (𝑚𝑇 → ((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = (𝑚𝐽))
136135eqeq1d 2760 . . . . . . . . . . . . . . . . . . 19 (𝑚𝑇 → (((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓 ↔ (𝑚𝐽) = 𝑓))
137134, 136syl 17 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ (𝑇𝑅) → (((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓 ↔ (𝑚𝐽) = 𝑓))
138 eqcom 2765 . . . . . . . . . . . . . . . . . 18 ((𝑚𝐽) = 𝑓𝑓 = (𝑚𝐽))
139137, 138syl6bb 276 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ (𝑇𝑅) → (((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓𝑓 = (𝑚𝐽)))
140139rexbiia 3176 . . . . . . . . . . . . . . . 16 (∃𝑚 ∈ (𝑇𝑅)((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓 ↔ ∃𝑚 ∈ (𝑇𝑅)𝑓 = (𝑚𝐽))
141131, 133, 1403bitr4ri 293 . . . . . . . . . . . . . . 15 (∃𝑚 ∈ (𝑇𝑅)((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅))
142127, 141bitri 264 . . . . . . . . . . . . . 14 (𝑓 ∈ ((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) ↔ 𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅))
143142eqriv 2755 . . . . . . . . . . . . 13 ((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) = ((ℕ0𝑚 𝐽) ∩ 𝑅)
144 f1oeq3 6288 . . . . . . . . . . . . 13 (((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) = ((ℕ0𝑚 𝐽) ∩ 𝑅) → (((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) ↔ ((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((ℕ0𝑚 𝐽) ∩ 𝑅)))
145143, 144ax-mp 5 . . . . . . . . . . . 12 (((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) ↔ ((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((ℕ0𝑚 𝐽) ∩ 𝑅))
146 resmpt 5605 . . . . . . . . . . . . 13 ((𝑇𝑅) ⊆ 𝑇 → ((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)))
147 f1oeq1 6286 . . . . . . . . . . . . 13 (((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)) → (((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((ℕ0𝑚 𝐽) ∩ 𝑅) ↔ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)–1-1-onto→((ℕ0𝑚 𝐽) ∩ 𝑅)))
148120, 146, 147mp2b 10 . . . . . . . . . . . 12 (((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((ℕ0𝑚 𝐽) ∩ 𝑅) ↔ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)–1-1-onto→((ℕ0𝑚 𝐽) ∩ 𝑅))
149145, 148bitri 264 . . . . . . . . . . 11 (((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) ↔ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)–1-1-onto→((ℕ0𝑚 𝐽) ∩ 𝑅))
150122, 149mpbi 220 . . . . . . . . . 10 (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)–1-1-onto→((ℕ0𝑚 𝐽) ∩ 𝑅)
151 f1oco 6318 . . . . . . . . . 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 710 . . . . . . . . 9 ((𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽))):(𝑇𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
153 f1of 6296 . . . . . . . . . . . . . 14 ((𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)–1-1-onto→((ℕ0𝑚 𝐽) ∩ 𝑅) → (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)⟶((ℕ0𝑚 𝐽) ∩ 𝑅))
154 eqid 2758 . . . . . . . . . . . . . . . 16 (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽))
155154fmpt 6542 . . . . . . . . . . . . . . 15 (∀𝑜 ∈ (𝑇𝑅)(𝑜𝐽) ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↔ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)⟶((ℕ0𝑚 𝐽) ∩ 𝑅))
156155biimpri 218 . . . . . . . . . . . . . 14 ((𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)⟶((ℕ0𝑚 𝐽) ∩ 𝑅) → ∀𝑜 ∈ (𝑇𝑅)(𝑜𝐽) ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅))
157150, 153, 156mp2b 10 . . . . . . . . . . . . 13 𝑜 ∈ (𝑇𝑅)(𝑜𝐽) ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅)
158157a1i 11 . . . . . . . . . . . 12 (⊤ → ∀𝑜 ∈ (𝑇𝑅)(𝑜𝐽) ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅))
159 eqidd 2759 . . . . . . . . . . . 12 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)))
160 eqidd 2759 . . . . . . . . . . . 12 (⊤ → (𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)))
161 coeq2 5434 . . . . . . . . . . . 12 (𝑓 = (𝑜𝐽) → (bits ∘ 𝑓) = (bits ∘ (𝑜𝐽)))
162158, 159, 160, 161fmptcof 6558 . . . . . . . . . . 11 (⊤ → ((𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽))) = (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))))
163162eqcomd 2764 . . . . . . . . . 10 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))) = ((𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽))))
164 eqidd 2759 . . . . . . . . . 10 (⊤ → (𝑇𝑅) = (𝑇𝑅))
16550a1i 11 . . . . . . . . . 10 (⊤ → 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
166163, 164, 165f1oeq123d 6292 . . . . . . . . 9 (⊤ → ((𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)–1-1-onto𝐻 ↔ ((𝑓 ∈ ((ℕ0𝑚 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽))):(𝑇𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}))
167152, 166mpbiri 248 . . . . . . . 8 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)–1-1-onto𝐻)
168167trud 1640 . . . . . . 7 (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)–1-1-onto𝐻
169 f1oco 6318 . . . . . . 7 ((𝑀:𝐻1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) ∧ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)–1-1-onto𝐻) → (𝑀 ∘ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin))
17052, 168, 169mp2an 710 . . . . . 6 (𝑀 ∘ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
171 eqidd 2759 . . . . . . . . . . 11 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))) = (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))))
172 bitsf 15349 . . . . . . . . . . . . . 14 bits:ℤ⟶𝒫 ℕ0
173 zex 11576 . . . . . . . . . . . . . 14 ℤ ∈ V
174 fex 6651 . . . . . . . . . . . . . 14 ((bits:ℤ⟶𝒫 ℕ0 ∧ ℤ ∈ V) → bits ∈ V)
175172, 173, 174mp2an 710 . . . . . . . . . . . . 13 bits ∈ V
176175, 124coex 7281 . . . . . . . . . . . 12 (bits ∘ (𝑜𝐽)) ∈ V
177176a1i 11 . . . . . . . . . . 11 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → (bits ∘ (𝑜𝐽)) ∈ V)
178171, 177fvmpt2d 6453 . . . . . . . . . 10 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → ((𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))‘𝑜) = (bits ∘ (𝑜𝐽)))
179 f1of 6296 . . . . . . . . . . . 12 ((𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)–1-1-onto𝐻 → (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)⟶𝐻)
180167, 179syl 17 . . . . . . . . . . 11 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)⟶𝐻)
181180ffvelrnda 6520 . . . . . . . . . 10 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → ((𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))‘𝑜) ∈ 𝐻)
182178, 181eqeltrrd 2838 . . . . . . . . 9 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → (bits ∘ (𝑜𝐽)) ∈ 𝐻)
183 f1ofn 6297 . . . . . . . . . . . 12 (𝑀:𝐻1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) → 𝑀 Fn 𝐻)
18452, 183ax-mp 5 . . . . . . . . . . 11 𝑀 Fn 𝐻
185 dffn5 6401 . . . . . . . . . . 11 (𝑀 Fn 𝐻𝑀 = (𝑟𝐻 ↦ (𝑀𝑟)))
186184, 185mpbi 220 . . . . . . . . . 10 𝑀 = (𝑟𝐻 ↦ (𝑀𝑟))
187186a1i 11 . . . . . . . . 9 (⊤ → 𝑀 = (𝑟𝐻 ↦ (𝑀𝑟)))
188 fveq2 6350 . . . . . . . . 9 (𝑟 = (bits ∘ (𝑜𝐽)) → (𝑀𝑟) = (𝑀‘(bits ∘ (𝑜𝐽))))
189182, 171, 187, 188fmptco 6557 . . . . . . . 8 (⊤ → (𝑀 ∘ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))))
190189trud 1640 . . . . . . 7 (𝑀 ∘ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))
191 f1oeq1 6286 . . . . . . 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 220 . . . . 5 (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
194 f1oco 6318 . . . . 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 710 . . . 4 ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)
196 simpr 479 . . . . . . . . 9 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → 𝑜 ∈ (𝑇𝑅))
197 fvex 6360 . . . . . . . . 9 (𝑀‘(bits ∘ (𝑜𝐽))) ∈ V
198 eqid 2758 . . . . . . . . . 10 (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))
199198fvmpt2 6451 . . . . . . . . 9 ((𝑜 ∈ (𝑇𝑅) ∧ (𝑀‘(bits ∘ (𝑜𝐽))) ∈ V) → ((𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))‘𝑜) = (𝑀‘(bits ∘ (𝑜𝐽))))
200196, 197, 199sylancl 697 . . . . . . . 8 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → ((𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))‘𝑜) = (𝑀‘(bits ∘ (𝑜𝐽))))
201 f1of 6296 . . . . . . . . . 10 ((𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) → (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))):(𝑇𝑅)⟶(𝒫 (𝐽 × ℕ0) ∩ Fin))
202193, 201mp1i 13 . . . . . . . . 9 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))):(𝑇𝑅)⟶(𝒫 (𝐽 × ℕ0) ∩ Fin))
203202ffvelrnda 6520 . . . . . . . 8 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → ((𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))‘𝑜) ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin))
204200, 203eqeltrrd 2838 . . . . . . 7 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → (𝑀‘(bits ∘ (𝑜𝐽))) ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin))
205 eqidd 2759 . . . . . . 7 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))))
206 eqidd 2759 . . . . . . 7 (⊤ → (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) = (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)))
207 imaeq2 5618 . . . . . . 7 (𝑎 = (𝑀‘(bits ∘ (𝑜𝐽))) → (𝐹𝑎) = (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))
208204, 205, 206, 207fmptco 6557 . . . . . 6 (⊤ → ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
209208trud 1640 . . . . 5 ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))
210 f1oeq1 6286 . . . . 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 220 . . 3 (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)
213 f1oco 6318 . . 3 ((((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∧ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)) → (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))):(𝑇𝑅)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅))
21441, 212, 213mp2an 710 . 2 (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))):(𝑇𝑅)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅)
215 eulerpart.g . . . 4 𝐺 = (𝑜 ∈ (𝑇𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
21643mpt2exg 7411 . . . . . . . . . 10 ((𝐽 ∈ V ∧ ℕ0 ∈ V) → 𝐹 ∈ V)
21755, 57, 216mp2an 710 . . . . . . . . 9 𝐹 ∈ V
218 imaexg 7266 . . . . . . . . 9 (𝐹 ∈ V → (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))) ∈ V)
219217, 218ax-mp 5 . . . . . . . 8 (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))) ∈ V
220 eqid 2758 . . . . . . . . 9 (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))
221220fvmpt2 6451 . . . . . . . 8 ((𝑜 ∈ (𝑇𝑅) ∧ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))) ∈ V) → ((𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))‘𝑜) = (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))
222196, 219, 221sylancl 697 . . . . . . 7 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → ((𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))‘𝑜) = (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))
223 f1of 6296 . . . . . . . . 9 ((𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin) → (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)⟶(𝒫 ℕ ∩ Fin))
224212, 223mp1i 13 . . . . . . . 8 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)⟶(𝒫 ℕ ∩ Fin))
225224ffvelrnda 6520 . . . . . . 7 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → ((𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))‘𝑜) ∈ (𝒫 ℕ ∩ Fin))
226222, 225eqeltrrd 2838 . . . . . 6 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))) ∈ (𝒫 ℕ ∩ Fin))
227 eqidd 2759 . . . . . 6 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
228 indf1o 30393 . . . . . . . . . . 11 (ℕ ∈ V → (𝟭‘ℕ):𝒫 ℕ–1-1-onto→({0, 1} ↑𝑚 ℕ))
229 f1ofn 6297 . . . . . . . . . . 11 ((𝟭‘ℕ):𝒫 ℕ–1-1-onto→({0, 1} ↑𝑚 ℕ) → (𝟭‘ℕ) Fn 𝒫 ℕ)
2301, 228, 229mp2b 10 . . . . . . . . . 10 (𝟭‘ℕ) Fn 𝒫 ℕ
231 dffn5 6401 . . . . . . . . . 10 ((𝟭‘ℕ) Fn 𝒫 ℕ ↔ (𝟭‘ℕ) = (𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)))
232230, 231mpbi 220 . . . . . . . . 9 (𝟭‘ℕ) = (𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏))
233232reseq1i 5545 . . . . . . . 8 ((𝟭‘ℕ) ↾ Fin) = ((𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)) ↾ Fin)
234 resmpt3 5606 . . . . . . . 8 ((𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏))
235233, 234eqtri 2780 . . . . . . 7 ((𝟭‘ℕ) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏))
236235a1i 11 . . . . . 6 (⊤ → ((𝟭‘ℕ) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏)))
237 fveq2 6350 . . . . . 6 (𝑏 = (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))) → ((𝟭‘ℕ)‘𝑏) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
238226, 227, 236, 237fmptco 6557 . . . . 5 (⊤ → (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) = (𝑜 ∈ (𝑇𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))))
239238trud 1640 . . . 4 (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) = (𝑜 ∈ (𝑇𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
240215, 239eqtr4i 2783 . . 3 𝐺 = (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
241 f1oeq1 6286 . . 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 221 1 𝐺:(𝑇𝑅)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wa 383  w3a 1072   = wceq 1630  wtru 1631  wcel 2137  {cab 2744  wral 3048  wrex 3049  {crab 3052  Vcvv 3338  cdif 3710  cun 3711  cin 3712  wss 3713  c0 4056  𝒫 cpw 4300  {csn 4319  {cpr 4321   class class class wbr 4802  {copab 4862  cmpt 4879   × cxp 5262  ccnv 5263  ran crn 5265  cres 5266  cima 5267  ccom 5268  Fun wfun 6041   Fn wfn 6042  wf 6043  1-1wf1 6044  1-1-ontowf1o 6046  cfv 6047  (class class class)co 6811  cmpt2 6813   supp csupp 7461  𝑚 cmap 8021  Fincfn 8119   finSupp cfsupp 8438  0cc0 10126  1c1 10127   · cmul 10131  cle 10265  cn 11210  2c2 11260  0cn0 11482  cz 11567  cexp 13052  Σcsu 14613  cdvds 15180  bitscbits 15341  𝟭cind 30379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-rep 4921  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053  ax-un 7112  ax-inf2 8709  ax-ac2 9475  ax-cnex 10182  ax-resscn 10183  ax-1cn 10184  ax-icn 10185  ax-addcl 10186  ax-addrcl 10187  ax-mulcl 10188  ax-mulrcl 10189  ax-mulcom 10190  ax-addass 10191  ax-mulass 10192  ax-distr 10193  ax-i2m1 10194  ax-1ne0 10195  ax-1rid 10196  ax-rnegex 10197  ax-rrecex 10198  ax-cnre 10199  ax-pre-lttri 10200  ax-pre-lttrn 10201  ax-pre-ltadd 10202  ax-pre-mulgt0 10203  ax-pre-sup 10204
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1633  df-fal 1636  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-nel 3034  df-ral 3053  df-rex 3054  df-reu 3055  df-rmo 3056  df-rab 3057  df-v 3340  df-sbc 3575  df-csb 3673  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-pss 3729  df-nul 4057  df-if 4229  df-pw 4302  df-sn 4320  df-pr 4322  df-tp 4324  df-op 4326  df-uni 4587  df-int 4626  df-iun 4672  df-disj 4771  df-br 4803  df-opab 4863  df-mpt 4880  df-tr 4903  df-id 5172  df-eprel 5177  df-po 5185  df-so 5186  df-fr 5223  df-se 5224  df-we 5225  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-rn 5275  df-res 5276  df-ima 5277  df-pred 5839  df-ord 5885  df-on 5886  df-lim 5887  df-suc 5888  df-iota 6010  df-fun 6049  df-fn 6050  df-f 6051  df-f1 6052  df-fo 6053  df-f1o 6054  df-fv 6055  df-isom 6056  df-riota 6772  df-ov 6814  df-oprab 6815  df-mpt2 6816  df-om 7229  df-1st 7331  df-2nd 7332  df-supp 7462  df-wrecs 7574  df-recs 7635  df-rdg 7673  df-1o 7727  df-2o 7728  df-oadd 7731  df-er 7909  df-map 8023  df-pm 8024  df-en 8120  df-dom 8121  df-sdom 8122  df-fin 8123  df-fsupp 8439  df-sup 8511  df-inf 8512  df-oi 8578  df-card 8953  df-acn 8956  df-ac 9127  df-cda 9180  df-pnf 10266  df-mnf 10267  df-xr 10268  df-ltxr 10269  df-le 10270  df-sub 10458  df-neg 10459  df-div 10875  df-nn 11211  df-2 11269  df-3 11270  df-n0 11483  df-xnn0 11554  df-z 11568  df-uz 11878  df-rp 12024  df-fz 12518  df-fzo 12658  df-fl 12785  df-mod 12861  df-seq 12994  df-exp 13053  df-hash 13310  df-cj 14036  df-re 14037  df-im 14038  df-sqrt 14172  df-abs 14173  df-clim 14416  df-sum 14614  df-dvds 15181  df-bits 15344  df-ind 30380
This theorem is referenced by:  eulerpartlemgf  30748  eulerpartlemgs2  30749  eulerpartlemn  30750
  Copyright terms: Public domain W3C validator