Theorem eulerpart

Description: Euler's theorem on partitions, also known as a special case of Glaisher's theorem. Let P be the set of all partitions of N , represented as multisets of positive integers, which is to say functions from NN to NN0 where the value of the function represents the number of repetitions of an individual element, and the sum of all the elements with repetition equals N . Then the set O of all partitions that only consist of odd numbers and the set D of all partitions which have no repeated elements have the same cardinality. This is Metamath 100 proof #45. (Contributed by Thierry Arnoux, 14-Aug-2018) (Revised by Thierry Arnoux, 1-Sep-2019)

	Ref	Expression
Hypotheses	eulerpart.p	$$⊢P=\left\{f\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)|\left(f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\wedge \sum _{k\in \mathbb{N}}f\left(k\right)k=N\right)\right\}$$
	eulerpart.o	$$⊢O=\left\{g\in P|\forall n\in g^{-1}\left[\mathbb{N}\right]\neg 2\parallel n\right\}$$
	eulerpart.d	$$⊢D=\left\{g\in P|\forall n\in \mathbb{N}g\left(n\right)\le 1\right\}$$
Assertion	eulerpart	$$⊢\left|O\right|=\left|D\right|$$

Proof

Step	Hyp	Ref	Expression
1		eulerpart.p	$$⊢P=\left\{f\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)|\left(f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\wedge \sum _{k\in \mathbb{N}}f\left(k\right)k=N\right)\right\}$$
2		eulerpart.o	$$⊢O=\left\{g\in P|\forall n\in g^{-1}\left[\mathbb{N}\right]\neg 2\parallel n\right\}$$
3		eulerpart.d	$$⊢D=\left\{g\in P|\forall n\in \mathbb{N}g\left(n\right)\le 1\right\}$$
4		eqid	$$⊢\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}=\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}$$
5		oveq2	$$⊢a=x\to 2^{b}a=2^{b}x$$
6		oveq2	$$⊢b=y\to 2^b=2^y$$
7	6	oveq1d	$$⊢b=y\to 2^{b}x=2^{y}x$$
8	5 7	cbvmpov	$$⊢\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\},b\in {\mathbb{N}}_0⟼2^{b}a\right)=\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\},y\in {\mathbb{N}}_0⟼2^{y}x\right)$$
9		oveq1	$$⊢r=m\to r\mathrm{supp}\varnothing =m\mathrm{supp}\varnothing$$
10	9	eleq1d	$$⊢r=m\to \left(r\mathrm{supp}\varnothing \in \mathrm{Fin}\leftrightarrow m\mathrm{supp}\varnothing \in \mathrm{Fin}\right)$$
11	10	cbvrabv	$$⊢\left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}=\left\{m\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|m\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}$$
12	11	eqcomi	$$⊢\left\{m\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|m\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}=\left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}$$
13		fveq1	$$⊢t=r\to t\left(a\right)=r\left(a\right)$$
14	13	eleq2d	$$⊢t=r\to \left(b\in t\left(a\right)\leftrightarrow b\in r\left(a\right)\right)$$
15	14	anbi2d	$$⊢t=r\to \left(\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge b\in t\left(a\right)\right)\leftrightarrow \left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge b\in r\left(a\right)\right)\right)$$
16	15	opabbidv	$$⊢t=r\to \left\{⟨a,b⟩|\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge b\in t\left(a\right)\right)\right\}=\left\{⟨a,b⟩|\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge b\in r\left(a\right)\right)\right\}$$
17	16	cbvmptv	$$⊢\left(t\in \left\{s\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|s\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨a,b⟩|\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge b\in t\left(a\right)\right)\right\}\right)=\left(r\in \left\{s\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|s\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨a,b⟩|\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge b\in r\left(a\right)\right)\right\}\right)$$
18		oveq1	$$⊢m=s\to m\mathrm{supp}\varnothing =s\mathrm{supp}\varnothing$$
19	18	eleq1d	$$⊢m=s\to \left(m\mathrm{supp}\varnothing \in \mathrm{Fin}\leftrightarrow s\mathrm{supp}\varnothing \in \mathrm{Fin}\right)$$
20	19	cbvrabv	$$⊢\left\{m\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|m\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}=\left\{s\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|s\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}$$
21	20	eqcomi	$$⊢\left\{s\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|s\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}=\left\{m\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|m\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}$$
22		simpl	$$⊢\left(a=x\wedge b=y\right)\to a=x$$
23	22	eleq1d	$$⊢\left(a=x\wedge b=y\right)\to \left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\leftrightarrow x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\right)$$
24		simpr	$$⊢\left(a=x\wedge b=y\right)\to b=y$$
25	22	fveq2d	$$⊢\left(a=x\wedge b=y\right)\to r\left(a\right)=r\left(x\right)$$
26	24 25	eleq12d	$$⊢\left(a=x\wedge b=y\right)\to \left(b\in r\left(a\right)\leftrightarrow y\in r\left(x\right)\right)$$
27	23 26	anbi12d	$$⊢\left(a=x\wedge b=y\right)\to \left(\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge b\in r\left(a\right)\right)\leftrightarrow \left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right)$$
28	27	cbvopabv	$$⊢\left\{⟨a,b⟩|\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge b\in r\left(a\right)\right)\right\}=\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}$$
29	21 28	mpteq12i	$$⊢\left(r\in \left\{s\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|s\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨a,b⟩|\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge b\in r\left(a\right)\right)\right\}\right)=\left(r\in \left\{m\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|m\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}\right)$$
30	17 29	eqtri	$$⊢\left(t\in \left\{s\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|s\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨a,b⟩|\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge b\in t\left(a\right)\right)\right\}\right)=\left(r\in \left\{m\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|m\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}\right)$$
31		cnveq	$$⊢h=f\to h^{-1}=f^{-1}$$
32	31	imaeq1d	$$⊢h=f\to h^{-1}\left[\mathbb{N}\right]=f^{-1}\left[\mathbb{N}\right]$$
33	32	eleq1d	$$⊢h=f\to \left(h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\leftrightarrow f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
34	33	cbvabv	$$⊢\left\{h|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{f|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
35	32	sseq1d	$$⊢h=f\to \left(h^{-1}\left[\mathbb{N}\right]\subseteq \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\leftrightarrow f^{-1}\left[\mathbb{N}\right]\subseteq \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\right)$$
36	35	cbvrabv	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)|h^{-1}\left[\mathbb{N}\right]\subseteq \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\right\}=\left\{f\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)|f^{-1}\left[\mathbb{N}\right]\subseteq \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\right\}$$
37		reseq1	$$⊢o=q\to {o\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}={q\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}$$
38	37	coeq2d	$$⊢o=q\to \mathrm{bits}\circ \left({o\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)=\mathrm{bits}\circ \left({q\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)$$
39	38	fveq2d	$$⊢o=q\to \left(r\in \left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}\right)\left(\mathrm{bits}\circ \left({o\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)\right)=\left(r\in \left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}\right)\left(\mathrm{bits}\circ \left({q\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)\right)$$
40	39	imaeq2d	$$⊢o=q\to \left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\},y\in {\mathbb{N}}_0⟼2^{y}x\right)\left[\left(r\in \left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}\right)\left(\mathrm{bits}\circ \left({o\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)\right)\right]=\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\},y\in {\mathbb{N}}_0⟼2^{y}x\right)\left[\left(r\in \left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}\right)\left(\mathrm{bits}\circ \left({q\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)\right)\right]$$
41	40	fveq2d	$$⊢o=q\to {𝟙}_{\mathbb{N}}\left(\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\},y\in {\mathbb{N}}_0⟼2^{y}x\right)\left[\left(r\in \left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}\right)\left(\mathrm{bits}\circ \left({o\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)\right)\right]\right)={𝟙}_{\mathbb{N}}\left(\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\},y\in {\mathbb{N}}_0⟼2^{y}x\right)\left[\left(r\in \left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}\right)\left(\mathrm{bits}\circ \left({q\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)\right)\right]\right)$$
42	41	cbvmptv	$$⊢\left(o\in \left(\left\{h\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)|h^{-1}\left[\mathbb{N}\right]\subseteq \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\right\}\cap \left\{h|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)⟼{𝟙}_{\mathbb{N}}\left(\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\},y\in {\mathbb{N}}_0⟼2^{y}x\right)\left[\left(r\in \left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}\right)\left(\mathrm{bits}\circ \left({o\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)\right)\right]\right)\right)=\left(q\in \left(\left\{h\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)|h^{-1}\left[\mathbb{N}\right]\subseteq \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\right\}\cap \left\{h|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)⟼{𝟙}_{\mathbb{N}}\left(\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\},y\in {\mathbb{N}}_0⟼2^{y}x\right)\left[\left(r\in \left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}\right)\left(\mathrm{bits}\circ \left({q\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)\right)\right]\right)\right)$$
43	8	eqcomi	$$⊢\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\},y\in {\mathbb{N}}_0⟼2^{y}x\right)=\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\},b\in {\mathbb{N}}_0⟼2^{b}a\right)$$
44	43	imaeq1i	$$⊢\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\},y\in {\mathbb{N}}_0⟼2^{y}x\right)\left[\left(r\in \left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}\right)\left(\mathrm{bits}\circ \left({q\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)\right)\right]=\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\},b\in {\mathbb{N}}_0⟼2^{b}a\right)\left[\left(r\in \left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}\right)\left(\mathrm{bits}\circ \left({q\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)\right)\right]$$
45		eqid	$$⊢\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}=\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}$$
46	11 45	mpteq12i	$$⊢\left(r\in \left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}\right)=\left(r\in \left\{m\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|m\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}\right)$$
47		fveq1	$$⊢r=t\to r\left(a\right)=t\left(a\right)$$
48	47	eleq2d	$$⊢r=t\to \left(b\in r\left(a\right)\leftrightarrow b\in t\left(a\right)\right)$$
49	48	anbi2d	$$⊢r=t\to \left(\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge b\in r\left(a\right)\right)\leftrightarrow \left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge b\in t\left(a\right)\right)\right)$$
50	49	opabbidv	$$⊢r=t\to \left\{⟨a,b⟩|\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge b\in r\left(a\right)\right)\right\}=\left\{⟨a,b⟩|\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge b\in t\left(a\right)\right)\right\}$$
51	50	cbvmptv	$$⊢\left(r\in \left\{s\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|s\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨a,b⟩|\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge b\in r\left(a\right)\right)\right\}\right)=\left(t\in \left\{s\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|s\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨a,b⟩|\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge b\in t\left(a\right)\right)\right\}\right)$$
52	46 29 51	3eqtr2i	$$⊢\left(r\in \left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}\right)=\left(t\in \left\{s\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|s\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨a,b⟩|\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge b\in t\left(a\right)\right)\right\}\right)$$
53	52	fveq1i	$$⊢\left(r\in \left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}\right)\left(\mathrm{bits}\circ \left({q\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)\right)=\left(t\in \left\{s\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|s\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨a,b⟩|\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge b\in t\left(a\right)\right)\right\}\right)\left(\mathrm{bits}\circ \left({q\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)\right)$$
54	53	imaeq2i	$$⊢\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\},b\in {\mathbb{N}}_0⟼2^{b}a\right)\left[\left(r\in \left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}\right)\left(\mathrm{bits}\circ \left({q\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)\right)\right]=\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\},b\in {\mathbb{N}}_0⟼2^{b}a\right)\left[\left(t\in \left\{s\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|s\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨a,b⟩|\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge b\in t\left(a\right)\right)\right\}\right)\left(\mathrm{bits}\circ \left({q\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)\right)\right]$$
55	44 54	eqtri	$$⊢\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\},y\in {\mathbb{N}}_0⟼2^{y}x\right)\left[\left(r\in \left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}\right)\left(\mathrm{bits}\circ \left({q\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)\right)\right]=\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\},b\in {\mathbb{N}}_0⟼2^{b}a\right)\left[\left(t\in \left\{s\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|s\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨a,b⟩|\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge b\in t\left(a\right)\right)\right\}\right)\left(\mathrm{bits}\circ \left({q\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)\right)\right]$$
56	55	fveq2i	$$⊢{𝟙}_{\mathbb{N}}\left(\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\},y\in {\mathbb{N}}_0⟼2^{y}x\right)\left[\left(r\in \left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}\right)\left(\mathrm{bits}\circ \left({q\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)\right)\right]\right)={𝟙}_{\mathbb{N}}\left(\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\},b\in {\mathbb{N}}_0⟼2^{b}a\right)\left[\left(t\in \left\{s\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|s\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨a,b⟩|\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge b\in t\left(a\right)\right)\right\}\right)\left(\mathrm{bits}\circ \left({q\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)\right)\right]\right)$$
57	56	mpteq2i	$$⊢\left(q\in \left(\left\{h\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)|h^{-1}\left[\mathbb{N}\right]\subseteq \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\right\}\cap \left\{h|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)⟼{𝟙}_{\mathbb{N}}\left(\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\},y\in {\mathbb{N}}_0⟼2^{y}x\right)\left[\left(r\in \left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}\right)\left(\mathrm{bits}\circ \left({q\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)\right)\right]\right)\right)=\left(q\in \left(\left\{h\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)|h^{-1}\left[\mathbb{N}\right]\subseteq \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\right\}\cap \left\{h|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)⟼{𝟙}_{\mathbb{N}}\left(\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\},b\in {\mathbb{N}}_0⟼2^{b}a\right)\left[\left(t\in \left\{s\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|s\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨a,b⟩|\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge b\in t\left(a\right)\right)\right\}\right)\left(\mathrm{bits}\circ \left({q\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)\right)\right]\right)\right)$$
58	42 57	eqtri	$$⊢\left(o\in \left(\left\{h\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)|h^{-1}\left[\mathbb{N}\right]\subseteq \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\right\}\cap \left\{h|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)⟼{𝟙}_{\mathbb{N}}\left(\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\},y\in {\mathbb{N}}_0⟼2^{y}x\right)\left[\left(r\in \left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}\right)\left(\mathrm{bits}\circ \left({o\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)\right)\right]\right)\right)=\left(q\in \left(\left\{h\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)|h^{-1}\left[\mathbb{N}\right]\subseteq \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\right\}\cap \left\{h|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)⟼{𝟙}_{\mathbb{N}}\left(\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\},b\in {\mathbb{N}}_0⟼2^{b}a\right)\left[\left(t\in \left\{s\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|s\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨a,b⟩|\left(a\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge b\in t\left(a\right)\right)\right\}\right)\left(\mathrm{bits}\circ \left({q\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)\right)\right]\right)\right)$$
59		eqid	$$⊢\left(f\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap \left\{h|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)⟼\sum _{k\in \mathbb{N}}f\left(k\right)k\right)=\left(f\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap \left\{h|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)⟼\sum _{k\in \mathbb{N}}f\left(k\right)k\right)$$
60	1 2 3 4 8 12 30 34 36 58 59	eulerpartlemn	$$⊢\left({\left(o\in \left(\left\{h\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)|h^{-1}\left[\mathbb{N}\right]\subseteq \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\right\}\cap \left\{h|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)⟼{𝟙}_{\mathbb{N}}\left(\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\},y\in {\mathbb{N}}_0⟼2^{y}x\right)\left[\left(r\in \left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}\right)\left(\mathrm{bits}\circ \left({o\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)\right)\right]\right)\right)\upharpoonright }_O\right):O\underset{1-1\; onto}{⟶}D$$
61		ovex	$$⊢{{\mathbb{N}}_0}^{\mathbb{N}}\in \mathrm{V}$$
62	61	rabex	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)|h^{-1}\left[\mathbb{N}\right]\subseteq \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\right\}\in \mathrm{V}$$
63	62	inex1	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)|h^{-1}\left[\mathbb{N}\right]\subseteq \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\right\}\cap \left\{h|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
64	63	mptex	$$⊢\left(o\in \left(\left\{h\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)|h^{-1}\left[\mathbb{N}\right]\subseteq \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\right\}\cap \left\{h|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)⟼{𝟙}_{\mathbb{N}}\left(\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\},y\in {\mathbb{N}}_0⟼2^{y}x\right)\left[\left(r\in \left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}\right)\left(\mathrm{bits}\circ \left({o\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)\right)\right]\right)\right)\in \mathrm{V}$$
65	64	resex	$$⊢{\left(o\in \left(\left\{h\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)|h^{-1}\left[\mathbb{N}\right]\subseteq \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\right\}\cap \left\{h|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)⟼{𝟙}_{\mathbb{N}}\left(\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\},y\in {\mathbb{N}}_0⟼2^{y}x\right)\left[\left(r\in \left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}\right)\left(\mathrm{bits}\circ \left({o\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)\right)\right]\right)\right)\upharpoonright }_O\in \mathrm{V}$$
66		f1oeq1	$$⊢g={\left(o\in \left(\left\{h\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)|h^{-1}\left[\mathbb{N}\right]\subseteq \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\right\}\cap \left\{h|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)⟼{𝟙}_{\mathbb{N}}\left(\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\},y\in {\mathbb{N}}_0⟼2^{y}x\right)\left[\left(r\in \left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}\right)\left(\mathrm{bits}\circ \left({o\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)\right)\right]\right)\right)\upharpoonright }_O\to \left(g:O\underset{1-1\; onto}{⟶}D\leftrightarrow \left({\left(o\in \left(\left\{h\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)|h^{-1}\left[\mathbb{N}\right]\subseteq \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\right\}\cap \left\{h|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)⟼{𝟙}_{\mathbb{N}}\left(\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\},y\in {\mathbb{N}}_0⟼2^{y}x\right)\left[\left(r\in \left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}\right)\left(\mathrm{bits}\circ \left({o\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)\right)\right]\right)\right)\upharpoonright }_O\right):O\underset{1-1\; onto}{⟶}D\right)$$
67	65 66	spcev	$$⊢\left({\left(o\in \left(\left\{h\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)|h^{-1}\left[\mathbb{N}\right]\subseteq \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\right\}\cap \left\{h|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)⟼{𝟙}_{\mathbb{N}}\left(\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\},y\in {\mathbb{N}}_0⟼2^{y}x\right)\left[\left(r\in \left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}⟼\left\{⟨x,y⟩|\left(x\in \left\{z\in \mathbb{N}|\neg 2\parallel z\right\}\wedge y\in r\left(x\right)\right)\right\}\right)\left(\mathrm{bits}\circ \left({o\upharpoonright }_{\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}}\right)\right)\right]\right)\right)\upharpoonright }_O\right):O\underset{1-1\; onto}{⟶}D\to \exists gg:O\underset{1-1\; onto}{⟶}D$$
68		bren	$$⊢O\approx D\leftrightarrow \exists gg:O\underset{1-1\; onto}{⟶}D$$
69		hasheni	$$⊢O\approx D\to \left|O\right|=\left|D\right|$$
70	68 69	sylbir	$$⊢\exists gg:O\underset{1-1\; onto}{⟶}D\to \left|O\right|=\left|D\right|$$
71	60 67 70	mp2b	$$⊢\left|O\right|=\left|D\right|$$