eulerpartgbij

Description: Lemma for eulerpart : The G function is a bijection. (Contributed by Thierry Arnoux, 27-Aug-2017) (Revised by Thierry Arnoux, 1-Sep-2019)

	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))\})$
	eulerpart.r	$⊢ R = \{f \| f^{-1} [ℕ] \in Fin\}$
	eulerpart.t	$⊢ T = \{f \in ({ℕ_{0}}^{ℕ}) \| f^{-1} [ℕ] \subseteq J\}$
	eulerpart.g	$⊢ G = (o \in (T \cap R) ⟼ 𝟙_{ℕ} (F [M (bits \circ ({o ↾}_{J}))]))$
Assertion	eulerpartgbij	$⊢ G : T \cap R \underset{1-1 onto}{⟶} ({\{0, 1\}}^{ℕ}) \cap R$

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		eulerpart.r	$⊢ R = \{f \| f^{-1} [ℕ] \in Fin\}$
9		eulerpart.t	$⊢ T = \{f \in ({ℕ_{0}}^{ℕ}) \| f^{-1} [ℕ] \subseteq J\}$
10		eulerpart.g	$⊢ G = (o \in (T \cap R) ⟼ 𝟙_{ℕ} (F [M (bits \circ ({o ↾}_{J}))]))$
11		nnex	$⊢ ℕ \in V$
12		indf1ofs	$⊢ ℕ \in V \to ({𝟙_{ℕ} ↾}_{Fin}) : 𝒫 ℕ \cap Fin \underset{1-1 onto}{⟶} \{f \in ({\{0, 1\}}^{ℕ}) \| f^{-1} [\{1\}] \in Fin\}$
13	11 12	ax-mp	$⊢ ({𝟙_{ℕ} ↾}_{Fin}) : 𝒫 ℕ \cap Fin \underset{1-1 onto}{⟶} \{f \in ({\{0, 1\}}^{ℕ}) \| f^{-1} [\{1\}] \in Fin\}$
14		incom	$⊢ ({\{0, 1\}}^{ℕ}) \cap \{f \| f^{-1} [ℕ] \in Fin\} = \{f \| f^{-1} [ℕ] \in Fin\} \cap ({\{0, 1\}}^{ℕ})$
15	8	ineq2i	$⊢ ({\{0, 1\}}^{ℕ}) \cap R = ({\{0, 1\}}^{ℕ}) \cap \{f \| f^{-1} [ℕ] \in Fin\}$
16		dfrab2	$⊢ \{f \in ({\{0, 1\}}^{ℕ}) \| f^{-1} [ℕ] \in Fin\} = \{f \| f^{-1} [ℕ] \in Fin\} \cap ({\{0, 1\}}^{ℕ})$
17	14 15 16	3eqtr4i	$⊢ ({\{0, 1\}}^{ℕ}) \cap R = \{f \in ({\{0, 1\}}^{ℕ}) \| f^{-1} [ℕ] \in Fin\}$
18		elmapfun	$⊢ f \in ({\{0, 1\}}^{ℕ}) \to Fun f$
19		elmapi	$⊢ f \in ({\{0, 1\}}^{ℕ}) \to f : ℕ ⟶ \{0, 1\}$
20	19	frnd	$⊢ f \in ({\{0, 1\}}^{ℕ}) \to ran f \subseteq \{0, 1\}$
21		fimacnvinrn2	$⊢ (Fun f \land ran f \subseteq \{0, 1\}) \to f^{-1} [ℕ] = f^{-1} [ℕ \cap \{0, 1\}]$
22		df-pr	$⊢ \{0, 1\} = \{0\} \cup \{1\}$
23	22	ineq2i	$⊢ ℕ \cap \{0, 1\} = ℕ \cap (\{0\} \cup \{1\})$
24		indi	$⊢ ℕ \cap (\{0\} \cup \{1\}) = (ℕ \cap \{0\}) \cup (ℕ \cap \{1\})$
25		0nnn	$⊢ \neg 0 \in ℕ$
26		disjsn	$⊢ ℕ \cap \{0\} = \emptyset \leftrightarrow \neg 0 \in ℕ$
27	25 26	mpbir	$⊢ ℕ \cap \{0\} = \emptyset$
28		1nn	$⊢ 1 \in ℕ$
29		1ex	$⊢ 1 \in V$
30	29	snss	$⊢ 1 \in ℕ \leftrightarrow \{1\} \subseteq ℕ$
31	28 30	mpbi	$⊢ \{1\} \subseteq ℕ$
32		dfss	$⊢ \{1\} \subseteq ℕ \leftrightarrow \{1\} = \{1\} \cap ℕ$
33	31 32	mpbi	$⊢ \{1\} = \{1\} \cap ℕ$
34		incom	$⊢ \{1\} \cap ℕ = ℕ \cap \{1\}$
35	33 34	eqtr2i	$⊢ ℕ \cap \{1\} = \{1\}$
36	27 35	uneq12i	$⊢ (ℕ \cap \{0\}) \cup (ℕ \cap \{1\}) = \emptyset \cup \{1\}$
37	23 24 36	3eqtri	$⊢ ℕ \cap \{0, 1\} = \emptyset \cup \{1\}$
38		uncom	$⊢ \emptyset \cup \{1\} = \{1\} \cup \emptyset$
39		un0	$⊢ \{1\} \cup \emptyset = \{1\}$
40	37 38 39	3eqtri	$⊢ ℕ \cap \{0, 1\} = \{1\}$
41	40	imaeq2i	$⊢ f^{-1} [ℕ \cap \{0, 1\}] = f^{-1} [\{1\}]$
42	21 41	eqtrdi	$⊢ (Fun f \land ran f \subseteq \{0, 1\}) \to f^{-1} [ℕ] = f^{-1} [\{1\}]$
43	18 20 42	syl2anc	$⊢ f \in ({\{0, 1\}}^{ℕ}) \to f^{-1} [ℕ] = f^{-1} [\{1\}]$
44	43	eleq1d	$⊢ f \in ({\{0, 1\}}^{ℕ}) \to (f^{-1} [ℕ] \in Fin \leftrightarrow f^{-1} [\{1\}] \in Fin)$
45	44	rabbiia	$⊢ \{f \in ({\{0, 1\}}^{ℕ}) \| f^{-1} [ℕ] \in Fin\} = \{f \in ({\{0, 1\}}^{ℕ}) \| f^{-1} [\{1\}] \in Fin\}$
46	17 45	eqtr2i	$⊢ \{f \in ({\{0, 1\}}^{ℕ}) \| f^{-1} [\{1\}] \in Fin\} = ({\{0, 1\}}^{ℕ}) \cap R$
47		f1oeq3	$⊢ \{f \in ({\{0, 1\}}^{ℕ}) \| f^{-1} [\{1\}] \in Fin\} = ({\{0, 1\}}^{ℕ}) \cap R \to (({𝟙_{ℕ} ↾}_{Fin}) : 𝒫 ℕ \cap Fin \underset{1-1 onto}{⟶} \{f \in ({\{0, 1\}}^{ℕ}) \| f^{-1} [\{1\}] \in Fin\} \leftrightarrow ({𝟙_{ℕ} ↾}_{Fin}) : 𝒫 ℕ \cap Fin \underset{1-1 onto}{⟶} ({\{0, 1\}}^{ℕ}) \cap R)$
48	46 47	ax-mp	$⊢ ({𝟙_{ℕ} ↾}_{Fin}) : 𝒫 ℕ \cap Fin \underset{1-1 onto}{⟶} \{f \in ({\{0, 1\}}^{ℕ}) \| f^{-1} [\{1\}] \in Fin\} \leftrightarrow ({𝟙_{ℕ} ↾}_{Fin}) : 𝒫 ℕ \cap Fin \underset{1-1 onto}{⟶} ({\{0, 1\}}^{ℕ}) \cap R$
49	13 48	mpbi	$⊢ ({𝟙_{ℕ} ↾}_{Fin}) : 𝒫 ℕ \cap Fin \underset{1-1 onto}{⟶} ({\{0, 1\}}^{ℕ}) \cap R$
50	4 5	oddpwdc	$⊢ F : J \times ℕ_{0} \underset{1-1 onto}{⟶} ℕ$
51		f1opwfi	$⊢ F : J \times ℕ_{0} \underset{1-1 onto}{⟶} ℕ \to (a \in (𝒫 (J \times ℕ_{0}) \cap Fin) ⟼ F [a]) : 𝒫 (J \times ℕ_{0}) \cap Fin \underset{1-1 onto}{⟶} 𝒫 ℕ \cap Fin$
52	50 51	ax-mp	$⊢ (a \in (𝒫 (J \times ℕ_{0}) \cap Fin) ⟼ F [a]) : 𝒫 (J \times ℕ_{0}) \cap Fin \underset{1-1 onto}{⟶} 𝒫 ℕ \cap Fin$
53	1 2 3 4 5 6 7	eulerpartlem1	$⊢ M : H \underset{1-1 onto}{⟶} 𝒫 (J \times ℕ_{0}) \cap Fin$
54		bitsf1o	$⊢ ({bits ↾}_{ℕ_{0}}) : ℕ_{0} \underset{1-1 onto}{⟶} 𝒫 ℕ_{0} \cap Fin$
55	54	a1i	$⊢ ⊤ \to ({bits ↾}_{ℕ_{0}}) : ℕ_{0} \underset{1-1 onto}{⟶} 𝒫 ℕ_{0} \cap Fin$
56	4 11	rabex2	$⊢ J \in V$
57	56	a1i	$⊢ ⊤ \to J \in V$
58		nn0ex	$⊢ ℕ_{0} \in V$
59	58	a1i	$⊢ ⊤ \to ℕ_{0} \in V$
60	58	pwex	$⊢ 𝒫 ℕ_{0} \in V$
61	60	inex1	$⊢ 𝒫 ℕ_{0} \cap Fin \in V$
62	61	a1i	$⊢ ⊤ \to 𝒫 ℕ_{0} \cap Fin \in V$
63		0nn0	$⊢ 0 \in ℕ_{0}$
64	63	a1i	$⊢ ⊤ \to 0 \in ℕ_{0}$
65		fvres	$⊢ 0 \in ℕ_{0} \to ({bits ↾}_{ℕ_{0}}) (0) = bits (0)$
66	63 65	ax-mp	$⊢ ({bits ↾}_{ℕ_{0}}) (0) = bits (0)$
67		0bits	$⊢ bits (0) = \emptyset$
68	66 67	eqtr2i	$⊢ \emptyset = ({bits ↾}_{ℕ_{0}}) (0)$
69		elmapi	$⊢ f \in ({ℕ_{0}}^{J}) \to f : J ⟶ ℕ_{0}$
70		frnnn0supp	$⊢ (J \in V \land f : J ⟶ ℕ_{0}) \to f supp 0 = f^{-1} [ℕ]$
71	56 69 70	sylancr	$⊢ f \in ({ℕ_{0}}^{J}) \to f supp 0 = f^{-1} [ℕ]$
72	71	eleq1d	$⊢ f \in ({ℕ_{0}}^{J}) \to (f supp 0 \in Fin \leftrightarrow f^{-1} [ℕ] \in Fin)$
73	72	rabbiia	$⊢ \{f \in ({ℕ_{0}}^{J}) \| f supp 0 \in Fin\} = \{f \in ({ℕ_{0}}^{J}) \| f^{-1} [ℕ] \in Fin\}$
74		elmapfun	$⊢ f \in ({ℕ_{0}}^{J}) \to Fun f$
75		vex	$⊢ f \in V$
76		funisfsupp	$⊢ (Fun f \land f \in V \land 0 \in ℕ_{0}) \to ({finSupp}_{0} (f) \leftrightarrow f supp 0 \in Fin)$
77	75 63 76	mp3an23	$⊢ Fun f \to ({finSupp}_{0} (f) \leftrightarrow f supp 0 \in Fin)$
78	74 77	syl	$⊢ f \in ({ℕ_{0}}^{J}) \to ({finSupp}_{0} (f) \leftrightarrow f supp 0 \in Fin)$
79	78	rabbiia	$⊢ \{f \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (f)\} = \{f \in ({ℕ_{0}}^{J}) \| f supp 0 \in Fin\}$
80		incom	$⊢ \{f \| f^{-1} [ℕ] \in Fin\} \cap ({ℕ_{0}}^{J}) = ({ℕ_{0}}^{J}) \cap \{f \| f^{-1} [ℕ] \in Fin\}$
81		dfrab2	$⊢ \{f \in ({ℕ_{0}}^{J}) \| f^{-1} [ℕ] \in Fin\} = \{f \| f^{-1} [ℕ] \in Fin\} \cap ({ℕ_{0}}^{J})$
82	8	ineq2i	$⊢ ({ℕ_{0}}^{J}) \cap R = ({ℕ_{0}}^{J}) \cap \{f \| f^{-1} [ℕ] \in Fin\}$
83	80 81 82	3eqtr4ri	$⊢ ({ℕ_{0}}^{J}) \cap R = \{f \in ({ℕ_{0}}^{J}) \| f^{-1} [ℕ] \in Fin\}$
84	73 79 83	3eqtr4ri	$⊢ ({ℕ_{0}}^{J}) \cap R = \{f \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (f)\}$
85		elmapfun	$⊢ r \in ({(𝒫 ℕ_{0} \cap Fin)}^{J}) \to Fun r$
86		vex	$⊢ r \in V$
87		0ex	$⊢ \emptyset \in V$
88		funisfsupp	$⊢ (Fun r \land r \in V \land \emptyset \in V) \to ({finSupp}_{\emptyset} (r) \leftrightarrow r supp \emptyset \in Fin)$
89	86 87 88	mp3an23	$⊢ Fun r \to ({finSupp}_{\emptyset} (r) \leftrightarrow r supp \emptyset \in Fin)$
90	89	bicomd	$⊢ Fun r \to (r supp \emptyset \in Fin \leftrightarrow {finSupp}_{\emptyset} (r))$
91	85 90	syl	$⊢ r \in ({(𝒫 ℕ_{0} \cap Fin)}^{J}) \to (r supp \emptyset \in Fin \leftrightarrow {finSupp}_{\emptyset} (r))$
92	91	rabbiia	$⊢ \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{J}) \| r supp \emptyset \in Fin\} = \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{J}) \| {finSupp}_{\emptyset} (r)\}$
93	55 57 59 62 64 68 84 92	fcobijfs	$⊢ ⊤ \to (f \in (({ℕ_{0}}^{J}) \cap R) ⟼ ({bits ↾}_{ℕ_{0}}) \circ f) : ({ℕ_{0}}^{J}) \cap R \underset{1-1 onto}{⟶} \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{J}) \| r supp \emptyset \in Fin\}$
94		elinel1	$⊢ f \in (({ℕ_{0}}^{J}) \cap R) \to f \in ({ℕ_{0}}^{J})$
95		frn	$⊢ f : J ⟶ ℕ_{0} \to ran f \subseteq ℕ_{0}$
96		cores	$⊢ ran f \subseteq ℕ_{0} \to ({bits ↾}_{ℕ_{0}}) \circ f = bits \circ f$
97	69 95 96	3syl	$⊢ f \in ({ℕ_{0}}^{J}) \to ({bits ↾}_{ℕ_{0}}) \circ f = bits \circ f$
98	94 97	syl	$⊢ f \in (({ℕ_{0}}^{J}) \cap R) \to ({bits ↾}_{ℕ_{0}}) \circ f = bits \circ f$
99	98	mpteq2ia	$⊢ (f \in (({ℕ_{0}}^{J}) \cap R) ⟼ ({bits ↾}_{ℕ_{0}}) \circ f) = (f \in (({ℕ_{0}}^{J}) \cap R) ⟼ bits \circ f)$
100	99	eqcomi	$⊢ (f \in (({ℕ_{0}}^{J}) \cap R) ⟼ bits \circ f) = (f \in (({ℕ_{0}}^{J}) \cap R) ⟼ ({bits ↾}_{ℕ_{0}}) \circ f)$
101		f1oeq1	$⊢ (f \in (({ℕ_{0}}^{J}) \cap R) ⟼ bits \circ f) = (f \in (({ℕ_{0}}^{J}) \cap R) ⟼ ({bits ↾}_{ℕ_{0}}) \circ f) \to ((f \in (({ℕ_{0}}^{J}) \cap R) ⟼ bits \circ f) : ({ℕ_{0}}^{J}) \cap R \underset{1-1 onto}{⟶} \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{J}) \| r supp \emptyset \in Fin\} \leftrightarrow (f \in (({ℕ_{0}}^{J}) \cap R) ⟼ ({bits ↾}_{ℕ_{0}}) \circ f) : ({ℕ_{0}}^{J}) \cap R \underset{1-1 onto}{⟶} \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{J}) \| r supp \emptyset \in Fin\})$
102	100 101	mp1i	$⊢ ⊤ \to ((f \in (({ℕ_{0}}^{J}) \cap R) ⟼ bits \circ f) : ({ℕ_{0}}^{J}) \cap R \underset{1-1 onto}{⟶} \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{J}) \| r supp \emptyset \in Fin\} \leftrightarrow (f \in (({ℕ_{0}}^{J}) \cap R) ⟼ ({bits ↾}_{ℕ_{0}}) \circ f) : ({ℕ_{0}}^{J}) \cap R \underset{1-1 onto}{⟶} \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{J}) \| r supp \emptyset \in Fin\})$
103	93 102	mpbird	$⊢ ⊤ \to (f \in (({ℕ_{0}}^{J}) \cap R) ⟼ bits \circ f) : ({ℕ_{0}}^{J}) \cap R \underset{1-1 onto}{⟶} \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{J}) \| r supp \emptyset \in Fin\}$
104	103	mptru	$⊢ (f \in (({ℕ_{0}}^{J}) \cap R) ⟼ bits \circ f) : ({ℕ_{0}}^{J}) \cap R \underset{1-1 onto}{⟶} \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{J}) \| r supp \emptyset \in Fin\}$
105		ssrab2	$⊢ \{z \in ℕ \| \neg 2 ∥ z\} \subseteq ℕ$
106	4 105	eqsstri	$⊢ J \subseteq ℕ$
107	11 58 106	3pm3.2i	$⊢ (ℕ \in V \land ℕ_{0} \in V \land J \subseteq ℕ)$
108		cnveq	$⊢ f = o \to f^{-1} = o^{-1}$
109		dfn2	$⊢ ℕ = ℕ_{0} ∖ \{0\}$
110	109	a1i	$⊢ f = o \to ℕ = ℕ_{0} ∖ \{0\}$
111	108 110	imaeq12d	$⊢ f = o \to f^{-1} [ℕ] = o^{-1} [ℕ_{0} ∖ \{0\}]$
112	111	sseq1d	$⊢ f = o \to (f^{-1} [ℕ] \subseteq J \leftrightarrow o^{-1} [ℕ_{0} ∖ \{0\}] \subseteq J)$
113	112	cbvrabv	$⊢ \{f \in ({ℕ_{0}}^{ℕ}) \| f^{-1} [ℕ] \subseteq J\} = \{o \in ({ℕ_{0}}^{ℕ}) \| o^{-1} [ℕ_{0} ∖ \{0\}] \subseteq J\}$
114	9 113	eqtri	$⊢ T = \{o \in ({ℕ_{0}}^{ℕ}) \| o^{-1} [ℕ_{0} ∖ \{0\}] \subseteq J\}$
115		eqid	$⊢ (o \in T ⟼ {o ↾}_{J}) = (o \in T ⟼ {o ↾}_{J})$
116	114 115	resf1o	$⊢ ((ℕ \in V \land ℕ_{0} \in V \land J \subseteq ℕ) \land 0 \in ℕ_{0}) \to (o \in T ⟼ {o ↾}_{J}) : T \underset{1-1 onto}{⟶} {ℕ_{0}}^{J}$
117	107 63 116	mp2an	$⊢ (o \in T ⟼ {o ↾}_{J}) : T \underset{1-1 onto}{⟶} {ℕ_{0}}^{J}$
118		f1of1	$⊢ (o \in T ⟼ {o ↾}_{J}) : T \underset{1-1 onto}{⟶} {ℕ_{0}}^{J} \to (o \in T ⟼ {o ↾}_{J}) : T \underset{1-1}{⟶} {ℕ_{0}}^{J}$
119	117 118	ax-mp	$⊢ (o \in T ⟼ {o ↾}_{J}) : T \underset{1-1}{⟶} {ℕ_{0}}^{J}$
120		inss1	$⊢ T \cap R \subseteq T$
121		f1ores	$⊢ ((o \in T ⟼ {o ↾}_{J}) : T \underset{1-1}{⟶} {ℕ_{0}}^{J} \land T \cap R \subseteq T) \to ({(o \in T ⟼ {o ↾}_{J}) ↾}_{(T \cap R)}) : T \cap R \underset{1-1 onto}{⟶} (o \in T ⟼ {o ↾}_{J}) [T \cap R]$
122	119 120 121	mp2an	$⊢ ({(o \in T ⟼ {o ↾}_{J}) ↾}_{(T \cap R)}) : T \cap R \underset{1-1 onto}{⟶} (o \in T ⟼ {o ↾}_{J}) [T \cap R]$
123		vex	$⊢ o \in V$
124	123	resex	$⊢ {o ↾}_{J} \in V$
125	124 115	fnmpti	$⊢ (o \in T ⟼ {o ↾}_{J}) Fn T$
126		fvelimab	$⊢ ((o \in T ⟼ {o ↾}_{J}) Fn T \land T \cap R \subseteq T) \to (f \in (o \in T ⟼ {o ↾}_{J}) [T \cap R] \leftrightarrow \exists m \in (T \cap R) (o \in T ⟼ {o ↾}_{J}) (m) = f)$
127	125 120 126	mp2an	$⊢ f \in (o \in T ⟼ {o ↾}_{J}) [T \cap R] \leftrightarrow \exists m \in (T \cap R) (o \in T ⟼ {o ↾}_{J}) (m) = f$
128		eqid	$⊢ (m \in (T \cap R) ⟼ {m ↾}_{J}) = (m \in (T \cap R) ⟼ {m ↾}_{J})$
129		vex	$⊢ m \in V$
130	129	resex	$⊢ {m ↾}_{J} \in V$
131	128 130	elrnmpti	$⊢ f \in ran (m \in (T \cap R) ⟼ {m ↾}_{J}) \leftrightarrow \exists m \in (T \cap R) f = {m ↾}_{J}$
132	1 2 3 4 5 6 7 8 9	eulerpartlemt	$⊢ ({ℕ_{0}}^{J}) \cap R = ran (m \in (T \cap R) ⟼ {m ↾}_{J})$
133	132	eleq2i	$⊢ f \in (({ℕ_{0}}^{J}) \cap R) \leftrightarrow f \in ran (m \in (T \cap R) ⟼ {m ↾}_{J})$
134		elinel1	$⊢ m \in (T \cap R) \to m \in T$
135	115	fvtresfn	$⊢ m \in T \to (o \in T ⟼ {o ↾}_{J}) (m) = {m ↾}_{J}$
136	135	eqeq1d	$⊢ m \in T \to ((o \in T ⟼ {o ↾}_{J}) (m) = f \leftrightarrow {m ↾}_{J} = f)$
137	134 136	syl	$⊢ m \in (T \cap R) \to ((o \in T ⟼ {o ↾}_{J}) (m) = f \leftrightarrow {m ↾}_{J} = f)$
138		eqcom	$⊢ {m ↾}_{J} = f \leftrightarrow f = {m ↾}_{J}$
139	137 138	bitrdi	$⊢ m \in (T \cap R) \to ((o \in T ⟼ {o ↾}_{J}) (m) = f \leftrightarrow f = {m ↾}_{J})$
140	139	rexbiia	$⊢ \exists m \in (T \cap R) (o \in T ⟼ {o ↾}_{J}) (m) = f \leftrightarrow \exists m \in (T \cap R) f = {m ↾}_{J}$
141	131 133 140	3bitr4ri	$⊢ \exists m \in (T \cap R) (o \in T ⟼ {o ↾}_{J}) (m) = f \leftrightarrow f \in (({ℕ_{0}}^{J}) \cap R)$
142	127 141	bitri	$⊢ f \in (o \in T ⟼ {o ↾}_{J}) [T \cap R] \leftrightarrow f \in (({ℕ_{0}}^{J}) \cap R)$
143	142	eqriv	$⊢ (o \in T ⟼ {o ↾}_{J}) [T \cap R] = ({ℕ_{0}}^{J}) \cap R$
144		f1oeq3	$⊢ (o \in T ⟼ {o ↾}_{J}) [T \cap R] = ({ℕ_{0}}^{J}) \cap R \to (({(o \in T ⟼ {o ↾}_{J}) ↾}_{(T \cap R)}) : T \cap R \underset{1-1 onto}{⟶} (o \in T ⟼ {o ↾}_{J}) [T \cap R] \leftrightarrow ({(o \in T ⟼ {o ↾}_{J}) ↾}_{(T \cap R)}) : T \cap R \underset{1-1 onto}{⟶} ({ℕ_{0}}^{J}) \cap R)$
145	143 144	ax-mp	$⊢ ({(o \in T ⟼ {o ↾}_{J}) ↾}_{(T \cap R)}) : T \cap R \underset{1-1 onto}{⟶} (o \in T ⟼ {o ↾}_{J}) [T \cap R] \leftrightarrow ({(o \in T ⟼ {o ↾}_{J}) ↾}_{(T \cap R)}) : T \cap R \underset{1-1 onto}{⟶} ({ℕ_{0}}^{J}) \cap R$
146		resmpt	$⊢ T \cap R \subseteq T \to {(o \in T ⟼ {o ↾}_{J}) ↾}_{(T \cap R)} = (o \in (T \cap R) ⟼ {o ↾}_{J})$
147		f1oeq1	$⊢ {(o \in T ⟼ {o ↾}_{J}) ↾}_{(T \cap R)} = (o \in (T \cap R) ⟼ {o ↾}_{J}) \to (({(o \in T ⟼ {o ↾}_{J}) ↾}_{(T \cap R)}) : T \cap R \underset{1-1 onto}{⟶} ({ℕ_{0}}^{J}) \cap R \leftrightarrow (o \in (T \cap R) ⟼ {o ↾}_{J}) : T \cap R \underset{1-1 onto}{⟶} ({ℕ_{0}}^{J}) \cap R)$
148	120 146 147	mp2b	$⊢ ({(o \in T ⟼ {o ↾}_{J}) ↾}_{(T \cap R)}) : T \cap R \underset{1-1 onto}{⟶} ({ℕ_{0}}^{J}) \cap R \leftrightarrow (o \in (T \cap R) ⟼ {o ↾}_{J}) : T \cap R \underset{1-1 onto}{⟶} ({ℕ_{0}}^{J}) \cap R$
149	145 148	bitri	$⊢ ({(o \in T ⟼ {o ↾}_{J}) ↾}_{(T \cap R)}) : T \cap R \underset{1-1 onto}{⟶} (o \in T ⟼ {o ↾}_{J}) [T \cap R] \leftrightarrow (o \in (T \cap R) ⟼ {o ↾}_{J}) : T \cap R \underset{1-1 onto}{⟶} ({ℕ_{0}}^{J}) \cap R$
150	122 149	mpbi	$⊢ (o \in (T \cap R) ⟼ {o ↾}_{J}) : T \cap R \underset{1-1 onto}{⟶} ({ℕ_{0}}^{J}) \cap R$
151		f1oco	$⊢ ((f \in (({ℕ_{0}}^{J}) \cap R) ⟼ bits \circ f) : ({ℕ_{0}}^{J}) \cap R \underset{1-1 onto}{⟶} \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{J}) \| r supp \emptyset \in Fin\} \land (o \in (T \cap R) ⟼ {o ↾}_{J}) : T \cap R \underset{1-1 onto}{⟶} ({ℕ_{0}}^{J}) \cap R) \to ((f \in (({ℕ_{0}}^{J}) \cap R) ⟼ bits \circ f) \circ (o \in (T \cap R) ⟼ {o ↾}_{J})) : T \cap R \underset{1-1 onto}{⟶} \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{J}) \| r supp \emptyset \in Fin\}$
152	104 150 151	mp2an	$⊢ ((f \in (({ℕ_{0}}^{J}) \cap R) ⟼ bits \circ f) \circ (o \in (T \cap R) ⟼ {o ↾}_{J})) : T \cap R \underset{1-1 onto}{⟶} \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{J}) \| r supp \emptyset \in Fin\}$
153		f1of	$⊢ (o \in (T \cap R) ⟼ {o ↾}_{J}) : T \cap R \underset{1-1 onto}{⟶} ({ℕ_{0}}^{J}) \cap R \to (o \in (T \cap R) ⟼ {o ↾}_{J}) : T \cap R ⟶ ({ℕ_{0}}^{J}) \cap R$
154		eqid	$⊢ (o \in (T \cap R) ⟼ {o ↾}_{J}) = (o \in (T \cap R) ⟼ {o ↾}_{J})$
155	154	fmpt	$⊢ \forall o \in (T \cap R) {o ↾}_{J} \in (({ℕ_{0}}^{J}) \cap R) \leftrightarrow (o \in (T \cap R) ⟼ {o ↾}_{J}) : T \cap R ⟶ ({ℕ_{0}}^{J}) \cap R$
156	155	biimpri	$⊢ (o \in (T \cap R) ⟼ {o ↾}_{J}) : T \cap R ⟶ ({ℕ_{0}}^{J}) \cap R \to \forall o \in (T \cap R) {o ↾}_{J} \in (({ℕ_{0}}^{J}) \cap R)$
157	150 153 156	mp2b	$⊢ \forall o \in (T \cap R) {o ↾}_{J} \in (({ℕ_{0}}^{J}) \cap R)$
158	157	a1i	$⊢ ⊤ \to \forall o \in (T \cap R) {o ↾}_{J} \in (({ℕ_{0}}^{J}) \cap R)$
159		eqidd	$⊢ ⊤ \to (o \in (T \cap R) ⟼ {o ↾}_{J}) = (o \in (T \cap R) ⟼ {o ↾}_{J})$
160		eqidd	$⊢ ⊤ \to (f \in (({ℕ_{0}}^{J}) \cap R) ⟼ bits \circ f) = (f \in (({ℕ_{0}}^{J}) \cap R) ⟼ bits \circ f)$
161		coeq2	$⊢ f = {o ↾}_{J} \to bits \circ f = bits \circ ({o ↾}_{J})$
162	158 159 160 161	fmptcof	$⊢ ⊤ \to (f \in (({ℕ_{0}}^{J}) \cap R) ⟼ bits \circ f) \circ (o \in (T \cap R) ⟼ {o ↾}_{J}) = (o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J}))$
163	162	eqcomd	$⊢ ⊤ \to (o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J})) = (f \in (({ℕ_{0}}^{J}) \cap R) ⟼ bits \circ f) \circ (o \in (T \cap R) ⟼ {o ↾}_{J})$
164		eqidd	$⊢ ⊤ \to T \cap R = T \cap R$
165	6	a1i	$⊢ ⊤ \to H = \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{J}) \| r supp \emptyset \in Fin\}$
166	163 164 165	f1oeq123d	$⊢ ⊤ \to ((o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J})) : T \cap R \underset{1-1 onto}{⟶} H \leftrightarrow ((f \in (({ℕ_{0}}^{J}) \cap R) ⟼ bits \circ f) \circ (o \in (T \cap R) ⟼ {o ↾}_{J})) : T \cap R \underset{1-1 onto}{⟶} \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{J}) \| r supp \emptyset \in Fin\})$
167	152 166	mpbiri	$⊢ ⊤ \to (o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J})) : T \cap R \underset{1-1 onto}{⟶} H$
168	167	mptru	$⊢ (o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J})) : T \cap R \underset{1-1 onto}{⟶} H$
169		f1oco	$⊢ (M : H \underset{1-1 onto}{⟶} 𝒫 (J \times ℕ_{0}) \cap Fin \land (o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J})) : T \cap R \underset{1-1 onto}{⟶} H) \to (M \circ (o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J}))) : T \cap R \underset{1-1 onto}{⟶} 𝒫 (J \times ℕ_{0}) \cap Fin$
170	53 168 169	mp2an	$⊢ (M \circ (o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J}))) : T \cap R \underset{1-1 onto}{⟶} 𝒫 (J \times ℕ_{0}) \cap Fin$
171		eqidd	$⊢ ⊤ \to (o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J})) = (o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J}))$
172		bitsf	$⊢ bits : ℤ ⟶ 𝒫 ℕ_{0}$
173		zex	$⊢ ℤ \in V$
174		fex	$⊢ (bits : ℤ ⟶ 𝒫 ℕ_{0} \land ℤ \in V) \to bits \in V$
175	172 173 174	mp2an	$⊢ bits \in V$
176	175 124	coex	$⊢ bits \circ ({o ↾}_{J}) \in V$
177	176	a1i	$⊢ (⊤ \land o \in (T \cap R)) \to bits \circ ({o ↾}_{J}) \in V$
178	171 177	fvmpt2d	$⊢ (⊤ \land o \in (T \cap R)) \to (o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J})) (o) = bits \circ ({o ↾}_{J})$
179		f1of	$⊢ (o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J})) : T \cap R \underset{1-1 onto}{⟶} H \to (o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J})) : T \cap R ⟶ H$
180	167 179	syl	$⊢ ⊤ \to (o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J})) : T \cap R ⟶ H$
181	180	ffvelrnda	$⊢ (⊤ \land o \in (T \cap R)) \to (o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J})) (o) \in H$
182	178 181	eqeltrrd	$⊢ (⊤ \land o \in (T \cap R)) \to bits \circ ({o ↾}_{J}) \in H$
183		f1ofn	$⊢ M : H \underset{1-1 onto}{⟶} 𝒫 (J \times ℕ_{0}) \cap Fin \to M Fn H$
184	53 183	ax-mp	$⊢ M Fn H$
185		dffn5	$⊢ M Fn H \leftrightarrow M = (r \in H ⟼ M (r))$
186	184 185	mpbi	$⊢ M = (r \in H ⟼ M (r))$
187	186	a1i	$⊢ ⊤ \to M = (r \in H ⟼ M (r))$
188		fveq2	$⊢ r = bits \circ ({o ↾}_{J}) \to M (r) = M (bits \circ ({o ↾}_{J}))$
189	182 171 187 188	fmptco	$⊢ ⊤ \to M \circ (o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J})) = (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J})))$
190	189	mptru	$⊢ M \circ (o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J})) = (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J})))$
191		f1oeq1	$⊢ M \circ (o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J})) = (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J}))) \to ((M \circ (o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J}))) : T \cap R \underset{1-1 onto}{⟶} 𝒫 (J \times ℕ_{0}) \cap Fin \leftrightarrow (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J}))) : T \cap R \underset{1-1 onto}{⟶} 𝒫 (J \times ℕ_{0}) \cap Fin)$
192	190 191	ax-mp	$⊢ (M \circ (o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J}))) : T \cap R \underset{1-1 onto}{⟶} 𝒫 (J \times ℕ_{0}) \cap Fin \leftrightarrow (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J}))) : T \cap R \underset{1-1 onto}{⟶} 𝒫 (J \times ℕ_{0}) \cap Fin$
193	170 192	mpbi	$⊢ (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J}))) : T \cap R \underset{1-1 onto}{⟶} 𝒫 (J \times ℕ_{0}) \cap Fin$
194		f1oco	$⊢ ((a \in (𝒫 (J \times ℕ_{0}) \cap Fin) ⟼ F [a]) : 𝒫 (J \times ℕ_{0}) \cap Fin \underset{1-1 onto}{⟶} 𝒫 ℕ \cap Fin \land (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J}))) : T \cap R \underset{1-1 onto}{⟶} 𝒫 (J \times ℕ_{0}) \cap Fin) \to ((a \in (𝒫 (J \times ℕ_{0}) \cap Fin) ⟼ F [a]) \circ (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J})))) : T \cap R \underset{1-1 onto}{⟶} 𝒫 ℕ \cap Fin$
195	52 193 194	mp2an	$⊢ ((a \in (𝒫 (J \times ℕ_{0}) \cap Fin) ⟼ F [a]) \circ (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J})))) : T \cap R \underset{1-1 onto}{⟶} 𝒫 ℕ \cap Fin$
196		simpr	$⊢ (⊤ \land o \in (T \cap R)) \to o \in (T \cap R)$
197		fvex	$⊢ M (bits \circ ({o ↾}_{J})) \in V$
198		eqid	$⊢ (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J}))) = (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J})))$
199	198	fvmpt2	$⊢ (o \in (T \cap R) \land M (bits \circ ({o ↾}_{J})) \in V) \to (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J}))) (o) = M (bits \circ ({o ↾}_{J}))$
200	196 197 199	sylancl	$⊢ (⊤ \land o \in (T \cap R)) \to (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J}))) (o) = M (bits \circ ({o ↾}_{J}))$
201		f1of	$⊢ (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J}))) : T \cap R \underset{1-1 onto}{⟶} 𝒫 (J \times ℕ_{0}) \cap Fin \to (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J}))) : T \cap R ⟶ 𝒫 (J \times ℕ_{0}) \cap Fin$
202	193 201	mp1i	$⊢ ⊤ \to (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J}))) : T \cap R ⟶ 𝒫 (J \times ℕ_{0}) \cap Fin$
203	202	ffvelrnda	$⊢ (⊤ \land o \in (T \cap R)) \to (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J}))) (o) \in (𝒫 (J \times ℕ_{0}) \cap Fin)$
204	200 203	eqeltrrd	$⊢ (⊤ \land o \in (T \cap R)) \to M (bits \circ ({o ↾}_{J})) \in (𝒫 (J \times ℕ_{0}) \cap Fin)$
205		eqidd	$⊢ ⊤ \to (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J}))) = (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J})))$
206		eqidd	$⊢ ⊤ \to (a \in (𝒫 (J \times ℕ_{0}) \cap Fin) ⟼ F [a]) = (a \in (𝒫 (J \times ℕ_{0}) \cap Fin) ⟼ F [a])$
207		imaeq2	$⊢ a = M (bits \circ ({o ↾}_{J})) \to F [a] = F [M (bits \circ ({o ↾}_{J}))]$
208	204 205 206 207	fmptco	$⊢ ⊤ \to (a \in (𝒫 (J \times ℕ_{0}) \cap Fin) ⟼ F [a]) \circ (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J}))) = (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))])$
209	208	mptru	$⊢ (a \in (𝒫 (J \times ℕ_{0}) \cap Fin) ⟼ F [a]) \circ (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J}))) = (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))])$
210		f1oeq1	$⊢ (a \in (𝒫 (J \times ℕ_{0}) \cap Fin) ⟼ F [a]) \circ (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J}))) = (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))]) \to (((a \in (𝒫 (J \times ℕ_{0}) \cap Fin) ⟼ F [a]) \circ (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J})))) : T \cap R \underset{1-1 onto}{⟶} 𝒫 ℕ \cap Fin \leftrightarrow (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))]) : T \cap R \underset{1-1 onto}{⟶} 𝒫 ℕ \cap Fin)$
211	209 210	ax-mp	$⊢ ((a \in (𝒫 (J \times ℕ_{0}) \cap Fin) ⟼ F [a]) \circ (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J})))) : T \cap R \underset{1-1 onto}{⟶} 𝒫 ℕ \cap Fin \leftrightarrow (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))]) : T \cap R \underset{1-1 onto}{⟶} 𝒫 ℕ \cap Fin$
212	195 211	mpbi	$⊢ (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))]) : T \cap R \underset{1-1 onto}{⟶} 𝒫 ℕ \cap Fin$
213		f1oco	$⊢ (({𝟙_{ℕ} ↾}_{Fin}) : 𝒫 ℕ \cap Fin \underset{1-1 onto}{⟶} ({\{0, 1\}}^{ℕ}) \cap R \land (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))]) : T \cap R \underset{1-1 onto}{⟶} 𝒫 ℕ \cap Fin) \to (({𝟙_{ℕ} ↾}_{Fin}) \circ (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))])) : T \cap R \underset{1-1 onto}{⟶} ({\{0, 1\}}^{ℕ}) \cap R$
214	49 212 213	mp2an	$⊢ (({𝟙_{ℕ} ↾}_{Fin}) \circ (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))])) : T \cap R \underset{1-1 onto}{⟶} ({\{0, 1\}}^{ℕ}) \cap R$
215	5	mpoexg	$⊢ (J \in V \land ℕ_{0} \in V) \to F \in V$
216	56 58 215	mp2an	$⊢ F \in V$
217		imaexg	$⊢ F \in V \to F [M (bits \circ ({o ↾}_{J}))] \in V$
218	216 217	ax-mp	$⊢ F [M (bits \circ ({o ↾}_{J}))] \in V$
219		eqid	$⊢ (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))]) = (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))])$
220	219	fvmpt2	$⊢ (o \in (T \cap R) \land F [M (bits \circ ({o ↾}_{J}))] \in V) \to (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))]) (o) = F [M (bits \circ ({o ↾}_{J}))]$
221	196 218 220	sylancl	$⊢ (⊤ \land o \in (T \cap R)) \to (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))]) (o) = F [M (bits \circ ({o ↾}_{J}))]$
222		f1of	$⊢ (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))]) : T \cap R \underset{1-1 onto}{⟶} 𝒫 ℕ \cap Fin \to (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))]) : T \cap R ⟶ 𝒫 ℕ \cap Fin$
223	212 222	mp1i	$⊢ ⊤ \to (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))]) : T \cap R ⟶ 𝒫 ℕ \cap Fin$
224	223	ffvelrnda	$⊢ (⊤ \land o \in (T \cap R)) \to (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))]) (o) \in (𝒫 ℕ \cap Fin)$
225	221 224	eqeltrrd	$⊢ (⊤ \land o \in (T \cap R)) \to F [M (bits \circ ({o ↾}_{J}))] \in (𝒫 ℕ \cap Fin)$
226		eqidd	$⊢ ⊤ \to (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))]) = (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))])$
227		indf1o	$⊢ ℕ \in V \to 𝟙_{ℕ} : 𝒫 ℕ \underset{1-1 onto}{⟶} {\{0, 1\}}^{ℕ}$
228		f1ofn	$⊢ 𝟙_{ℕ} : 𝒫 ℕ \underset{1-1 onto}{⟶} {\{0, 1\}}^{ℕ} \to 𝟙_{ℕ} Fn 𝒫 ℕ$
229	11 227 228	mp2b	$⊢ 𝟙_{ℕ} Fn 𝒫 ℕ$
230		dffn5	$⊢ 𝟙_{ℕ} Fn 𝒫 ℕ \leftrightarrow 𝟙_{ℕ} = (b \in 𝒫 ℕ ⟼ 𝟙_{ℕ} (b))$
231	229 230	mpbi	$⊢ 𝟙_{ℕ} = (b \in 𝒫 ℕ ⟼ 𝟙_{ℕ} (b))$
232	231	reseq1i	$⊢ {𝟙_{ℕ} ↾}_{Fin} = {(b \in 𝒫 ℕ ⟼ 𝟙_{ℕ} (b)) ↾}_{Fin}$
233		resmpt3	$⊢ {(b \in 𝒫 ℕ ⟼ 𝟙_{ℕ} (b)) ↾}_{Fin} = (b \in (𝒫 ℕ \cap Fin) ⟼ 𝟙_{ℕ} (b))$
234	232 233	eqtri	$⊢ {𝟙_{ℕ} ↾}_{Fin} = (b \in (𝒫 ℕ \cap Fin) ⟼ 𝟙_{ℕ} (b))$
235	234	a1i	$⊢ ⊤ \to {𝟙_{ℕ} ↾}_{Fin} = (b \in (𝒫 ℕ \cap Fin) ⟼ 𝟙_{ℕ} (b))$
236		fveq2	$⊢ b = F [M (bits \circ ({o ↾}_{J}))] \to 𝟙_{ℕ} (b) = 𝟙_{ℕ} (F [M (bits \circ ({o ↾}_{J}))])$
237	225 226 235 236	fmptco	$⊢ ⊤ \to ({𝟙_{ℕ} ↾}_{Fin}) \circ (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))]) = (o \in (T \cap R) ⟼ 𝟙_{ℕ} (F [M (bits \circ ({o ↾}_{J}))]))$
238	237	mptru	$⊢ ({𝟙_{ℕ} ↾}_{Fin}) \circ (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))]) = (o \in (T \cap R) ⟼ 𝟙_{ℕ} (F [M (bits \circ ({o ↾}_{J}))]))$
239	10 238	eqtr4i	$⊢ G = ({𝟙_{ℕ} ↾}_{Fin}) \circ (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))])$
240		f1oeq1	$⊢ G = ({𝟙_{ℕ} ↾}_{Fin}) \circ (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))]) \to (G : T \cap R \underset{1-1 onto}{⟶} ({\{0, 1\}}^{ℕ}) \cap R \leftrightarrow (({𝟙_{ℕ} ↾}_{Fin}) \circ (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))])) : T \cap R \underset{1-1 onto}{⟶} ({\{0, 1\}}^{ℕ}) \cap R)$
241	239 240	ax-mp	$⊢ G : T \cap R \underset{1-1 onto}{⟶} ({\{0, 1\}}^{ℕ}) \cap R \leftrightarrow (({𝟙_{ℕ} ↾}_{Fin}) \circ (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))])) : T \cap R \underset{1-1 onto}{⟶} ({\{0, 1\}}^{ℕ}) \cap R$
242	214 241	mpbir	$⊢ G : T \cap R \underset{1-1 onto}{⟶} ({\{0, 1\}}^{ℕ}) \cap R$

Metamath Proof Explorer

Theorem eulerpartgbij

Proof