eulerpartlemgh

Description: Lemma for eulerpart : The F function is a bijection on the U subsets. (Contributed by Thierry Arnoux, 15-Aug-2018)

	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}))]))$
	eulerpartlemgh.1	$⊢ U = ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t)))$
Assertion	eulerpartlemgh	$⊢ A \in (T \cap R) \to ({F ↾}_{U}) : U \underset{1-1 onto}{⟶} \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\}$

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		eulerpartlemgh.1	$⊢ U = ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t)))$
12	4 5	oddpwdc	$⊢ F : J \times ℕ_{0} \underset{1-1 onto}{⟶} ℕ$
13		f1of1	$⊢ F : J \times ℕ_{0} \underset{1-1 onto}{⟶} ℕ \to F : J \times ℕ_{0} \underset{1-1}{⟶} ℕ$
14	12 13	ax-mp	$⊢ F : J \times ℕ_{0} \underset{1-1}{⟶} ℕ$
15		iunss	$⊢ ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t))) \subseteq J \times ℕ_{0} \leftrightarrow \forall t \in (A^{-1} [ℕ] \cap J) \{t\} \times bits (A (t)) \subseteq J \times ℕ_{0}$
16		inss2	$⊢ A^{-1} [ℕ] \cap J \subseteq J$
17	16	sseli	$⊢ t \in (A^{-1} [ℕ] \cap J) \to t \in J$
18	17	snssd	$⊢ t \in (A^{-1} [ℕ] \cap J) \to \{t\} \subseteq J$
19		bitsss	$⊢ bits (A (t)) \subseteq ℕ_{0}$
20		xpss12	$⊢ (\{t\} \subseteq J \land bits (A (t)) \subseteq ℕ_{0}) \to \{t\} \times bits (A (t)) \subseteq J \times ℕ_{0}$
21	18 19 20	sylancl	$⊢ t \in (A^{-1} [ℕ] \cap J) \to \{t\} \times bits (A (t)) \subseteq J \times ℕ_{0}$
22	15 21	mprgbir	$⊢ ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t))) \subseteq J \times ℕ_{0}$
23	11 22	eqsstri	$⊢ U \subseteq J \times ℕ_{0}$
24		f1ores	$⊢ (F : J \times ℕ_{0} \underset{1-1}{⟶} ℕ \land U \subseteq J \times ℕ_{0}) \to ({F ↾}_{U}) : U \underset{1-1 onto}{⟶} F [U]$
25	14 23 24	mp2an	$⊢ ({F ↾}_{U}) : U \underset{1-1 onto}{⟶} F [U]$
26		simpr	$⊢ (((A \in (T \cap R) \land t \in ℕ) \land n \in bits (A (t))) \land 2^{n} t = p) \to 2^{n} t = p$
27		2nn	$⊢ 2 \in ℕ$
28	27	a1i	$⊢ ((A \in (T \cap R) \land t \in ℕ) \land n \in bits (A (t))) \to 2 \in ℕ$
29	19	sseli	$⊢ n \in bits (A (t)) \to n \in ℕ_{0}$
30	29	adantl	$⊢ ((A \in (T \cap R) \land t \in ℕ) \land n \in bits (A (t))) \to n \in ℕ_{0}$
31	28 30	nnexpcld	$⊢ ((A \in (T \cap R) \land t \in ℕ) \land n \in bits (A (t))) \to 2^{n} \in ℕ$
32		simplr	$⊢ ((A \in (T \cap R) \land t \in ℕ) \land n \in bits (A (t))) \to t \in ℕ$
33	31 32	nnmulcld	$⊢ ((A \in (T \cap R) \land t \in ℕ) \land n \in bits (A (t))) \to 2^{n} t \in ℕ$
34	33	adantr	$⊢ (((A \in (T \cap R) \land t \in ℕ) \land n \in bits (A (t))) \land 2^{n} t = p) \to 2^{n} t \in ℕ$
35	26 34	eqeltrrd	$⊢ (((A \in (T \cap R) \land t \in ℕ) \land n \in bits (A (t))) \land 2^{n} t = p) \to p \in ℕ$
36	35	rexlimdva2	$⊢ (A \in (T \cap R) \land t \in ℕ) \to (\exists n \in bits (A (t)) 2^{n} t = p \to p \in ℕ)$
37	36	rexlimdva	$⊢ A \in (T \cap R) \to (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = p \to p \in ℕ)$
38	37	pm4.71rd	$⊢ A \in (T \cap R) \to (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = p \leftrightarrow (p \in ℕ \land \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = p))$
39		rex0	$⊢ \neg \exists n \in \emptyset 2^{n} t = p$
40		simplr	$⊢ ((A \in (T \cap R) \land t \in ℕ) \land \neg t \in A^{-1} [ℕ]) \to t \in ℕ$
41		simpr	$⊢ ((A \in (T \cap R) \land t \in ℕ) \land \neg t \in A^{-1} [ℕ]) \to \neg t \in A^{-1} [ℕ]$
42	1 2 3 4 5 6 7 8 9	eulerpartlemt0	$⊢ A \in (T \cap R) \leftrightarrow (A \in ({ℕ_{0}}^{ℕ}) \land A^{-1} [ℕ] \in Fin \land A^{-1} [ℕ] \subseteq J)$
43	42	simp1bi	$⊢ A \in (T \cap R) \to A \in ({ℕ_{0}}^{ℕ})$
44		elmapi	$⊢ A \in ({ℕ_{0}}^{ℕ}) \to A : ℕ ⟶ ℕ_{0}$
45	43 44	syl	$⊢ A \in (T \cap R) \to A : ℕ ⟶ ℕ_{0}$
46	45	ad2antrr	$⊢ ((A \in (T \cap R) \land t \in ℕ) \land \neg t \in A^{-1} [ℕ]) \to A : ℕ ⟶ ℕ_{0}$
47		ffn	$⊢ A : ℕ ⟶ ℕ_{0} \to A Fn ℕ$
48		elpreima	$⊢ A Fn ℕ \to (t \in A^{-1} [ℕ] \leftrightarrow (t \in ℕ \land A (t) \in ℕ))$
49	46 47 48	3syl	$⊢ ((A \in (T \cap R) \land t \in ℕ) \land \neg t \in A^{-1} [ℕ]) \to (t \in A^{-1} [ℕ] \leftrightarrow (t \in ℕ \land A (t) \in ℕ))$
50	41 49	mtbid	$⊢ ((A \in (T \cap R) \land t \in ℕ) \land \neg t \in A^{-1} [ℕ]) \to \neg (t \in ℕ \land A (t) \in ℕ)$
51		imnan	$⊢ (t \in ℕ \to \neg A (t) \in ℕ) \leftrightarrow \neg (t \in ℕ \land A (t) \in ℕ)$
52	50 51	sylibr	$⊢ ((A \in (T \cap R) \land t \in ℕ) \land \neg t \in A^{-1} [ℕ]) \to (t \in ℕ \to \neg A (t) \in ℕ)$
53	40 52	mpd	$⊢ ((A \in (T \cap R) \land t \in ℕ) \land \neg t \in A^{-1} [ℕ]) \to \neg A (t) \in ℕ$
54	46 40	ffvelcdmd	$⊢ ((A \in (T \cap R) \land t \in ℕ) \land \neg t \in A^{-1} [ℕ]) \to A (t) \in ℕ_{0}$
55		elnn0	$⊢ A (t) \in ℕ_{0} \leftrightarrow (A (t) \in ℕ \lor A (t) = 0)$
56	54 55	sylib	$⊢ ((A \in (T \cap R) \land t \in ℕ) \land \neg t \in A^{-1} [ℕ]) \to (A (t) \in ℕ \lor A (t) = 0)$
57		orel1	$⊢ \neg A (t) \in ℕ \to ((A (t) \in ℕ \lor A (t) = 0) \to A (t) = 0)$
58	53 56 57	sylc	$⊢ ((A \in (T \cap R) \land t \in ℕ) \land \neg t \in A^{-1} [ℕ]) \to A (t) = 0$
59	58	fveq2d	$⊢ ((A \in (T \cap R) \land t \in ℕ) \land \neg t \in A^{-1} [ℕ]) \to bits (A (t)) = bits (0)$
60		0bits	$⊢ bits (0) = \emptyset$
61	59 60	eqtrdi	$⊢ ((A \in (T \cap R) \land t \in ℕ) \land \neg t \in A^{-1} [ℕ]) \to bits (A (t)) = \emptyset$
62	61	rexeqdv	$⊢ ((A \in (T \cap R) \land t \in ℕ) \land \neg t \in A^{-1} [ℕ]) \to (\exists n \in bits (A (t)) 2^{n} t = p \leftrightarrow \exists n \in \emptyset 2^{n} t = p)$
63	39 62	mtbiri	$⊢ ((A \in (T \cap R) \land t \in ℕ) \land \neg t \in A^{-1} [ℕ]) \to \neg \exists n \in bits (A (t)) 2^{n} t = p$
64	63	ex	$⊢ (A \in (T \cap R) \land t \in ℕ) \to (\neg t \in A^{-1} [ℕ] \to \neg \exists n \in bits (A (t)) 2^{n} t = p)$
65	64	con4d	$⊢ (A \in (T \cap R) \land t \in ℕ) \to (\exists n \in bits (A (t)) 2^{n} t = p \to t \in A^{-1} [ℕ])$
66	65	impr	$⊢ (A \in (T \cap R) \land (t \in ℕ \land \exists n \in bits (A (t)) 2^{n} t = p)) \to t \in A^{-1} [ℕ]$
67		eldif	$⊢ t \in (ℕ ∖ J) \leftrightarrow (t \in ℕ \land \neg t \in J)$
68	1 2 3 4 5 6 7 8 9	eulerpartlemf	$⊢ (A \in (T \cap R) \land t \in (ℕ ∖ J)) \to A (t) = 0$
69	67 68	sylan2br	$⊢ (A \in (T \cap R) \land (t \in ℕ \land \neg t \in J)) \to A (t) = 0$
70	69	anassrs	$⊢ ((A \in (T \cap R) \land t \in ℕ) \land \neg t \in J) \to A (t) = 0$
71	70	fveq2d	$⊢ ((A \in (T \cap R) \land t \in ℕ) \land \neg t \in J) \to bits (A (t)) = bits (0)$
72	71 60	eqtrdi	$⊢ ((A \in (T \cap R) \land t \in ℕ) \land \neg t \in J) \to bits (A (t)) = \emptyset$
73	72	rexeqdv	$⊢ ((A \in (T \cap R) \land t \in ℕ) \land \neg t \in J) \to (\exists n \in bits (A (t)) 2^{n} t = p \leftrightarrow \exists n \in \emptyset 2^{n} t = p)$
74	39 73	mtbiri	$⊢ ((A \in (T \cap R) \land t \in ℕ) \land \neg t \in J) \to \neg \exists n \in bits (A (t)) 2^{n} t = p$
75	74	ex	$⊢ (A \in (T \cap R) \land t \in ℕ) \to (\neg t \in J \to \neg \exists n \in bits (A (t)) 2^{n} t = p)$
76	75	con4d	$⊢ (A \in (T \cap R) \land t \in ℕ) \to (\exists n \in bits (A (t)) 2^{n} t = p \to t \in J)$
77	76	impr	$⊢ (A \in (T \cap R) \land (t \in ℕ \land \exists n \in bits (A (t)) 2^{n} t = p)) \to t \in J$
78	66 77	elind	$⊢ (A \in (T \cap R) \land (t \in ℕ \land \exists n \in bits (A (t)) 2^{n} t = p)) \to t \in (A^{-1} [ℕ] \cap J)$
79		simprr	$⊢ (A \in (T \cap R) \land (t \in ℕ \land \exists n \in bits (A (t)) 2^{n} t = p)) \to \exists n \in bits (A (t)) 2^{n} t = p$
80	78 79	jca	$⊢ (A \in (T \cap R) \land (t \in ℕ \land \exists n \in bits (A (t)) 2^{n} t = p)) \to (t \in (A^{-1} [ℕ] \cap J) \land \exists n \in bits (A (t)) 2^{n} t = p)$
81	80	ex	$⊢ A \in (T \cap R) \to ((t \in ℕ \land \exists n \in bits (A (t)) 2^{n} t = p) \to (t \in (A^{-1} [ℕ] \cap J) \land \exists n \in bits (A (t)) 2^{n} t = p))$
82	81	reximdv2	$⊢ A \in (T \cap R) \to (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = p \to \exists t \in (A^{-1} [ℕ] \cap J) \exists n \in bits (A (t)) 2^{n} t = p)$
83		ssrab2	$⊢ \{z \in ℕ \| \neg 2 ∥ z\} \subseteq ℕ$
84	4 83	eqsstri	$⊢ J \subseteq ℕ$
85	16 84	sstri	$⊢ A^{-1} [ℕ] \cap J \subseteq ℕ$
86		ssrexv	$⊢ A^{-1} [ℕ] \cap J \subseteq ℕ \to (\exists t \in (A^{-1} [ℕ] \cap J) \exists n \in bits (A (t)) 2^{n} t = p \to \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = p)$
87	85 86	mp1i	$⊢ A \in (T \cap R) \to (\exists t \in (A^{-1} [ℕ] \cap J) \exists n \in bits (A (t)) 2^{n} t = p \to \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = p)$
88	82 87	impbid	$⊢ A \in (T \cap R) \to (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = p \leftrightarrow \exists t \in (A^{-1} [ℕ] \cap J) \exists n \in bits (A (t)) 2^{n} t = p)$
89	38 88	bitr3d	$⊢ A \in (T \cap R) \to ((p \in ℕ \land \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = p) \leftrightarrow \exists t \in (A^{-1} [ℕ] \cap J) \exists n \in bits (A (t)) 2^{n} t = p)$
90		eqeq2	$⊢ m = p \to (2^{n} t = m \leftrightarrow 2^{n} t = p)$
91	90	2rexbidv	$⊢ m = p \to (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m \leftrightarrow \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = p)$
92	91	elrab	$⊢ p \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\} \leftrightarrow (p \in ℕ \land \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = p)$
93	92	a1i	$⊢ A \in (T \cap R) \to (p \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\} \leftrightarrow (p \in ℕ \land \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = p))$
94	11	imaeq2i	$⊢ F [U] = F [⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t)))]$
95		imaiun	$⊢ F [⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t)))] = ⋃_{t \in A^{-1} [ℕ] \cap J} F [\{t\} \times bits (A (t))]$
96	94 95	eqtri	$⊢ F [U] = ⋃_{t \in A^{-1} [ℕ] \cap J} F [\{t\} \times bits (A (t))]$
97	96	eleq2i	$⊢ p \in F [U] \leftrightarrow p \in ⋃_{t \in A^{-1} [ℕ] \cap J} F [\{t\} \times bits (A (t))]$
98		eliun	$⊢ p \in ⋃_{t \in A^{-1} [ℕ] \cap J} F [\{t\} \times bits (A (t))] \leftrightarrow \exists t \in (A^{-1} [ℕ] \cap J) p \in F [\{t\} \times bits (A (t))]$
99		f1ofn	$⊢ F : J \times ℕ_{0} \underset{1-1 onto}{⟶} ℕ \to F Fn (J \times ℕ_{0})$
100	12 99	ax-mp	$⊢ F Fn (J \times ℕ_{0})$
101		snssi	$⊢ t \in J \to \{t\} \subseteq J$
102	101 19 20	sylancl	$⊢ t \in J \to \{t\} \times bits (A (t)) \subseteq J \times ℕ_{0}$
103		ovelimab	$⊢ (F Fn (J \times ℕ_{0}) \land \{t\} \times bits (A (t)) \subseteq J \times ℕ_{0}) \to (p \in F [\{t\} \times bits (A (t))] \leftrightarrow \exists x \in \{t\} \exists n \in bits (A (t)) p = x F n)$
104	100 102 103	sylancr	$⊢ t \in J \to (p \in F [\{t\} \times bits (A (t))] \leftrightarrow \exists x \in \{t\} \exists n \in bits (A (t)) p = x F n)$
105		vex	$⊢ t \in V$
106		oveq1	$⊢ x = t \to x F n = t F n$
107	106	eqeq2d	$⊢ x = t \to (p = x F n \leftrightarrow p = t F n)$
108	107	rexbidv	$⊢ x = t \to (\exists n \in bits (A (t)) p = x F n \leftrightarrow \exists n \in bits (A (t)) p = t F n)$
109	105 108	rexsn	$⊢ \exists x \in \{t\} \exists n \in bits (A (t)) p = x F n \leftrightarrow \exists n \in bits (A (t)) p = t F n$
110	104 109	bitrdi	$⊢ t \in J \to (p \in F [\{t\} \times bits (A (t))] \leftrightarrow \exists n \in bits (A (t)) p = t F n)$
111		df-ov	$⊢ t F n = F (⟨t, n⟩)$
112	111	eqeq1i	$⊢ t F n = p \leftrightarrow F (⟨t, n⟩) = p$
113		eqcom	$⊢ t F n = p \leftrightarrow p = t F n$
114	112 113	bitr3i	$⊢ F (⟨t, n⟩) = p \leftrightarrow p = t F n$
115		opelxpi	$⊢ (t \in J \land n \in ℕ_{0}) \to ⟨t, n⟩ \in (J \times ℕ_{0})$
116	4 5	oddpwdcv	$⊢ ⟨t, n⟩ \in (J \times ℕ_{0}) \to F (⟨t, n⟩) = 2^{2^{nd} (⟨t, n⟩)} 1^{st} (⟨t, n⟩)$
117		vex	$⊢ n \in V$
118	105 117	op2nd	$⊢ 2^{nd} (⟨t, n⟩) = n$
119	118	oveq2i	$⊢ 2^{2^{nd} (⟨t, n⟩)} = 2^{n}$
120	105 117	op1st	$⊢ 1^{st} (⟨t, n⟩) = t$
121	119 120	oveq12i	$⊢ 2^{2^{nd} (⟨t, n⟩)} 1^{st} (⟨t, n⟩) = 2^{n} t$
122	116 121	eqtrdi	$⊢ ⟨t, n⟩ \in (J \times ℕ_{0}) \to F (⟨t, n⟩) = 2^{n} t$
123	115 122	syl	$⊢ (t \in J \land n \in ℕ_{0}) \to F (⟨t, n⟩) = 2^{n} t$
124	123	eqeq1d	$⊢ (t \in J \land n \in ℕ_{0}) \to (F (⟨t, n⟩) = p \leftrightarrow 2^{n} t = p)$
125	114 124	bitr3id	$⊢ (t \in J \land n \in ℕ_{0}) \to (p = t F n \leftrightarrow 2^{n} t = p)$
126	29 125	sylan2	$⊢ (t \in J \land n \in bits (A (t))) \to (p = t F n \leftrightarrow 2^{n} t = p)$
127	126	rexbidva	$⊢ t \in J \to (\exists n \in bits (A (t)) p = t F n \leftrightarrow \exists n \in bits (A (t)) 2^{n} t = p)$
128	110 127	bitrd	$⊢ t \in J \to (p \in F [\{t\} \times bits (A (t))] \leftrightarrow \exists n \in bits (A (t)) 2^{n} t = p)$
129	17 128	syl	$⊢ t \in (A^{-1} [ℕ] \cap J) \to (p \in F [\{t\} \times bits (A (t))] \leftrightarrow \exists n \in bits (A (t)) 2^{n} t = p)$
130	129	rexbiia	$⊢ \exists t \in (A^{-1} [ℕ] \cap J) p \in F [\{t\} \times bits (A (t))] \leftrightarrow \exists t \in (A^{-1} [ℕ] \cap J) \exists n \in bits (A (t)) 2^{n} t = p$
131	97 98 130	3bitri	$⊢ p \in F [U] \leftrightarrow \exists t \in (A^{-1} [ℕ] \cap J) \exists n \in bits (A (t)) 2^{n} t = p$
132	131	a1i	$⊢ A \in (T \cap R) \to (p \in F [U] \leftrightarrow \exists t \in (A^{-1} [ℕ] \cap J) \exists n \in bits (A (t)) 2^{n} t = p)$
133	89 93 132	3bitr4rd	$⊢ A \in (T \cap R) \to (p \in F [U] \leftrightarrow p \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\})$
134	133	eqrdv	$⊢ A \in (T \cap R) \to F [U] = \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\}$
135		f1oeq3	$⊢ F [U] = \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\} \to (({F ↾}_{U}) : U \underset{1-1 onto}{⟶} F [U] \leftrightarrow ({F ↾}_{U}) : U \underset{1-1 onto}{⟶} \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\})$
136	134 135	syl	$⊢ A \in (T \cap R) \to (({F ↾}_{U}) : U \underset{1-1 onto}{⟶} F [U] \leftrightarrow ({F ↾}_{U}) : U \underset{1-1 onto}{⟶} \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\})$
137	25 136	mpbii	$⊢ A \in (T \cap R) \to ({F ↾}_{U}) : U \underset{1-1 onto}{⟶} \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\}$

Metamath Proof Explorer

Theorem eulerpartlemgh

Proof