# Metamath Proof Explorer

## Theorem eulerpartlemgh

Description: Lemma for eulerpart : The F function is a bijection on the U subsets. (Contributed by Thierry Arnoux, 15-Aug-2018)

Ref Expression
Hypotheses eulerpart.p ${⊢}{P}=\left\{{f}\in \left({{ℕ}_{0}}^{ℕ}\right)|\left({{f}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\wedge \sum _{{k}\in ℕ}{f}\left({k}\right){k}={N}\right)\right\}$
eulerpart.o ${⊢}{O}=\left\{{g}\in {P}|\forall {n}\in {{g}}^{-1}\left[ℕ\right]\phantom{\rule{.4em}{0ex}}¬2\parallel {n}\right\}$
eulerpart.d ${⊢}{D}=\left\{{g}\in {P}|\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({n}\right)\le 1\right\}$
eulerpart.j ${⊢}{J}=\left\{{z}\in ℕ|¬2\parallel {z}\right\}$
eulerpart.f ${⊢}{F}=\left({x}\in {J},{y}\in {ℕ}_{0}⟼{2}^{{y}}{x}\right)$
eulerpart.h ${⊢}{H}=\left\{{r}\in \left({\left(𝒫{ℕ}_{0}\cap \mathrm{Fin}\right)}^{{J}}\right)|{r}\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}$
eulerpart.m ${⊢}{M}=\left({r}\in {H}⟼\left\{⟨{x},{y}⟩|\left({x}\in {J}\wedge {y}\in {r}\left({x}\right)\right)\right\}\right)$
eulerpart.r ${⊢}{R}=\left\{{f}|{{f}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}$
eulerpart.t ${⊢}{T}=\left\{{f}\in \left({{ℕ}_{0}}^{ℕ}\right)|{{f}}^{-1}\left[ℕ\right]\subseteq {J}\right\}$
eulerpart.g ${⊢}{G}=\left({o}\in \left({T}\cap {R}\right)⟼{𝟙}_{ℕ}\left({F}\left[{M}\left(\mathrm{bits}\circ \left({{o}↾}_{{J}}\right)\right)\right]\right)\right)$
eulerpartlemgh.1 ${⊢}{U}=\bigcup _{{t}\in {{A}}^{-1}\left[ℕ\right]\cap {J}}\left(\left\{{t}\right\}×\mathrm{bits}\left({A}\left({t}\right)\right)\right)$
Assertion eulerpartlemgh ${⊢}{A}\in \left({T}\cap {R}\right)\to \left({{F}↾}_{{U}}\right):{U}\underset{1-1 onto}{⟶}\left\{{m}\in ℕ|\exists {t}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={m}\right\}$

### Proof

Step Hyp Ref Expression
1 eulerpart.p ${⊢}{P}=\left\{{f}\in \left({{ℕ}_{0}}^{ℕ}\right)|\left({{f}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\wedge \sum _{{k}\in ℕ}{f}\left({k}\right){k}={N}\right)\right\}$
2 eulerpart.o ${⊢}{O}=\left\{{g}\in {P}|\forall {n}\in {{g}}^{-1}\left[ℕ\right]\phantom{\rule{.4em}{0ex}}¬2\parallel {n}\right\}$
3 eulerpart.d ${⊢}{D}=\left\{{g}\in {P}|\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({n}\right)\le 1\right\}$
4 eulerpart.j ${⊢}{J}=\left\{{z}\in ℕ|¬2\parallel {z}\right\}$
5 eulerpart.f ${⊢}{F}=\left({x}\in {J},{y}\in {ℕ}_{0}⟼{2}^{{y}}{x}\right)$
6 eulerpart.h ${⊢}{H}=\left\{{r}\in \left({\left(𝒫{ℕ}_{0}\cap \mathrm{Fin}\right)}^{{J}}\right)|{r}\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}$
7 eulerpart.m ${⊢}{M}=\left({r}\in {H}⟼\left\{⟨{x},{y}⟩|\left({x}\in {J}\wedge {y}\in {r}\left({x}\right)\right)\right\}\right)$
8 eulerpart.r ${⊢}{R}=\left\{{f}|{{f}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}$
9 eulerpart.t ${⊢}{T}=\left\{{f}\in \left({{ℕ}_{0}}^{ℕ}\right)|{{f}}^{-1}\left[ℕ\right]\subseteq {J}\right\}$
10 eulerpart.g ${⊢}{G}=\left({o}\in \left({T}\cap {R}\right)⟼{𝟙}_{ℕ}\left({F}\left[{M}\left(\mathrm{bits}\circ \left({{o}↾}_{{J}}\right)\right)\right]\right)\right)$
11 eulerpartlemgh.1 ${⊢}{U}=\bigcup _{{t}\in {{A}}^{-1}\left[ℕ\right]\cap {J}}\left(\left\{{t}\right\}×\mathrm{bits}\left({A}\left({t}\right)\right)\right)$
12 4 5 oddpwdc ${⊢}{F}:{J}×{ℕ}_{0}\underset{1-1 onto}{⟶}ℕ$
13 f1of1 ${⊢}{F}:{J}×{ℕ}_{0}\underset{1-1 onto}{⟶}ℕ\to {F}:{J}×{ℕ}_{0}\underset{1-1}{⟶}ℕ$
14 12 13 ax-mp ${⊢}{F}:{J}×{ℕ}_{0}\underset{1-1}{⟶}ℕ$
15 iunss ${⊢}\bigcup _{{t}\in {{A}}^{-1}\left[ℕ\right]\cap {J}}\left(\left\{{t}\right\}×\mathrm{bits}\left({A}\left({t}\right)\right)\right)\subseteq {J}×{ℕ}_{0}↔\forall {t}\in \left({{A}}^{-1}\left[ℕ\right]\cap {J}\right)\phantom{\rule{.4em}{0ex}}\left\{{t}\right\}×\mathrm{bits}\left({A}\left({t}\right)\right)\subseteq {J}×{ℕ}_{0}$
16 inss2 ${⊢}{{A}}^{-1}\left[ℕ\right]\cap {J}\subseteq {J}$
17 16 sseli ${⊢}{t}\in \left({{A}}^{-1}\left[ℕ\right]\cap {J}\right)\to {t}\in {J}$
18 17 snssd ${⊢}{t}\in \left({{A}}^{-1}\left[ℕ\right]\cap {J}\right)\to \left\{{t}\right\}\subseteq {J}$
19 bitsss ${⊢}\mathrm{bits}\left({A}\left({t}\right)\right)\subseteq {ℕ}_{0}$
20 xpss12 ${⊢}\left(\left\{{t}\right\}\subseteq {J}\wedge \mathrm{bits}\left({A}\left({t}\right)\right)\subseteq {ℕ}_{0}\right)\to \left\{{t}\right\}×\mathrm{bits}\left({A}\left({t}\right)\right)\subseteq {J}×{ℕ}_{0}$
21 18 19 20 sylancl ${⊢}{t}\in \left({{A}}^{-1}\left[ℕ\right]\cap {J}\right)\to \left\{{t}\right\}×\mathrm{bits}\left({A}\left({t}\right)\right)\subseteq {J}×{ℕ}_{0}$
22 15 21 mprgbir ${⊢}\bigcup _{{t}\in {{A}}^{-1}\left[ℕ\right]\cap {J}}\left(\left\{{t}\right\}×\mathrm{bits}\left({A}\left({t}\right)\right)\right)\subseteq {J}×{ℕ}_{0}$
23 11 22 eqsstri ${⊢}{U}\subseteq {J}×{ℕ}_{0}$
24 f1ores ${⊢}\left({F}:{J}×{ℕ}_{0}\underset{1-1}{⟶}ℕ\wedge {U}\subseteq {J}×{ℕ}_{0}\right)\to \left({{F}↾}_{{U}}\right):{U}\underset{1-1 onto}{⟶}{F}\left[{U}\right]$
25 14 23 24 mp2an ${⊢}\left({{F}↾}_{{U}}\right):{U}\underset{1-1 onto}{⟶}{F}\left[{U}\right]$
26 simpr ${⊢}\left(\left(\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\wedge {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\right)\wedge {2}^{{n}}{t}={p}\right)\to {2}^{{n}}{t}={p}$
27 2nn ${⊢}2\in ℕ$
28 27 a1i ${⊢}\left(\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\wedge {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\right)\to 2\in ℕ$
29 19 sseli ${⊢}{n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\to {n}\in {ℕ}_{0}$
30 29 adantl ${⊢}\left(\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\wedge {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\right)\to {n}\in {ℕ}_{0}$
31 28 30 nnexpcld ${⊢}\left(\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\wedge {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\right)\to {2}^{{n}}\in ℕ$
32 simplr ${⊢}\left(\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\wedge {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\right)\to {t}\in ℕ$
33 31 32 nnmulcld ${⊢}\left(\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\wedge {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\right)\to {2}^{{n}}{t}\in ℕ$
34 33 adantr ${⊢}\left(\left(\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\wedge {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\right)\wedge {2}^{{n}}{t}={p}\right)\to {2}^{{n}}{t}\in ℕ$
35 26 34 eqeltrrd ${⊢}\left(\left(\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\wedge {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\right)\wedge {2}^{{n}}{t}={p}\right)\to {p}\in ℕ$
36 35 rexlimdva2 ${⊢}\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\to \left(\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\to {p}\in ℕ\right)$
37 36 rexlimdva ${⊢}{A}\in \left({T}\cap {R}\right)\to \left(\exists {t}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\to {p}\in ℕ\right)$
38 37 pm4.71rd ${⊢}{A}\in \left({T}\cap {R}\right)\to \left(\exists {t}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}↔\left({p}\in ℕ\wedge \exists {t}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\right)\right)$
39 rex0 ${⊢}¬\exists {n}\in \varnothing \phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}$
40 simplr ${⊢}\left(\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\wedge ¬{t}\in {{A}}^{-1}\left[ℕ\right]\right)\to {t}\in ℕ$
41 simpr ${⊢}\left(\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\wedge ¬{t}\in {{A}}^{-1}\left[ℕ\right]\right)\to ¬{t}\in {{A}}^{-1}\left[ℕ\right]$
42 1 2 3 4 5 6 7 8 9 eulerpartlemt0 ${⊢}{A}\in \left({T}\cap {R}\right)↔\left({A}\in \left({{ℕ}_{0}}^{ℕ}\right)\wedge {{A}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\wedge {{A}}^{-1}\left[ℕ\right]\subseteq {J}\right)$
43 42 simp1bi ${⊢}{A}\in \left({T}\cap {R}\right)\to {A}\in \left({{ℕ}_{0}}^{ℕ}\right)$
44 elmapi ${⊢}{A}\in \left({{ℕ}_{0}}^{ℕ}\right)\to {A}:ℕ⟶{ℕ}_{0}$
45 43 44 syl ${⊢}{A}\in \left({T}\cap {R}\right)\to {A}:ℕ⟶{ℕ}_{0}$
46 45 ad2antrr ${⊢}\left(\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\wedge ¬{t}\in {{A}}^{-1}\left[ℕ\right]\right)\to {A}:ℕ⟶{ℕ}_{0}$
47 ffn ${⊢}{A}:ℕ⟶{ℕ}_{0}\to {A}Fnℕ$
48 elpreima ${⊢}{A}Fnℕ\to \left({t}\in {{A}}^{-1}\left[ℕ\right]↔\left({t}\in ℕ\wedge {A}\left({t}\right)\in ℕ\right)\right)$
49 46 47 48 3syl ${⊢}\left(\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\wedge ¬{t}\in {{A}}^{-1}\left[ℕ\right]\right)\to \left({t}\in {{A}}^{-1}\left[ℕ\right]↔\left({t}\in ℕ\wedge {A}\left({t}\right)\in ℕ\right)\right)$
50 41 49 mtbid ${⊢}\left(\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\wedge ¬{t}\in {{A}}^{-1}\left[ℕ\right]\right)\to ¬\left({t}\in ℕ\wedge {A}\left({t}\right)\in ℕ\right)$
51 imnan ${⊢}\left({t}\in ℕ\to ¬{A}\left({t}\right)\in ℕ\right)↔¬\left({t}\in ℕ\wedge {A}\left({t}\right)\in ℕ\right)$
52 50 51 sylibr ${⊢}\left(\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\wedge ¬{t}\in {{A}}^{-1}\left[ℕ\right]\right)\to \left({t}\in ℕ\to ¬{A}\left({t}\right)\in ℕ\right)$
53 40 52 mpd ${⊢}\left(\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\wedge ¬{t}\in {{A}}^{-1}\left[ℕ\right]\right)\to ¬{A}\left({t}\right)\in ℕ$
54 46 40 ffvelrnd ${⊢}\left(\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\wedge ¬{t}\in {{A}}^{-1}\left[ℕ\right]\right)\to {A}\left({t}\right)\in {ℕ}_{0}$
55 elnn0 ${⊢}{A}\left({t}\right)\in {ℕ}_{0}↔\left({A}\left({t}\right)\in ℕ\vee {A}\left({t}\right)=0\right)$
56 54 55 sylib ${⊢}\left(\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\wedge ¬{t}\in {{A}}^{-1}\left[ℕ\right]\right)\to \left({A}\left({t}\right)\in ℕ\vee {A}\left({t}\right)=0\right)$
57 orel1 ${⊢}¬{A}\left({t}\right)\in ℕ\to \left(\left({A}\left({t}\right)\in ℕ\vee {A}\left({t}\right)=0\right)\to {A}\left({t}\right)=0\right)$
58 53 56 57 sylc ${⊢}\left(\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\wedge ¬{t}\in {{A}}^{-1}\left[ℕ\right]\right)\to {A}\left({t}\right)=0$
59 58 fveq2d ${⊢}\left(\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\wedge ¬{t}\in {{A}}^{-1}\left[ℕ\right]\right)\to \mathrm{bits}\left({A}\left({t}\right)\right)=\mathrm{bits}\left(0\right)$
60 0bits ${⊢}\mathrm{bits}\left(0\right)=\varnothing$
61 59 60 syl6eq ${⊢}\left(\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\wedge ¬{t}\in {{A}}^{-1}\left[ℕ\right]\right)\to \mathrm{bits}\left({A}\left({t}\right)\right)=\varnothing$
62 61 rexeqdv ${⊢}\left(\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\wedge ¬{t}\in {{A}}^{-1}\left[ℕ\right]\right)\to \left(\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}↔\exists {n}\in \varnothing \phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\right)$
63 39 62 mtbiri ${⊢}\left(\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\wedge ¬{t}\in {{A}}^{-1}\left[ℕ\right]\right)\to ¬\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}$
64 63 ex ${⊢}\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\to \left(¬{t}\in {{A}}^{-1}\left[ℕ\right]\to ¬\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\right)$
65 64 con4d ${⊢}\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\to \left(\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\to {t}\in {{A}}^{-1}\left[ℕ\right]\right)$
66 65 impr ${⊢}\left({A}\in \left({T}\cap {R}\right)\wedge \left({t}\in ℕ\wedge \exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\right)\right)\to {t}\in {{A}}^{-1}\left[ℕ\right]$
67 eldif ${⊢}{t}\in \left(ℕ\setminus {J}\right)↔\left({t}\in ℕ\wedge ¬{t}\in {J}\right)$
68 1 2 3 4 5 6 7 8 9 eulerpartlemf ${⊢}\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in \left(ℕ\setminus {J}\right)\right)\to {A}\left({t}\right)=0$
69 67 68 sylan2br ${⊢}\left({A}\in \left({T}\cap {R}\right)\wedge \left({t}\in ℕ\wedge ¬{t}\in {J}\right)\right)\to {A}\left({t}\right)=0$
70 69 anassrs ${⊢}\left(\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\wedge ¬{t}\in {J}\right)\to {A}\left({t}\right)=0$
71 70 fveq2d ${⊢}\left(\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\wedge ¬{t}\in {J}\right)\to \mathrm{bits}\left({A}\left({t}\right)\right)=\mathrm{bits}\left(0\right)$
72 71 60 syl6eq ${⊢}\left(\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\wedge ¬{t}\in {J}\right)\to \mathrm{bits}\left({A}\left({t}\right)\right)=\varnothing$
73 72 rexeqdv ${⊢}\left(\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\wedge ¬{t}\in {J}\right)\to \left(\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}↔\exists {n}\in \varnothing \phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\right)$
74 39 73 mtbiri ${⊢}\left(\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\wedge ¬{t}\in {J}\right)\to ¬\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}$
75 74 ex ${⊢}\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\to \left(¬{t}\in {J}\to ¬\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\right)$
76 75 con4d ${⊢}\left({A}\in \left({T}\cap {R}\right)\wedge {t}\in ℕ\right)\to \left(\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\to {t}\in {J}\right)$
77 76 impr ${⊢}\left({A}\in \left({T}\cap {R}\right)\wedge \left({t}\in ℕ\wedge \exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\right)\right)\to {t}\in {J}$
78 66 77 elind ${⊢}\left({A}\in \left({T}\cap {R}\right)\wedge \left({t}\in ℕ\wedge \exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\right)\right)\to {t}\in \left({{A}}^{-1}\left[ℕ\right]\cap {J}\right)$
79 simprr ${⊢}\left({A}\in \left({T}\cap {R}\right)\wedge \left({t}\in ℕ\wedge \exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\right)\right)\to \exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}$
80 78 79 jca ${⊢}\left({A}\in \left({T}\cap {R}\right)\wedge \left({t}\in ℕ\wedge \exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\right)\right)\to \left({t}\in \left({{A}}^{-1}\left[ℕ\right]\cap {J}\right)\wedge \exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\right)$
81 80 ex ${⊢}{A}\in \left({T}\cap {R}\right)\to \left(\left({t}\in ℕ\wedge \exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\right)\to \left({t}\in \left({{A}}^{-1}\left[ℕ\right]\cap {J}\right)\wedge \exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\right)\right)$
82 81 reximdv2 ${⊢}{A}\in \left({T}\cap {R}\right)\to \left(\exists {t}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\to \exists {t}\in \left({{A}}^{-1}\left[ℕ\right]\cap {J}\right)\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\right)$
83 ssrab2 ${⊢}\left\{{z}\in ℕ|¬2\parallel {z}\right\}\subseteq ℕ$
84 4 83 eqsstri ${⊢}{J}\subseteq ℕ$
85 16 84 sstri ${⊢}{{A}}^{-1}\left[ℕ\right]\cap {J}\subseteq ℕ$
86 ssrexv ${⊢}{{A}}^{-1}\left[ℕ\right]\cap {J}\subseteq ℕ\to \left(\exists {t}\in \left({{A}}^{-1}\left[ℕ\right]\cap {J}\right)\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\to \exists {t}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\right)$
87 85 86 mp1i ${⊢}{A}\in \left({T}\cap {R}\right)\to \left(\exists {t}\in \left({{A}}^{-1}\left[ℕ\right]\cap {J}\right)\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\to \exists {t}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\right)$
88 82 87 impbid ${⊢}{A}\in \left({T}\cap {R}\right)\to \left(\exists {t}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}↔\exists {t}\in \left({{A}}^{-1}\left[ℕ\right]\cap {J}\right)\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\right)$
89 38 88 bitr3d ${⊢}{A}\in \left({T}\cap {R}\right)\to \left(\left({p}\in ℕ\wedge \exists {t}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\right)↔\exists {t}\in \left({{A}}^{-1}\left[ℕ\right]\cap {J}\right)\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\right)$
90 eqeq2 ${⊢}{m}={p}\to \left({2}^{{n}}{t}={m}↔{2}^{{n}}{t}={p}\right)$
91 90 2rexbidv ${⊢}{m}={p}\to \left(\exists {t}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={m}↔\exists {t}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\right)$
92 91 elrab ${⊢}{p}\in \left\{{m}\in ℕ|\exists {t}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={m}\right\}↔\left({p}\in ℕ\wedge \exists {t}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\right)$
93 92 a1i ${⊢}{A}\in \left({T}\cap {R}\right)\to \left({p}\in \left\{{m}\in ℕ|\exists {t}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={m}\right\}↔\left({p}\in ℕ\wedge \exists {t}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\right)\right)$
94 11 imaeq2i ${⊢}{F}\left[{U}\right]={F}\left[\bigcup _{{t}\in {{A}}^{-1}\left[ℕ\right]\cap {J}}\left(\left\{{t}\right\}×\mathrm{bits}\left({A}\left({t}\right)\right)\right)\right]$
95 imaiun ${⊢}{F}\left[\bigcup _{{t}\in {{A}}^{-1}\left[ℕ\right]\cap {J}}\left(\left\{{t}\right\}×\mathrm{bits}\left({A}\left({t}\right)\right)\right)\right]=\bigcup _{{t}\in {{A}}^{-1}\left[ℕ\right]\cap {J}}{F}\left[\left\{{t}\right\}×\mathrm{bits}\left({A}\left({t}\right)\right)\right]$
96 94 95 eqtri ${⊢}{F}\left[{U}\right]=\bigcup _{{t}\in {{A}}^{-1}\left[ℕ\right]\cap {J}}{F}\left[\left\{{t}\right\}×\mathrm{bits}\left({A}\left({t}\right)\right)\right]$
97 96 eleq2i ${⊢}{p}\in {F}\left[{U}\right]↔{p}\in \bigcup _{{t}\in {{A}}^{-1}\left[ℕ\right]\cap {J}}{F}\left[\left\{{t}\right\}×\mathrm{bits}\left({A}\left({t}\right)\right)\right]$
98 eliun ${⊢}{p}\in \bigcup _{{t}\in {{A}}^{-1}\left[ℕ\right]\cap {J}}{F}\left[\left\{{t}\right\}×\mathrm{bits}\left({A}\left({t}\right)\right)\right]↔\exists {t}\in \left({{A}}^{-1}\left[ℕ\right]\cap {J}\right)\phantom{\rule{.4em}{0ex}}{p}\in {F}\left[\left\{{t}\right\}×\mathrm{bits}\left({A}\left({t}\right)\right)\right]$
99 f1ofn ${⊢}{F}:{J}×{ℕ}_{0}\underset{1-1 onto}{⟶}ℕ\to {F}Fn\left({J}×{ℕ}_{0}\right)$
100 12 99 ax-mp ${⊢}{F}Fn\left({J}×{ℕ}_{0}\right)$
101 snssi ${⊢}{t}\in {J}\to \left\{{t}\right\}\subseteq {J}$
102 101 19 20 sylancl ${⊢}{t}\in {J}\to \left\{{t}\right\}×\mathrm{bits}\left({A}\left({t}\right)\right)\subseteq {J}×{ℕ}_{0}$
103 ovelimab ${⊢}\left({F}Fn\left({J}×{ℕ}_{0}\right)\wedge \left\{{t}\right\}×\mathrm{bits}\left({A}\left({t}\right)\right)\subseteq {J}×{ℕ}_{0}\right)\to \left({p}\in {F}\left[\left\{{t}\right\}×\mathrm{bits}\left({A}\left({t}\right)\right)\right]↔\exists {x}\in \left\{{t}\right\}\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{p}={x}{F}{n}\right)$
104 100 102 103 sylancr ${⊢}{t}\in {J}\to \left({p}\in {F}\left[\left\{{t}\right\}×\mathrm{bits}\left({A}\left({t}\right)\right)\right]↔\exists {x}\in \left\{{t}\right\}\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{p}={x}{F}{n}\right)$
105 vex ${⊢}{t}\in \mathrm{V}$
106 oveq1 ${⊢}{x}={t}\to {x}{F}{n}={t}{F}{n}$
107 106 eqeq2d ${⊢}{x}={t}\to \left({p}={x}{F}{n}↔{p}={t}{F}{n}\right)$
108 107 rexbidv ${⊢}{x}={t}\to \left(\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{p}={x}{F}{n}↔\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{p}={t}{F}{n}\right)$
109 105 108 rexsn ${⊢}\exists {x}\in \left\{{t}\right\}\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{p}={x}{F}{n}↔\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{p}={t}{F}{n}$
110 104 109 syl6bb ${⊢}{t}\in {J}\to \left({p}\in {F}\left[\left\{{t}\right\}×\mathrm{bits}\left({A}\left({t}\right)\right)\right]↔\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{p}={t}{F}{n}\right)$
111 df-ov ${⊢}{t}{F}{n}={F}\left(⟨{t},{n}⟩\right)$
112 111 eqeq1i ${⊢}{t}{F}{n}={p}↔{F}\left(⟨{t},{n}⟩\right)={p}$
113 eqcom ${⊢}{t}{F}{n}={p}↔{p}={t}{F}{n}$
114 112 113 bitr3i ${⊢}{F}\left(⟨{t},{n}⟩\right)={p}↔{p}={t}{F}{n}$
115 opelxpi ${⊢}\left({t}\in {J}\wedge {n}\in {ℕ}_{0}\right)\to ⟨{t},{n}⟩\in \left({J}×{ℕ}_{0}\right)$
116 4 5 oddpwdcv ${⊢}⟨{t},{n}⟩\in \left({J}×{ℕ}_{0}\right)\to {F}\left(⟨{t},{n}⟩\right)={2}^{{2}^{nd}\left(⟨{t},{n}⟩\right)}{1}^{st}\left(⟨{t},{n}⟩\right)$
117 vex ${⊢}{n}\in \mathrm{V}$
118 105 117 op2nd ${⊢}{2}^{nd}\left(⟨{t},{n}⟩\right)={n}$
119 118 oveq2i ${⊢}{2}^{{2}^{nd}\left(⟨{t},{n}⟩\right)}={2}^{{n}}$
120 105 117 op1st ${⊢}{1}^{st}\left(⟨{t},{n}⟩\right)={t}$
121 119 120 oveq12i ${⊢}{2}^{{2}^{nd}\left(⟨{t},{n}⟩\right)}{1}^{st}\left(⟨{t},{n}⟩\right)={2}^{{n}}{t}$
122 116 121 syl6eq ${⊢}⟨{t},{n}⟩\in \left({J}×{ℕ}_{0}\right)\to {F}\left(⟨{t},{n}⟩\right)={2}^{{n}}{t}$
123 115 122 syl ${⊢}\left({t}\in {J}\wedge {n}\in {ℕ}_{0}\right)\to {F}\left(⟨{t},{n}⟩\right)={2}^{{n}}{t}$
124 123 eqeq1d ${⊢}\left({t}\in {J}\wedge {n}\in {ℕ}_{0}\right)\to \left({F}\left(⟨{t},{n}⟩\right)={p}↔{2}^{{n}}{t}={p}\right)$
125 114 124 syl5bbr ${⊢}\left({t}\in {J}\wedge {n}\in {ℕ}_{0}\right)\to \left({p}={t}{F}{n}↔{2}^{{n}}{t}={p}\right)$
126 29 125 sylan2 ${⊢}\left({t}\in {J}\wedge {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\right)\to \left({p}={t}{F}{n}↔{2}^{{n}}{t}={p}\right)$
127 126 rexbidva ${⊢}{t}\in {J}\to \left(\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{p}={t}{F}{n}↔\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\right)$
128 110 127 bitrd ${⊢}{t}\in {J}\to \left({p}\in {F}\left[\left\{{t}\right\}×\mathrm{bits}\left({A}\left({t}\right)\right)\right]↔\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\right)$
129 17 128 syl ${⊢}{t}\in \left({{A}}^{-1}\left[ℕ\right]\cap {J}\right)\to \left({p}\in {F}\left[\left\{{t}\right\}×\mathrm{bits}\left({A}\left({t}\right)\right)\right]↔\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\right)$
130 129 rexbiia ${⊢}\exists {t}\in \left({{A}}^{-1}\left[ℕ\right]\cap {J}\right)\phantom{\rule{.4em}{0ex}}{p}\in {F}\left[\left\{{t}\right\}×\mathrm{bits}\left({A}\left({t}\right)\right)\right]↔\exists {t}\in \left({{A}}^{-1}\left[ℕ\right]\cap {J}\right)\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}$
131 97 98 130 3bitri ${⊢}{p}\in {F}\left[{U}\right]↔\exists {t}\in \left({{A}}^{-1}\left[ℕ\right]\cap {J}\right)\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}$
132 131 a1i ${⊢}{A}\in \left({T}\cap {R}\right)\to \left({p}\in {F}\left[{U}\right]↔\exists {t}\in \left({{A}}^{-1}\left[ℕ\right]\cap {J}\right)\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={p}\right)$
133 89 93 132 3bitr4rd ${⊢}{A}\in \left({T}\cap {R}\right)\to \left({p}\in {F}\left[{U}\right]↔{p}\in \left\{{m}\in ℕ|\exists {t}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={m}\right\}\right)$
134 133 eqrdv ${⊢}{A}\in \left({T}\cap {R}\right)\to {F}\left[{U}\right]=\left\{{m}\in ℕ|\exists {t}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={m}\right\}$
135 f1oeq3 ${⊢}{F}\left[{U}\right]=\left\{{m}\in ℕ|\exists {t}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={m}\right\}\to \left(\left({{F}↾}_{{U}}\right):{U}\underset{1-1 onto}{⟶}{F}\left[{U}\right]↔\left({{F}↾}_{{U}}\right):{U}\underset{1-1 onto}{⟶}\left\{{m}\in ℕ|\exists {t}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={m}\right\}\right)$
136 134 135 syl ${⊢}{A}\in \left({T}\cap {R}\right)\to \left(\left({{F}↾}_{{U}}\right):{U}\underset{1-1 onto}{⟶}{F}\left[{U}\right]↔\left({{F}↾}_{{U}}\right):{U}\underset{1-1 onto}{⟶}\left\{{m}\in ℕ|\exists {t}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={m}\right\}\right)$
137 25 136 mpbii ${⊢}{A}\in \left({T}\cap {R}\right)\to \left({{F}↾}_{{U}}\right):{U}\underset{1-1 onto}{⟶}\left\{{m}\in ℕ|\exists {t}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {n}\in \mathrm{bits}\left({A}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}{2}^{{n}}{t}={m}\right\}$