Theorem eulerpartlemelr

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 8-Aug-2018)

	Ref	Expression
Hypotheses	eulerpartlems.r	$$⊢R=\left\{f|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	eulerpartlems.s	$$⊢S=\left(f\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)⟼\sum _{k\in \mathbb{N}}f\left(k\right)k\right)$$
Assertion	eulerpartlemelr	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to \left(A:\mathbb{N}⟶{\mathbb{N}}_0\wedge A^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$

Proof

Step	Hyp	Ref	Expression
1		eulerpartlems.r	$$⊢R=\left\{f|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
2		eulerpartlems.s	$$⊢S=\left(f\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)⟼\sum _{k\in \mathbb{N}}f\left(k\right)k\right)$$
3		inss1	$$⊢\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\subseteq {{\mathbb{N}}_0}^{\mathbb{N}}$$
4	3	sseli	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to A\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)$$
5		elmapi	$$⊢A\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\to A:\mathbb{N}⟶{\mathbb{N}}_0$$
6	4 5	syl	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to A:\mathbb{N}⟶{\mathbb{N}}_0$$
7		inss2	$$⊢\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\subseteq R$$
8	7	sseli	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to A\in R$$
9		cnveq	$$⊢f=A\to f^{-1}=A^{-1}$$
10	9	imaeq1d	$$⊢f=A\to f^{-1}\left[\mathbb{N}\right]=A^{-1}\left[\mathbb{N}\right]$$
11	10	eleq1d	$$⊢f=A\to \left(f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\leftrightarrow A^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
12	11 1	elab2g	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to \left(A\in R\leftrightarrow A^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
13	8 12	mpbid	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to A^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
14	6 13	jca	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to \left(A:\mathbb{N}⟶{\mathbb{N}}_0\wedge A^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$