Theorem eulerpartlem1

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 27-Aug-2017) (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\}$$
	eulerpart.j	$$⊢J=\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}$$
	eulerpart.f	$$⊢F=\left(x\in J,y\in {\mathbb{N}}_0⟼2^{y}x\right)$$
	eulerpart.h	$$⊢H=\left\{r\in \left({\left(𝒫{\mathbb{N}}_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)$$
Assertion	eulerpartlem1	$$⊢M:H\underset{1-1\; onto}{⟶}𝒫\left(J\times {\mathbb{N}}_0\right)\cap \mathrm{Fin}$$

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		eulerpart.j	$$⊢J=\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}$$
5		eulerpart.f	$$⊢F=\left(x\in J,y\in {\mathbb{N}}_0⟼2^{y}x\right)$$
6		eulerpart.h	$$⊢H=\left\{r\in \left({\left(𝒫{\mathbb{N}}_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		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
9	4 8	rabex2	$$⊢J\in \mathrm{V}$$
10		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
11		eqid	$$⊢\left(r\in \left({𝒫{\mathbb{N}}_0}^J\right)⟼\left\{⟨x,y⟩|\left(x\in J\wedge y\in r\left(x\right)\right)\right\}\right)=\left(r\in \left({𝒫{\mathbb{N}}_0}^J\right)⟼\left\{⟨x,y⟩|\left(x\in J\wedge y\in r\left(x\right)\right)\right\}\right)$$
12	9 10 11 6	fpwrelmapffs	$$⊢\left({\left(r\in \left({𝒫{\mathbb{N}}_0}^J\right)⟼\left\{⟨x,y⟩|\left(x\in J\wedge y\in r\left(x\right)\right)\right\}\right)\upharpoonright }_H\right):H\underset{1-1\; onto}{⟶}𝒫\left(J\times {\mathbb{N}}_0\right)\cap \mathrm{Fin}$$
13		ssrab2	$$⊢\left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^J\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}\subseteq {\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^J$$
14	10	pwex	$$⊢𝒫{\mathbb{N}}_0\in \mathrm{V}$$
15		inss1	$$⊢𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\subseteq 𝒫{\mathbb{N}}_0$$
16		mapss	$$⊢\left(𝒫{\mathbb{N}}_0\in \mathrm{V}\wedge 𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\subseteq 𝒫{\mathbb{N}}_0\right)\to {\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^J\subseteq {𝒫{\mathbb{N}}_0}^J$$
17	14 15 16	mp2an	$$⊢{\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^J\subseteq {𝒫{\mathbb{N}}_0}^J$$
18	13 17	sstri	$$⊢\left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^J\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}\subseteq {𝒫{\mathbb{N}}_0}^J$$
19	6 18	eqsstri	$$⊢H\subseteq {𝒫{\mathbb{N}}_0}^J$$
20		resmpt	$$⊢H\subseteq {𝒫{\mathbb{N}}_0}^J\to {\left(r\in \left({𝒫{\mathbb{N}}_0}^J\right)⟼\left\{⟨x,y⟩|\left(x\in J\wedge y\in r\left(x\right)\right)\right\}\right)\upharpoonright }_H=\left(r\in H⟼\left\{⟨x,y⟩|\left(x\in J\wedge y\in r\left(x\right)\right)\right\}\right)$$
21	19 20	ax-mp	$$⊢{\left(r\in \left({𝒫{\mathbb{N}}_0}^J\right)⟼\left\{⟨x,y⟩|\left(x\in J\wedge y\in r\left(x\right)\right)\right\}\right)\upharpoonright }_H=\left(r\in H⟼\left\{⟨x,y⟩|\left(x\in J\wedge y\in r\left(x\right)\right)\right\}\right)$$
22	7 21	eqtr4i	$$⊢M={\left(r\in \left({𝒫{\mathbb{N}}_0}^J\right)⟼\left\{⟨x,y⟩|\left(x\in J\wedge y\in r\left(x\right)\right)\right\}\right)\upharpoonright }_H$$
23		f1oeq1	$$⊢M={\left(r\in \left({𝒫{\mathbb{N}}_0}^J\right)⟼\left\{⟨x,y⟩|\left(x\in J\wedge y\in r\left(x\right)\right)\right\}\right)\upharpoonright }_H\to \left(M:H\underset{1-1\; onto}{⟶}𝒫\left(J\times {\mathbb{N}}_0\right)\cap \mathrm{Fin}\leftrightarrow \left({\left(r\in \left({𝒫{\mathbb{N}}_0}^J\right)⟼\left\{⟨x,y⟩|\left(x\in J\wedge y\in r\left(x\right)\right)\right\}\right)\upharpoonright }_H\right):H\underset{1-1\; onto}{⟶}𝒫\left(J\times {\mathbb{N}}_0\right)\cap \mathrm{Fin}\right)$$
24	22 23	ax-mp	$$⊢M:H\underset{1-1\; onto}{⟶}𝒫\left(J\times {\mathbb{N}}_0\right)\cap \mathrm{Fin}\leftrightarrow \left({\left(r\in \left({𝒫{\mathbb{N}}_0}^J\right)⟼\left\{⟨x,y⟩|\left(x\in J\wedge y\in r\left(x\right)\right)\right\}\right)\upharpoonright }_H\right):H\underset{1-1\; onto}{⟶}𝒫\left(J\times {\mathbb{N}}_0\right)\cap \mathrm{Fin}$$
25	12 24	mpbir	$$⊢M:H\underset{1-1\; onto}{⟶}𝒫\left(J\times {\mathbb{N}}_0\right)\cap \mathrm{Fin}$$