eulerpartlem1

	Ref	Expression
Hypotheses	eulerpart.p	$⊢ P = \{f \in ({ℕ_{0}}^{ℕ}) \| (f^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} f (k) k = N)\}$
	eulerpart.o	$⊢ O = \{g \in P \| \forall n \in g^{-1} [ℕ] \neg 2 ∥ n\}$
	eulerpart.d	$⊢ D = \{g \in P \| \forall n \in ℕ g (n) \leq 1\}$
	eulerpart.j	$⊢ J = \{z \in ℕ \| \neg 2 ∥ z\}$
	eulerpart.f	$⊢ F = (x \in J, y \in ℕ_{0} ⟼ 2^{y} x)$
	eulerpart.h	$⊢ H = \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{J}) \| r supp \emptyset \in Fin\}$
	eulerpart.m	$⊢ M = (r \in H ⟼ \{⟨x, y⟩ \| (x \in J \land y \in r (x))\})$
Assertion	eulerpartlem1	$⊢ M : H \underset{1-1 onto}{⟶} 𝒫 (J \times ℕ_{0}) \cap Fin$

Proof

Step	Hyp	Ref	Expression
1		eulerpart.p	$⊢ P = \{f \in ({ℕ_{0}}^{ℕ}) \| (f^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} f (k) k = N)\}$
2		eulerpart.o	$⊢ O = \{g \in P \| \forall n \in g^{-1} [ℕ] \neg 2 ∥ n\}$
3		eulerpart.d	$⊢ D = \{g \in P \| \forall n \in ℕ g (n) \leq 1\}$
4		eulerpart.j	$⊢ J = \{z \in ℕ \| \neg 2 ∥ z\}$
5		eulerpart.f	$⊢ F = (x \in J, y \in ℕ_{0} ⟼ 2^{y} x)$
6		eulerpart.h	$⊢ H = \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{J}) \| r supp \emptyset \in Fin\}$
7		eulerpart.m	$⊢ M = (r \in H ⟼ \{⟨x, y⟩ \| (x \in J \land y \in r (x))\})$
8		nnex	$⊢ ℕ \in V$
9	4 8	rabex2	$⊢ J \in V$
10		nn0ex	$⊢ ℕ_{0} \in V$
11		eqid	$⊢ (r \in ({𝒫 ℕ_{0}}^{J}) ⟼ \{⟨x, y⟩ \| (x \in J \land y \in r (x))\}) = (r \in ({𝒫 ℕ_{0}}^{J}) ⟼ \{⟨x, y⟩ \| (x \in J \land y \in r (x))\})$
12	9 10 11 6	fpwrelmapffs	$⊢ ({(r \in ({𝒫 ℕ_{0}}^{J}) ⟼ \{⟨x, y⟩ \| (x \in J \land y \in r (x))\}) ↾}_{H}) : H \underset{1-1 onto}{⟶} 𝒫 (J \times ℕ_{0}) \cap Fin$
13		ssrab2	$⊢ \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{J}) \| r supp \emptyset \in Fin\} \subseteq {(𝒫 ℕ_{0} \cap Fin)}^{J}$
14	10	pwex	$⊢ 𝒫 ℕ_{0} \in V$
15		inss1	$⊢ 𝒫 ℕ_{0} \cap Fin \subseteq 𝒫 ℕ_{0}$
16		mapss	$⊢ (𝒫 ℕ_{0} \in V \land 𝒫 ℕ_{0} \cap Fin \subseteq 𝒫 ℕ_{0}) \to {(𝒫 ℕ_{0} \cap Fin)}^{J} \subseteq {𝒫 ℕ_{0}}^{J}$
17	14 15 16	mp2an	$⊢ {(𝒫 ℕ_{0} \cap Fin)}^{J} \subseteq {𝒫 ℕ_{0}}^{J}$
18	13 17	sstri	$⊢ \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{J}) \| r supp \emptyset \in Fin\} \subseteq {𝒫 ℕ_{0}}^{J}$
19	6 18	eqsstri	$⊢ H \subseteq {𝒫 ℕ_{0}}^{J}$
20		resmpt	$⊢ H \subseteq {𝒫 ℕ_{0}}^{J} \to {(r \in ({𝒫 ℕ_{0}}^{J}) ⟼ \{⟨x, y⟩ \| (x \in J \land y \in r (x))\}) ↾}_{H} = (r \in H ⟼ \{⟨x, y⟩ \| (x \in J \land y \in r (x))\})$
21	19 20	ax-mp	$⊢ {(r \in ({𝒫 ℕ_{0}}^{J}) ⟼ \{⟨x, y⟩ \| (x \in J \land y \in r (x))\}) ↾}_{H} = (r \in H ⟼ \{⟨x, y⟩ \| (x \in J \land y \in r (x))\})$
22	7 21	eqtr4i	$⊢ M = {(r \in ({𝒫 ℕ_{0}}^{J}) ⟼ \{⟨x, y⟩ \| (x \in J \land y \in r (x))\}) ↾}_{H}$
23		f1oeq1	$⊢ M = {(r \in ({𝒫 ℕ_{0}}^{J}) ⟼ \{⟨x, y⟩ \| (x \in J \land y \in r (x))\}) ↾}_{H} \to (M : H \underset{1-1 onto}{⟶} 𝒫 (J \times ℕ_{0}) \cap Fin \leftrightarrow ({(r \in ({𝒫 ℕ_{0}}^{J}) ⟼ \{⟨x, y⟩ \| (x \in J \land y \in r (x))\}) ↾}_{H}) : H \underset{1-1 onto}{⟶} 𝒫 (J \times ℕ_{0}) \cap Fin)$
24	22 23	ax-mp	$⊢ M : H \underset{1-1 onto}{⟶} 𝒫 (J \times ℕ_{0}) \cap Fin \leftrightarrow ({(r \in ({𝒫 ℕ_{0}}^{J}) ⟼ \{⟨x, y⟩ \| (x \in J \land y \in r (x))\}) ↾}_{H}) : H \underset{1-1 onto}{⟶} 𝒫 (J \times ℕ_{0}) \cap Fin$
25	12 24	mpbir	$⊢ M : H \underset{1-1 onto}{⟶} 𝒫 (J \times ℕ_{0}) \cap Fin$

Metamath Proof Explorer

Theorem eulerpartlem1

Proof