Theorem eulerpartlemo

Description: Lemma for eulerpart : O is the set of odd partitions of N . (Contributed by Thierry Arnoux, 10-Aug-2017)

	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	eulerpartlemo	$$⊢A\in O\leftrightarrow \left(A\in P\wedge \forall n\in A^{-1}\left[\mathbb{N}\right]\neg 2\parallel n\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		cnveq	$$⊢g=A\to g^{-1}=A^{-1}$$
5	4	imaeq1d	$$⊢g=A\to g^{-1}\left[\mathbb{N}\right]=A^{-1}\left[\mathbb{N}\right]$$
6	5	raleqdv	$$⊢g=A\to \left(\forall n\in g^{-1}\left[\mathbb{N}\right]\neg 2\parallel n\leftrightarrow \forall n\in A^{-1}\left[\mathbb{N}\right]\neg 2\parallel n\right)$$
7	6 2	elrab2	$$⊢A\in O\leftrightarrow \left(A\in P\wedge \forall n\in A^{-1}\left[\mathbb{N}\right]\neg 2\parallel n\right)$$