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		fcdmnn0supp	$⊢ (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	94 69 95 96	4syl	$⊢ f \in (({ℕ_{0}}^{J}) \cap R) \to ({bits ↾}_{ℕ_{0}}) \circ f = bits \circ f$
98	97	mpteq2ia	$⊢ (f \in (({ℕ_{0}}^{J}) \cap R) ⟼ ({bits ↾}_{ℕ_{0}}) \circ f) = (f \in (({ℕ_{0}}^{J}) \cap R) ⟼ bits \circ f)$
99	98	eqcomi	$⊢ (f \in (({ℕ_{0}}^{J}) \cap R) ⟼ bits \circ f) = (f \in (({ℕ_{0}}^{J}) \cap R) ⟼ ({bits ↾}_{ℕ_{0}}) \circ f)$
100		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\})$
101	99 100	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\})$
102	93 101	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\}$
103	102	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\}$
104		ssrab2	$⊢ \{z \in ℕ \| \neg 2 ∥ z\} \subseteq ℕ$
105	4 104	eqsstri	$⊢ J \subseteq ℕ$
106	11 58 105	3pm3.2i	$⊢ (ℕ \in V \land ℕ_{0} \in V \land J \subseteq ℕ)$
107		cnveq	$⊢ f = o \to f^{-1} = o^{-1}$
108		dfn2	$⊢ ℕ = ℕ_{0} ∖ \{0\}$
109	108	a1i	$⊢ f = o \to ℕ = ℕ_{0} ∖ \{0\}$
110	107 109	imaeq12d	$⊢ f = o \to f^{-1} [ℕ] = o^{-1} [ℕ_{0} ∖ \{0\}]$
111	110	sseq1d	$⊢ f = o \to (f^{-1} [ℕ] \subseteq J \leftrightarrow o^{-1} [ℕ_{0} ∖ \{0\}] \subseteq J)$
112	111	cbvrabv	$⊢ \{f \in ({ℕ_{0}}^{ℕ}) \| f^{-1} [ℕ] \subseteq J\} = \{o \in ({ℕ_{0}}^{ℕ}) \| o^{-1} [ℕ_{0} ∖ \{0\}] \subseteq J\}$
113	9 112	eqtri	$⊢ T = \{o \in ({ℕ_{0}}^{ℕ}) \| o^{-1} [ℕ_{0} ∖ \{0\}] \subseteq J\}$
114		eqid	$⊢ (o \in T ⟼ {o ↾}_{J}) = (o \in T ⟼ {o ↾}_{J})$
115	113 114	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}$
116	106 63 115	mp2an	$⊢ (o \in T ⟼ {o ↾}_{J}) : T \underset{1-1 onto}{⟶} {ℕ_{0}}^{J}$
117		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}$
118	116 117	ax-mp	$⊢ (o \in T ⟼ {o ↾}_{J}) : T \underset{1-1}{⟶} {ℕ_{0}}^{J}$
119		inss1	$⊢ T \cap R \subseteq T$
120		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]$
121	118 119 120	mp2an	$⊢ ({(o \in T ⟼ {o ↾}_{J}) ↾}_{(T \cap R)}) : T \cap R \underset{1-1 onto}{⟶} (o \in T ⟼ {o ↾}_{J}) [T \cap R]$
122		vex	$⊢ o \in V$
123	122	resex	$⊢ {o ↾}_{J} \in V$
124	123 114	fnmpti	$⊢ (o \in T ⟼ {o ↾}_{J}) Fn T$
125		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)$
126	124 119 125	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$
127		eqid	$⊢ (m \in (T \cap R) ⟼ {m ↾}_{J}) = (m \in (T \cap R) ⟼ {m ↾}_{J})$
128		vex	$⊢ m \in V$
129	128	resex	$⊢ {m ↾}_{J} \in V$
130	127 129	elrnmpti	$⊢ f \in ran (m \in (T \cap R) ⟼ {m ↾}_{J}) \leftrightarrow \exists m \in (T \cap R) f = {m ↾}_{J}$
131	1 2 3 4 5 6 7 8 9	eulerpartlemt	$⊢ ({ℕ_{0}}^{J}) \cap R = ran (m \in (T \cap R) ⟼ {m ↾}_{J})$
132	131	eleq2i	$⊢ f \in (({ℕ_{0}}^{J}) \cap R) \leftrightarrow f \in ran (m \in (T \cap R) ⟼ {m ↾}_{J})$
133		elinel1	$⊢ m \in (T \cap R) \to m \in T$
134	114	fvtresfn	$⊢ m \in T \to (o \in T ⟼ {o ↾}_{J}) (m) = {m ↾}_{J}$
135	134	eqeq1d	$⊢ m \in T \to ((o \in T ⟼ {o ↾}_{J}) (m) = f \leftrightarrow {m ↾}_{J} = f)$
136	133 135	syl	$⊢ m \in (T \cap R) \to ((o \in T ⟼ {o ↾}_{J}) (m) = f \leftrightarrow {m ↾}_{J} = f)$
137		eqcom	$⊢ {m ↾}_{J} = f \leftrightarrow f = {m ↾}_{J}$
138	136 137	bitrdi	$⊢ m \in (T \cap R) \to ((o \in T ⟼ {o ↾}_{J}) (m) = f \leftrightarrow f = {m ↾}_{J})$
139	138	rexbiia	$⊢ \exists m \in (T \cap R) (o \in T ⟼ {o ↾}_{J}) (m) = f \leftrightarrow \exists m \in (T \cap R) f = {m ↾}_{J}$
140	130 132 139	3bitr4ri	$⊢ \exists m \in (T \cap R) (o \in T ⟼ {o ↾}_{J}) (m) = f \leftrightarrow f \in (({ℕ_{0}}^{J}) \cap R)$
141	126 140	bitri	$⊢ f \in (o \in T ⟼ {o ↾}_{J}) [T \cap R] \leftrightarrow f \in (({ℕ_{0}}^{J}) \cap R)$
142	141	eqriv	$⊢ (o \in T ⟼ {o ↾}_{J}) [T \cap R] = ({ℕ_{0}}^{J}) \cap R$
143		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)$
144	142 143	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$
145		resmpt	$⊢ T \cap R \subseteq T \to {(o \in T ⟼ {o ↾}_{J}) ↾}_{(T \cap R)} = (o \in (T \cap R) ⟼ {o ↾}_{J})$
146		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)$
147	119 145 146	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$
148	144 147	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$
149	121 148	mpbi	$⊢ (o \in (T \cap R) ⟼ {o ↾}_{J}) : T \cap R \underset{1-1 onto}{⟶} ({ℕ_{0}}^{J}) \cap R$
150		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\}$
151	103 149 150	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\}$
152		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$
153		eqid	$⊢ (o \in (T \cap R) ⟼ {o ↾}_{J}) = (o \in (T \cap R) ⟼ {o ↾}_{J})$
154	153	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$
155	154	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)$
156	149 152 155	mp2b	$⊢ \forall o \in (T \cap R) {o ↾}_{J} \in (({ℕ_{0}}^{J}) \cap R)$
157	156	a1i	$⊢ ⊤ \to \forall o \in (T \cap R) {o ↾}_{J} \in (({ℕ_{0}}^{J}) \cap R)$
158		eqidd	$⊢ ⊤ \to (o \in (T \cap R) ⟼ {o ↾}_{J}) = (o \in (T \cap R) ⟼ {o ↾}_{J})$
159		eqidd	$⊢ ⊤ \to (f \in (({ℕ_{0}}^{J}) \cap R) ⟼ bits \circ f) = (f \in (({ℕ_{0}}^{J}) \cap R) ⟼ bits \circ f)$
160		coeq2	$⊢ f = {o ↾}_{J} \to bits \circ f = bits \circ ({o ↾}_{J})$
161	157 158 159 160	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}))$
162	161	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})$
163		eqidd	$⊢ ⊤ \to T \cap R = T \cap R$
164	6	a1i	$⊢ ⊤ \to H = \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{J}) \| r supp \emptyset \in Fin\}$
165	162 163 164	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\})$
166	151 165	mpbiri	$⊢ ⊤ \to (o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J})) : T \cap R \underset{1-1 onto}{⟶} H$
167	166	mptru	$⊢ (o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J})) : T \cap R \underset{1-1 onto}{⟶} H$
168		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$
169	53 167 168	mp2an	$⊢ (M \circ (o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J}))) : T \cap R \underset{1-1 onto}{⟶} 𝒫 (J \times ℕ_{0}) \cap Fin$
170		eqidd	$⊢ ⊤ \to (o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J})) = (o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J}))$
171		bitsf	$⊢ bits : ℤ ⟶ 𝒫 ℕ_{0}$
172		zex	$⊢ ℤ \in V$
173		fex	$⊢ (bits : ℤ ⟶ 𝒫 ℕ_{0} \land ℤ \in V) \to bits \in V$
174	171 172 173	mp2an	$⊢ bits \in V$
175	174 123	coex	$⊢ bits \circ ({o ↾}_{J}) \in V$
176	175	a1i	$⊢ (⊤ \land o \in (T \cap R)) \to bits \circ ({o ↾}_{J}) \in V$
177	170 176	fvmpt2d	$⊢ (⊤ \land o \in (T \cap R)) \to (o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J})) (o) = bits \circ ({o ↾}_{J})$
178		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$
179	166 178	syl	$⊢ ⊤ \to (o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J})) : T \cap R ⟶ H$
180	179	ffvelcdmda	$⊢ (⊤ \land o \in (T \cap R)) \to (o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J})) (o) \in H$
181	177 180	eqeltrrd	$⊢ (⊤ \land o \in (T \cap R)) \to bits \circ ({o ↾}_{J}) \in H$
182		f1ofn	$⊢ M : H \underset{1-1 onto}{⟶} 𝒫 (J \times ℕ_{0}) \cap Fin \to M Fn H$
183	53 182	ax-mp	$⊢ M Fn H$
184		dffn5	$⊢ M Fn H \leftrightarrow M = (r \in H ⟼ M (r))$
185	183 184	mpbi	$⊢ M = (r \in H ⟼ M (r))$
186	185	a1i	$⊢ ⊤ \to M = (r \in H ⟼ M (r))$
187		fveq2	$⊢ r = bits \circ ({o ↾}_{J}) \to M (r) = M (bits \circ ({o ↾}_{J}))$
188	181 170 186 187	fmptco	$⊢ ⊤ \to M \circ (o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J})) = (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J})))$
189	188	mptru	$⊢ M \circ (o \in (T \cap R) ⟼ bits \circ ({o ↾}_{J})) = (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J})))$
190		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)$
191	189 190	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$
192	169 191	mpbi	$⊢ (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J}))) : T \cap R \underset{1-1 onto}{⟶} 𝒫 (J \times ℕ_{0}) \cap Fin$
193		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$
194	52 192 193	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$
195		simpr	$⊢ (⊤ \land o \in (T \cap R)) \to o \in (T \cap R)$
196		fvex	$⊢ M (bits \circ ({o ↾}_{J})) \in V$
197		eqid	$⊢ (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J}))) = (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J})))$
198	197	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}))$
199	195 196 198	sylancl	$⊢ (⊤ \land o \in (T \cap R)) \to (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J}))) (o) = M (bits \circ ({o ↾}_{J}))$
200		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$
201	192 200	mp1i	$⊢ ⊤ \to (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J}))) : T \cap R ⟶ 𝒫 (J \times ℕ_{0}) \cap Fin$
202	201	ffvelcdmda	$⊢ (⊤ \land o \in (T \cap R)) \to (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J}))) (o) \in (𝒫 (J \times ℕ_{0}) \cap Fin)$
203	199 202	eqeltrrd	$⊢ (⊤ \land o \in (T \cap R)) \to M (bits \circ ({o ↾}_{J})) \in (𝒫 (J \times ℕ_{0}) \cap Fin)$
204		eqidd	$⊢ ⊤ \to (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J}))) = (o \in (T \cap R) ⟼ M (bits \circ ({o ↾}_{J})))$
205		eqidd	$⊢ ⊤ \to (a \in (𝒫 (J \times ℕ_{0}) \cap Fin) ⟼ F [a]) = (a \in (𝒫 (J \times ℕ_{0}) \cap Fin) ⟼ F [a])$
206		imaeq2	$⊢ a = M (bits \circ ({o ↾}_{J})) \to F [a] = F [M (bits \circ ({o ↾}_{J}))]$
207	203 204 205 206	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}))])$
208	207	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}))])$
209		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)$
210	208 209	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$
211	194 210	mpbi	$⊢ (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))]) : T \cap R \underset{1-1 onto}{⟶} 𝒫 ℕ \cap Fin$
212		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$
213	49 211 212	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$
214	5	mpoexg	$⊢ (J \in V \land ℕ_{0} \in V) \to F \in V$
215	56 58 214	mp2an	$⊢ F \in V$
216		imaexg	$⊢ F \in V \to F [M (bits \circ ({o ↾}_{J}))] \in V$
217	215 216	ax-mp	$⊢ F [M (bits \circ ({o ↾}_{J}))] \in V$
218		eqid	$⊢ (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))]) = (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))])$
219	218	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}))]$
220	195 217 219	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}))]$
221		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$
222	211 221	mp1i	$⊢ ⊤ \to (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))]) : T \cap R ⟶ 𝒫 ℕ \cap Fin$
223	222	ffvelcdmda	$⊢ (⊤ \land o \in (T \cap R)) \to (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))]) (o) \in (𝒫 ℕ \cap Fin)$
224	220 223	eqeltrrd	$⊢ (⊤ \land o \in (T \cap R)) \to F [M (bits \circ ({o ↾}_{J}))] \in (𝒫 ℕ \cap Fin)$
225		eqidd	$⊢ ⊤ \to (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))]) = (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))])$
226		indf1o	$⊢ ℕ \in V \to 𝟙_{ℕ} : 𝒫 ℕ \underset{1-1 onto}{⟶} {\{0, 1\}}^{ℕ}$
227		f1ofn	$⊢ 𝟙_{ℕ} : 𝒫 ℕ \underset{1-1 onto}{⟶} {\{0, 1\}}^{ℕ} \to 𝟙_{ℕ} Fn 𝒫 ℕ$
228	11 226 227	mp2b	$⊢ 𝟙_{ℕ} Fn 𝒫 ℕ$
229		dffn5	$⊢ 𝟙_{ℕ} Fn 𝒫 ℕ \leftrightarrow 𝟙_{ℕ} = (b \in 𝒫 ℕ ⟼ 𝟙_{ℕ} (b))$
230	228 229	mpbi	$⊢ 𝟙_{ℕ} = (b \in 𝒫 ℕ ⟼ 𝟙_{ℕ} (b))$
231	230	reseq1i	$⊢ {𝟙_{ℕ} ↾}_{Fin} = {(b \in 𝒫 ℕ ⟼ 𝟙_{ℕ} (b)) ↾}_{Fin}$
232		resmpt3	$⊢ {(b \in 𝒫 ℕ ⟼ 𝟙_{ℕ} (b)) ↾}_{Fin} = (b \in (𝒫 ℕ \cap Fin) ⟼ 𝟙_{ℕ} (b))$
233	231 232	eqtri	$⊢ {𝟙_{ℕ} ↾}_{Fin} = (b \in (𝒫 ℕ \cap Fin) ⟼ 𝟙_{ℕ} (b))$
234	233	a1i	$⊢ ⊤ \to {𝟙_{ℕ} ↾}_{Fin} = (b \in (𝒫 ℕ \cap Fin) ⟼ 𝟙_{ℕ} (b))$
235		fveq2	$⊢ b = F [M (bits \circ ({o ↾}_{J}))] \to 𝟙_{ℕ} (b) = 𝟙_{ℕ} (F [M (bits \circ ({o ↾}_{J}))])$
236	224 225 234 235	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}))]))$
237	236	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}))]))$
238	10 237	eqtr4i	$⊢ G = ({𝟙_{ℕ} ↾}_{Fin}) \circ (o \in (T \cap R) ⟼ F [M (bits \circ ({o ↾}_{J}))])$
239		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)$
240	238 239	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$
241	213 240	mpbir	$⊢ G : T \cap R \underset{1-1 onto}{⟶} ({\{0, 1\}}^{ℕ}) \cap R$

Metamath Proof Explorer

Theorem eulerpartgbij

Proof