Theorem eulerpartgbij 29207

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

Hypotheses

Ref	Expression
eulerpart.p	|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }
eulerpart.o	|- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }
eulerpart.d	|- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }
eulerpart.j	|- J = { z e. NN | -. 2 || z }
eulerpart.f	|- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )
eulerpart.h	|- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }
eulerpart.m	|- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )
eulerpart.r	|- R = { f | ( `' f " NN ) e. Fin }
eulerpart.t	|- T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }
eulerpart.g	|- G = ( o e. ( T i^i R ) |-> ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )

Assertion

Ref	Expression
eulerpartgbij	|- G : ( T i^i R ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R )

Distinct variable groups:   f, g, k, n, o, x, y, z   o, F   f, r, J, o, x, y   o, M, r   f, N, g, x   P, g   R, f, o   o, H, r   T, f, o

Allowed substitution hints:   D( x, y, z, f, g, k, n, o, r)   P( x, y, z, f, k, n, o, r)   R( x, y, z, g, k, n, r)   T( x, y, z, g, k, n, r)   F( x, y, z, f, g, k, n, r)   G( x, y, z, f, g, k, n, o, r)   H( x, y, z, f, g, k, n)   J( z, g, k, n)   M( x, y, z, f, g, k, n)   N( y, z, k, n, o, r)   O( x, y, z, f, g, k, n, o, r)

Proof of Theorem eulerpartgbij

Dummy variables a m b are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnex 10617	. . . . 5 |- NN e. _V
2		indf1ofs 28849	. . . . 5 |- ( NN e. _V -> ( (𝟭 ` NN ) |` Fin ) : ( ~P NN i^i Fin ) -1-1-onto-> { f e. ( { 0 , 1 } ^m NN ) | ( `' f " { 1 } ) e. Fin } )
3	1, 2	ax-mp 5	. . . 4 |- ( (𝟭 ` NN ) |` Fin ) : ( ~P NN i^i Fin ) -1-1-onto-> { f e. ( { 0 , 1 } ^m NN ) | ( `' f " { 1 } ) e. Fin }
4		incom 3656	. . . . . . 7 |- ( ( { 0 , 1 } ^m NN ) i^i { f | ( `' f " NN ) e. Fin } ) = ( { f | ( `' f " NN ) e. Fin } i^i ( { 0 , 1 } ^m NN ) )
5		eulerpart.r	. . . . . . . 8 |- R = { f | ( `' f " NN ) e. Fin }
6	5	ineq2i 3662	. . . . . . 7 |- ( ( { 0 , 1 } ^m NN ) i^i R ) = ( ( { 0 , 1 } ^m NN ) i^i { f | ( `' f " NN ) e. Fin } )
7		dfrab2 3750	. . . . . . 7 |- { f e. ( { 0 , 1 } ^m NN ) | ( `' f " NN ) e. Fin } = ( { f | ( `' f " NN ) e. Fin } i^i ( { 0 , 1 } ^m NN ) )
8	4, 6, 7	3eqtr4i 2462	. . . . . 6 |- ( ( { 0 , 1 } ^m NN ) i^i R ) = { f e. ( { 0 , 1 } ^m NN ) | ( `' f " NN ) e. Fin }
9		elmapfun 7501	. . . . . . . . 9 |- ( f e. ( { 0 , 1 } ^m NN ) -> Fun f )
10		elmapi 7499	. . . . . . . . . 10 |- ( f e. ( { 0 , 1 } ^m NN ) -> f : NN --> { 0 , 1 } )
11		frn 5750	. . . . . . . . . 10 |- ( f : NN --> { 0 , 1 } -> ran f C_ { 0 , 1 } )
12	10, 11	syl 17	. . . . . . . . 9 |- ( f e. ( { 0 , 1 } ^m NN ) -> ran f C_ { 0 , 1 } )
13		fimacnvinrn2 28232	. . . . . . . . . 10 |- ( ( Fun f /\ ran f C_ { 0 , 1 } ) -> ( `' f " NN ) = ( `' f " ( NN i^i { 0 , 1 } ) ) )
14		df-pr 4000	. . . . . . . . . . . . . 14 |- { 0 , 1 } = ( { 0 } u. { 1 } )
15	14	ineq2i 3662	. . . . . . . . . . . . 13 |- ( NN i^i { 0 , 1 } ) = ( NN i^i ( { 0 } u. { 1 } ) )
16		indi 3720	. . . . . . . . . . . . 13 |- ( NN i^i ( { 0 } u. { 1 } ) ) = ( ( NN i^i { 0 } ) u. ( NN i^i { 1 } ) )
17		0nnn 10643	. . . . . . . . . . . . . . 15 |- -. 0 e. NN
18		disjsn 4058	. . . . . . . . . . . . . . 15 |- ( ( NN i^i { 0 } ) = (/) <-> -. 0 e. NN )
19	17, 18	mpbir 213	. . . . . . . . . . . . . 14 |- ( NN i^i { 0 } ) = (/)
20		1nn 10622	. . . . . . . . . . . . . . . . 17 |- 1 e. NN
21		1ex 9640	. . . . . . . . . . . . . . . . . 18 |- 1 e. _V
22	21	snss 4122	. . . . . . . . . . . . . . . . 17 |- ( 1 e. NN <-> { 1 } C_ NN )
23	20, 22	mpbi 212	. . . . . . . . . . . . . . . 16 |- { 1 } C_ NN
24		dfss 3452	. . . . . . . . . . . . . . . 16 |- ( { 1 } C_ NN <-> { 1 } = ( { 1 } i^i NN ) )
25	23, 24	mpbi 212	. . . . . . . . . . . . . . 15 |- { 1 } = ( { 1 } i^i NN )
26		incom 3656	. . . . . . . . . . . . . . 15 |- ( { 1 } i^i NN ) = ( NN i^i { 1 } )
27	25, 26	eqtr2i 2453	. . . . . . . . . . . . . 14 |- ( NN i^i { 1 } ) = { 1 }
28	19, 27	uneq12i 3619	. . . . . . . . . . . . 13 |- ( ( NN i^i { 0 } ) u. ( NN i^i { 1 } ) ) = ( (/) u. { 1 } )
29	15, 16, 28	3eqtri 2456	. . . . . . . . . . . 12 |- ( NN i^i { 0 , 1 } ) = ( (/) u. { 1 } )
30		uncom 3611	. . . . . . . . . . . 12 |- ( (/) u. { 1 } ) = ( { 1 } u. (/) )
31		un0 3788	. . . . . . . . . . . 12 |- ( { 1 } u. (/) ) = { 1 }
32	29, 30, 31	3eqtri 2456	. . . . . . . . . . 11 |- ( NN i^i { 0 , 1 } ) = { 1 }
33	32	imaeq2i 5183	. . . . . . . . . 10 |- ( `' f " ( NN i^i { 0 , 1 } ) ) = ( `' f " { 1 } )
34	13, 33	syl6eq 2480	. . . . . . . . 9 |- ( ( Fun f /\ ran f C_ { 0 , 1 } ) -> ( `' f " NN ) = ( `' f " { 1 } ) )
35	9, 12, 34	syl2anc 666	. . . . . . . 8 |- ( f e. ( { 0 , 1 } ^m NN ) -> ( `' f " NN ) = ( `' f " { 1 } ) )
36	35	eleq1d 2492	. . . . . . 7 |- ( f e. ( { 0 , 1 } ^m NN ) -> ( ( `' f " NN ) e. Fin <-> ( `' f " { 1 } ) e. Fin ) )
37	36	rabbiia 3070	. . . . . 6 |- { f e. ( { 0 , 1 } ^m NN ) | ( `' f " NN ) e. Fin } = { f e. ( { 0 , 1 } ^m NN ) | ( `' f " { 1 } ) e. Fin }
38	8, 37	eqtr2i 2453	. . . . 5 |- { f e. ( { 0 , 1 } ^m NN ) | ( `' f " { 1 } ) e. Fin } = ( ( { 0 , 1 } ^m NN ) i^i R )
39		f1oeq3 5822	. . . . 5 |- ( { f e. ( { 0 , 1 } ^m NN ) | ( `' f " { 1 } ) e. Fin } = ( ( { 0 , 1 } ^m NN ) i^i R ) -> ( ( (𝟭 ` NN ) |` Fin ) : ( ~P NN i^i Fin ) -1-1-onto-> { f e. ( { 0 , 1 } ^m NN ) | ( `' f " { 1 } ) e. Fin } <-> ( (𝟭 ` NN ) |` Fin ) : ( ~P NN i^i Fin ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R ) ) )
40	38, 39	ax-mp 5	. . . 4 |- ( ( (𝟭 ` NN ) |` Fin ) : ( ~P NN i^i Fin ) -1-1-onto-> { f e. ( { 0 , 1 } ^m NN ) | ( `' f " { 1 } ) e. Fin } <-> ( (𝟭 ` NN ) |` Fin ) : ( ~P NN i^i Fin ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R ) )
41	3, 40	mpbi 212	. . 3 |- ( (𝟭 ` NN ) |` Fin ) : ( ~P NN i^i Fin ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R )
42		eulerpart.j	. . . . . . 7 |- J = { z e. NN | -. 2 || z }
43		eulerpart.f	. . . . . . 7 |- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )
44	42, 43	oddpwdc 29189	. . . . . 6 |- F : ( J X. NN0 ) -1-1-onto-> NN
45		f1opwfi 7882	. . . . . 6 |- ( F : ( J X. NN0 ) -1-1-onto-> NN -> ( a e. ( ~P ( J X. NN0 ) i^i Fin ) |-> ( F " a ) ) : ( ~P ( J X. NN0 ) i^i Fin ) -1-1-onto-> ( ~P NN i^i Fin ) )
46	44, 45	ax-mp 5	. . . . 5 |- ( a e. ( ~P ( J X. NN0 ) i^i Fin ) |-> ( F " a ) ) : ( ~P ( J X. NN0 ) i^i Fin ) -1-1-onto-> ( ~P NN i^i Fin )
47		eulerpart.p	. . . . . . . 8 |- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }
48		eulerpart.o	. . . . . . . 8 |- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }
49		eulerpart.d	. . . . . . . 8 |- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }
50		eulerpart.h	. . . . . . . 8 |- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }
51		eulerpart.m	. . . . . . . 8 |- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )
52	47, 48, 49, 42, 43, 50, 51	eulerpartlem1 29202	. . . . . . 7 |- M : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin )
53		bitsf1o 14412	. . . . . . . . . . . . . 14 |- (bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin )
54	53	a1i 11	. . . . . . . . . . . . 13 |- ( T. -> (bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) )
55	42, 1	rabex2 4575	. . . . . . . . . . . . . 14 |- J e. _V
56	55	a1i 11	. . . . . . . . . . . . 13 |- ( T. -> J e. _V )
57		nn0ex 10877	. . . . . . . . . . . . . 14 |- NN0 e. _V
58	57	a1i 11	. . . . . . . . . . . . 13 |- ( T. -> NN0 e. _V )
59	57	pwex 4605	. . . . . . . . . . . . . . 15 |- ~P NN0 e. _V
60	59	inex1 4563	. . . . . . . . . . . . . 14 |- ( ~P NN0 i^i Fin ) e. _V
61	60	a1i 11	. . . . . . . . . . . . 13 |- ( T. -> ( ~P NN0 i^i Fin ) e. _V )
62		0nn0 10886	. . . . . . . . . . . . . 14 |- 0 e. NN0
63	62	a1i 11	. . . . . . . . . . . . 13 |- ( T. -> 0 e. NN0 )
64		fvres 5893	. . . . . . . . . . . . . . 15 |- ( 0 e. NN0 -> ( (bits |` NN0 ) ` 0 ) = (bits ` 0 ) )
65	62, 64	ax-mp 5	. . . . . . . . . . . . . 14 |- ( (bits |` NN0 ) ` 0 ) = (bits ` 0 )
66		0bits 14406	. . . . . . . . . . . . . 14 |- (bits ` 0 ) = (/)
67	65, 66	eqtr2i 2453	. . . . . . . . . . . . 13 |- (/) = ( (bits |` NN0 ) ` 0 )
68		elmapi 7499	. . . . . . . . . . . . . . . . 17 |- ( f e. ( NN0 ^m J ) -> f : J --> NN0 )
69		frnnn0supp 10925	. . . . . . . . . . . . . . . . 17 |- ( ( J e. _V /\ f : J --> NN0 ) -> ( f supp 0 ) = ( `' f " NN ) )
70	55, 68, 69	sylancr 668	. . . . . . . . . . . . . . . 16 |- ( f e. ( NN0 ^m J ) -> ( f supp 0 ) = ( `' f " NN ) )
71	70	eleq1d 2492	. . . . . . . . . . . . . . 15 |- ( f e. ( NN0 ^m J ) -> ( ( f supp 0 ) e. Fin <-> ( `' f " NN ) e. Fin ) )
72	71	rabbiia 3070	. . . . . . . . . . . . . 14 |- { f e. ( NN0 ^m J ) | ( f supp 0 ) e. Fin } = { f e. ( NN0 ^m J ) | ( `' f " NN ) e. Fin }
73		elmapfun 7501	. . . . . . . . . . . . . . . 16 |- ( f e. ( NN0 ^m J ) -> Fun f )
74		vex 3085	. . . . . . . . . . . . . . . . 17 |- f e. _V
75		funisfsupp 7892	. . . . . . . . . . . . . . . . 17 |- ( ( Fun f /\ f e. _V /\ 0 e. NN0 ) -> ( f finSupp 0 <-> ( f supp 0 ) e. Fin ) )
76	74, 62, 75	mp3an23 1353	. . . . . . . . . . . . . . . 16 |- ( Fun f -> ( f finSupp 0 <-> ( f supp 0 ) e. Fin ) )
77	73, 76	syl 17	. . . . . . . . . . . . . . 15 |- ( f e. ( NN0 ^m J ) -> ( f finSupp 0 <-> ( f supp 0 ) e. Fin ) )
78	77	rabbiia 3070	. . . . . . . . . . . . . 14 |- { f e. ( NN0 ^m J ) | f finSupp 0 } = { f e. ( NN0 ^m J ) | ( f supp 0 ) e. Fin }
79		incom 3656	. . . . . . . . . . . . . . 15 |- ( { f | ( `' f " NN ) e. Fin } i^i ( NN0 ^m J ) ) = ( ( NN0 ^m J ) i^i { f | ( `' f " NN ) e. Fin } )
80		dfrab2 3750	. . . . . . . . . . . . . . 15 |- { f e. ( NN0 ^m J ) | ( `' f " NN ) e. Fin } = ( { f | ( `' f " NN ) e. Fin } i^i ( NN0 ^m J ) )
81	5	ineq2i 3662	. . . . . . . . . . . . . . 15 |- ( ( NN0 ^m J ) i^i R ) = ( ( NN0 ^m J ) i^i { f | ( `' f " NN ) e. Fin } )
82	79, 80, 81	3eqtr4ri 2463	. . . . . . . . . . . . . 14 |- ( ( NN0 ^m J ) i^i R ) = { f e. ( NN0 ^m J ) | ( `' f " NN ) e. Fin }
83	72, 78, 82	3eqtr4ri 2463	. . . . . . . . . . . . 13 |- ( ( NN0 ^m J ) i^i R ) = { f e. ( NN0 ^m J ) | f finSupp 0 }
84		elmapfun 7501	. . . . . . . . . . . . . . 15 |- ( r e. ( ( ~P NN0 i^i Fin ) ^m J ) -> Fun r )
85		vex 3085	. . . . . . . . . . . . . . . . 17 |- r e. _V
86		0ex 4554	. . . . . . . . . . . . . . . . 17 |- (/) e. _V
87		funisfsupp 7892	. . . . . . . . . . . . . . . . 17 |- ( ( Fun r /\ r e. _V /\ (/) e. _V ) -> ( r finSupp (/) <-> ( r supp (/) ) e. Fin ) )
88	85, 86, 87	mp3an23 1353	. . . . . . . . . . . . . . . 16 |- ( Fun r -> ( r finSupp (/) <-> ( r supp (/) ) e. Fin ) )
89	88	bicomd 205	. . . . . . . . . . . . . . 15 |- ( Fun r -> ( ( r supp (/) ) e. Fin <-> r finSupp (/) ) )
90	84, 89	syl 17	. . . . . . . . . . . . . 14 |- ( r e. ( ( ~P NN0 i^i Fin ) ^m J ) -> ( ( r supp (/) ) e. Fin <-> r finSupp (/) ) )
91	90	rabbiia 3070	. . . . . . . . . . . . 13 |- { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin } = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | r finSupp (/) }
92	54, 56, 58, 61, 63, 67, 83, 91	fcobijfs 28311	. . . . . . . . . . . 12 |- ( T. -> ( f e. ( ( NN0 ^m J ) i^i R ) |-> ( (bits |` NN0 ) o. f ) ) : ( ( NN0 ^m J ) i^i R ) -1-1-onto-> { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin } )
93		inss1 3683	. . . . . . . . . . . . . . . . 17 |- ( ( NN0 ^m J ) i^i R ) C_ ( NN0 ^m J )
94	93	sseli 3461	. . . . . . . . . . . . . . . 16 |- ( f e. ( ( NN0 ^m J ) i^i R ) -> f e. ( NN0 ^m J ) )
95		frn 5750	. . . . . . . . . . . . . . . . 17 |- ( f : J --> NN0 -> ran f C_ NN0 )
96		cores 5355	. . . . . . . . . . . . . . . . 17 |- ( ran f C_ NN0 -> ( (bits |` NN0 ) o. f ) = (bits o. f ) )
97	68, 95, 96	3syl 18	. . . . . . . . . . . . . . . 16 |- ( f e. ( NN0 ^m J ) -> ( (bits |` NN0 ) o. f ) = (bits o. f ) )
98	94, 97	syl 17	. . . . . . . . . . . . . . 15 |- ( f e. ( ( NN0 ^m J ) i^i R ) -> ( (bits |` NN0 ) o. f ) = (bits o. f ) )
99	98	mpteq2ia 4504	. . . . . . . . . . . . . 14 |- ( f e. ( ( NN0 ^m J ) i^i R ) |-> ( (bits |` NN0 ) o. f ) ) = ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) )
100	99	eqcomi 2436	. . . . . . . . . . . . 13 |- ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) = ( f e. ( ( NN0 ^m J ) i^i R ) |-> ( (bits |` NN0 ) o. f ) )
101		f1oeq1 5820	. . . . . . . . . . . . 13 |- ( ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) = ( f e. ( ( NN0 ^m J ) i^i R ) |-> ( (bits |` NN0 ) o. f ) ) -> ( ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) : ( ( NN0 ^m J ) i^i R ) -1-1-onto-> { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin } <-> ( f e. ( ( NN0 ^m J ) i^i R ) |-> ( (bits |` NN0 ) o. f ) ) : ( ( NN0 ^m J ) i^i R ) -1-1-onto-> { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin } ) )
102	100, 101	mp1i 13	. . . . . . . . . . . 12 |- ( T. -> ( ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) : ( ( NN0 ^m J ) i^i R ) -1-1-onto-> { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin } <-> ( f e. ( ( NN0 ^m J ) i^i R ) |-> ( (bits |` NN0 ) o. f ) ) : ( ( NN0 ^m J ) i^i R ) -1-1-onto-> { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin } ) )
103	92, 102	mpbird 236	. . . . . . . . . . 11 |- ( T. -> ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) : ( ( NN0 ^m J ) i^i R ) -1-1-onto-> { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin } )
104	103	trud 1447	. . . . . . . . . 10 |- ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) : ( ( NN0 ^m J ) i^i R ) -1-1-onto-> { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }
105		ssrab2 3547	. . . . . . . . . . . . . . . 16 |- { z e. NN | -. 2 || z } C_ NN
106	42, 105	eqsstri 3495	. . . . . . . . . . . . . . 15 |- J C_ NN
107	1, 57, 106	3pm3.2i 1184	. . . . . . . . . . . . . 14 |- ( NN e. _V /\ NN0 e. _V /\ J C_ NN )
108		eulerpart.t	. . . . . . . . . . . . . . . 16 |- T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }
109		cnveq 5025	. . . . . . . . . . . . . . . . . . 19 |- ( f = o -> `' f = `' o )
110		dfn2 10884	. . . . . . . . . . . . . . . . . . . 20 |- NN = ( NN0 \ { 0 } )
111	110	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( f = o -> NN = ( NN0 \ { 0 } ) )
112	109, 111	imaeq12d 5186	. . . . . . . . . . . . . . . . . 18 |- ( f = o -> ( `' f " NN ) = ( `' o " ( NN0 \ { 0 } ) ) )
113	112	sseq1d 3492	. . . . . . . . . . . . . . . . 17 |- ( f = o -> ( ( `' f " NN ) C_ J <-> ( `' o " ( NN0 \ { 0 } ) ) C_ J ) )
114	113	cbvrabv 3081	. . . . . . . . . . . . . . . 16 |- { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J } = { o e. ( NN0 ^m NN ) | ( `' o " ( NN0 \ { 0 } ) ) C_ J }
115	108, 114	eqtri 2452	. . . . . . . . . . . . . . 15 |- T = { o e. ( NN0 ^m NN ) | ( `' o " ( NN0 \ { 0 } ) ) C_ J }
116		eqid 2423	. . . . . . . . . . . . . . 15 |- ( o e. T |-> ( o |` J ) ) = ( o e. T |-> ( o |` J ) )
117	115, 116	resf1o 28315	. . . . . . . . . . . . . 14 |- ( ( ( NN e. _V /\ NN0 e. _V /\ J C_ NN ) /\ 0 e. NN0 ) -> ( o e. T |-> ( o |` J ) ) : T -1-1-onto-> ( NN0 ^m J ) )
118	107, 62, 117	mp2an 677	. . . . . . . . . . . . 13 |- ( o e. T |-> ( o |` J ) ) : T -1-1-onto-> ( NN0 ^m J )
119		f1of1 5828	. . . . . . . . . . . . 13 |- ( ( o e. T |-> ( o |` J ) ) : T -1-1-onto-> ( NN0 ^m J ) -> ( o e. T |-> ( o |` J ) ) : T -1-1-> ( NN0 ^m J ) )
120	118, 119	ax-mp 5	. . . . . . . . . . . 12 |- ( o e. T |-> ( o |` J ) ) : T -1-1-> ( NN0 ^m J )
121		inss1 3683	. . . . . . . . . . . 12 |- ( T i^i R ) C_ T
122		f1ores 5843	. . . . . . . . . . . 12 |- ( ( ( o e. T |-> ( o |` J ) ) : T -1-1-> ( NN0 ^m J ) /\ ( T i^i R ) C_ T ) -> ( ( o e. T |-> ( o |` J ) ) |` ( T i^i R ) ) : ( T i^i R ) -1-1-onto-> ( ( o e. T |-> ( o |` J ) ) " ( T i^i R ) ) )
123	120, 121, 122	mp2an 677	. . . . . . . . . . 11 |- ( ( o e. T |-> ( o |` J ) ) |` ( T i^i R ) ) : ( T i^i R ) -1-1-onto-> ( ( o e. T |-> ( o |` J ) ) " ( T i^i R ) )
124		vex 3085	. . . . . . . . . . . . . . . . . 18 |- o e. _V
125	124	resex 5165	. . . . . . . . . . . . . . . . 17 |- ( o |` J ) e. _V
126	125, 116	fnmpti 5722	. . . . . . . . . . . . . . . 16 |- ( o e. T |-> ( o |` J ) ) Fn T
127		fvelimab 5935	. . . . . . . . . . . . . . . 16 |- ( ( ( o e. T |-> ( o |` J ) ) Fn T /\ ( T i^i R ) C_ T ) -> ( f e. ( ( o e. T |-> ( o |` J ) ) " ( T i^i R ) ) <-> E. m e. ( T i^i R ) ( ( o e. T |-> ( o |` J ) ) ` m ) = f ) )
128	126, 121, 127	mp2an 677	. . . . . . . . . . . . . . 15 |- ( f e. ( ( o e. T |-> ( o |` J ) ) " ( T i^i R ) ) <-> E. m e. ( T i^i R ) ( ( o e. T |-> ( o |` J ) ) ` m ) = f )
129		eqid 2423	. . . . . . . . . . . . . . . . 17 |- ( m e. ( T i^i R ) |-> ( m |` J ) ) = ( m e. ( T i^i R ) |-> ( m |` J ) )
130		vex 3085	. . . . . . . . . . . . . . . . . 18 |- m e. _V
131	130	resex 5165	. . . . . . . . . . . . . . . . 17 |- ( m |` J ) e. _V
132	129, 131	elrnmpti 5102	. . . . . . . . . . . . . . . 16 |- ( f e. ran ( m e. ( T i^i R ) |-> ( m |` J ) ) <-> E. m e. ( T i^i R ) f = ( m |` J ) )
133	47, 48, 49, 42, 43, 50, 51, 5, 108	eulerpartlemt 29206	. . . . . . . . . . . . . . . . 17 |- ( ( NN0 ^m J ) i^i R ) = ran ( m e. ( T i^i R ) |-> ( m |` J ) )
134	133	eleq2i 2501	. . . . . . . . . . . . . . . 16 |- ( f e. ( ( NN0 ^m J ) i^i R ) <-> f e. ran ( m e. ( T i^i R ) |-> ( m |` J ) ) )
135	121	sseli 3461	. . . . . . . . . . . . . . . . . . 19 |- ( m e. ( T i^i R ) -> m e. T )
136	116	fvtresfn 5964	. . . . . . . . . . . . . . . . . . . 20 |- ( m e. T -> ( ( o e. T |-> ( o |` J ) ) ` m ) = ( m |` J ) )
137	136	eqeq1d 2425	. . . . . . . . . . . . . . . . . . 19 |- ( m e. T -> ( ( ( o e. T |-> ( o |` J ) ) ` m ) = f <-> ( m |` J ) = f ) )
138	135, 137	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( m e. ( T i^i R ) -> ( ( ( o e. T |-> ( o |` J ) ) ` m ) = f <-> ( m |` J ) = f ) )
139		eqcom 2432	. . . . . . . . . . . . . . . . . 18 |- ( ( m |` J ) = f <-> f = ( m |` J ) )
140	138, 139	syl6bb 265	. . . . . . . . . . . . . . . . 17 |- ( m e. ( T i^i R ) -> ( ( ( o e. T |-> ( o |` J ) ) ` m ) = f <-> f = ( m |` J ) ) )
141	140	rexbiia 2927	. . . . . . . . . . . . . . . 16 |- ( E. m e. ( T i^i R ) ( ( o e. T |-> ( o |` J ) ) ` m ) = f <-> E. m e. ( T i^i R ) f = ( m |` J ) )
142	132, 134, 141	3bitr4ri 282	. . . . . . . . . . . . . . 15 |- ( E. m e. ( T i^i R ) ( ( o e. T |-> ( o |` J ) ) ` m ) = f <-> f e. ( ( NN0 ^m J ) i^i R ) )
143	128, 142	bitri 253	. . . . . . . . . . . . . 14 |- ( f e. ( ( o e. T |-> ( o |` J ) ) " ( T i^i R ) ) <-> f e. ( ( NN0 ^m J ) i^i R ) )
144	143	eqriv 2419	. . . . . . . . . . . . 13 |- ( ( o e. T |-> ( o |` J ) ) " ( T i^i R ) ) = ( ( NN0 ^m J ) i^i R )
145		f1oeq3 5822	. . . . . . . . . . . . 13 |- ( ( ( o e. T |-> ( o |` J ) ) " ( T i^i R ) ) = ( ( NN0 ^m J ) i^i R ) -> ( ( ( o e. T |-> ( o |` J ) ) |` ( T i^i R ) ) : ( T i^i R ) -1-1-onto-> ( ( o e. T |-> ( o |` J ) ) " ( T i^i R ) ) <-> ( ( o e. T |-> ( o |` J ) ) |` ( T i^i R ) ) : ( T i^i R ) -1-1-onto-> ( ( NN0 ^m J ) i^i R ) ) )
146	144, 145	ax-mp 5	. . . . . . . . . . . 12 |- ( ( ( o e. T |-> ( o |` J ) ) |` ( T i^i R ) ) : ( T i^i R ) -1-1-onto-> ( ( o e. T |-> ( o |` J ) ) " ( T i^i R ) ) <-> ( ( o e. T |-> ( o |` J ) ) |` ( T i^i R ) ) : ( T i^i R ) -1-1-onto-> ( ( NN0 ^m J ) i^i R ) )
147		resmpt 5171	. . . . . . . . . . . . 13 |- ( ( T i^i R ) C_ T -> ( ( o e. T |-> ( o |` J ) ) |` ( T i^i R ) ) = ( o e. ( T i^i R ) |-> ( o |` J ) ) )
148		f1oeq1 5820	. . . . . . . . . . . . 13 |- ( ( ( o e. T |-> ( o |` J ) ) |` ( T i^i R ) ) = ( o e. ( T i^i R ) |-> ( o |` J ) ) -> ( ( ( o e. T |-> ( o |` J ) ) |` ( T i^i R ) ) : ( T i^i R ) -1-1-onto-> ( ( NN0 ^m J ) i^i R ) <-> ( o e. ( T i^i R ) |-> ( o |` J ) ) : ( T i^i R ) -1-1-onto-> ( ( NN0 ^m J ) i^i R ) ) )
149	121, 147, 148	mp2b 10	. . . . . . . . . . . 12 |- ( ( ( o e. T |-> ( o |` J ) ) |` ( T i^i R ) ) : ( T i^i R ) -1-1-onto-> ( ( NN0 ^m J ) i^i R ) <-> ( o e. ( T i^i R ) |-> ( o |` J ) ) : ( T i^i R ) -1-1-onto-> ( ( NN0 ^m J ) i^i R ) )
150	146, 149	bitri 253	. . . . . . . . . . 11 |- ( ( ( o e. T |-> ( o |` J ) ) |` ( T i^i R ) ) : ( T i^i R ) -1-1-onto-> ( ( o e. T |-> ( o |` J ) ) " ( T i^i R ) ) <-> ( o e. ( T i^i R ) |-> ( o |` J ) ) : ( T i^i R ) -1-1-onto-> ( ( NN0 ^m J ) i^i R ) )
151	123, 150	mpbi 212	. . . . . . . . . 10 |- ( o e. ( T i^i R ) |-> ( o |` J ) ) : ( T i^i R ) -1-1-onto-> ( ( NN0 ^m J ) i^i R )
152		f1oco 5851	. . . . . . . . . 10 |- ( ( ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) : ( ( NN0 ^m J ) i^i R ) -1-1-onto-> { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin } /\ ( o e. ( T i^i R ) |-> ( o |` J ) ) : ( T i^i R ) -1-1-onto-> ( ( NN0 ^m J ) i^i R ) ) -> ( ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) o. ( o e. ( T i^i R ) |-> ( o |` J ) ) ) : ( T i^i R ) -1-1-onto-> { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin } )
153	104, 151, 152	mp2an 677	. . . . . . . . 9 |- ( ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) o. ( o e. ( T i^i R ) |-> ( o |` J ) ) ) : ( T i^i R ) -1-1-onto-> { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }
154		f1of 5829	. . . . . . . . . . . . . 14 |- ( ( o e. ( T i^i R ) |-> ( o |` J ) ) : ( T i^i R ) -1-1-onto-> ( ( NN0 ^m J ) i^i R ) -> ( o e. ( T i^i R ) |-> ( o |` J ) ) : ( T i^i R ) --> ( ( NN0 ^m J ) i^i R ) )
155		eqid 2423	. . . . . . . . . . . . . . . 16 |- ( o e. ( T i^i R ) |-> ( o |` J ) ) = ( o e. ( T i^i R ) |-> ( o |` J ) )
156	155	fmpt 6056	. . . . . . . . . . . . . . 15 |- ( A. o e. ( T i^i R ) ( o |` J ) e. ( ( NN0 ^m J ) i^i R ) <-> ( o e. ( T i^i R ) |-> ( o |` J ) ) : ( T i^i R ) --> ( ( NN0 ^m J ) i^i R ) )
157	156	biimpri 210	. . . . . . . . . . . . . 14 |- ( ( o e. ( T i^i R ) |-> ( o |` J ) ) : ( T i^i R ) --> ( ( NN0 ^m J ) i^i R ) -> A. o e. ( T i^i R ) ( o |` J ) e. ( ( NN0 ^m J ) i^i R ) )
158	151, 154, 157	mp2b 10	. . . . . . . . . . . . 13 |- A. o e. ( T i^i R ) ( o |` J ) e. ( ( NN0 ^m J ) i^i R )
159	158	a1i 11	. . . . . . . . . . . 12 |- ( T. -> A. o e. ( T i^i R ) ( o |` J ) e. ( ( NN0 ^m J ) i^i R ) )
160		eqidd 2424	. . . . . . . . . . . 12 |- ( T. -> ( o e. ( T i^i R ) |-> ( o |` J ) ) = ( o e. ( T i^i R ) |-> ( o |` J ) ) )
161		eqidd 2424	. . . . . . . . . . . 12 |- ( T. -> ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) = ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) )
162		coeq2 5010	. . . . . . . . . . . 12 |- ( f = ( o |` J ) -> (bits o. f ) = (bits o. ( o |` J ) ) )
163	159, 160, 161, 162	fmptcof 6070	. . . . . . . . . . 11 |- ( T. -> ( ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) o. ( o e. ( T i^i R ) |-> ( o |` J ) ) ) = ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) )
164	163	eqcomd 2431	. . . . . . . . . 10 |- ( T. -> ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) = ( ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) o. ( o e. ( T i^i R ) |-> ( o |` J ) ) ) )
165		eqidd 2424	. . . . . . . . . 10 |- ( T. -> ( T i^i R ) = ( T i^i R ) )
166	50	a1i 11	. . . . . . . . . 10 |- ( T. -> H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin } )
167	164, 165, 166	f1oeq123d 5826	. . . . . . . . 9 |- ( T. -> ( ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) : ( T i^i R ) -1-1-onto-> H <-> ( ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) o. ( o e. ( T i^i R ) |-> ( o |` J ) ) ) : ( T i^i R ) -1-1-onto-> { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin } ) )
168	153, 167	mpbiri 237	. . . . . . . 8 |- ( T. -> ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) : ( T i^i R ) -1-1-onto-> H )
169	168	trud 1447	. . . . . . 7 |- ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) : ( T i^i R ) -1-1-onto-> H
170		f1oco 5851	. . . . . . 7 |- ( ( M : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin ) /\ ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) : ( T i^i R ) -1-1-onto-> H ) -> ( M o. ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin ) )
171	52, 169, 170	mp2an 677	. . . . . 6 |- ( M o. ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin )
172		eqidd 2424	. . . . . . . . . . 11 |- ( T. -> ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) = ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) )
173		bitsf 14393	. . . . . . . . . . . . . 14 |- bits : ZZ --> ~P NN0
174		zex 10948	. . . . . . . . . . . . . 14 |- ZZ e. _V
175		fex 6151	. . . . . . . . . . . . . 14 |- ( (bits : ZZ --> ~P NN0 /\ ZZ e. _V ) -> bits e. _V )
176	173, 174, 175	mp2an 677	. . . . . . . . . . . . 13 |- bits e. _V
177	176, 125	coex 6757	. . . . . . . . . . . 12 |- (bits o. ( o |` J ) ) e. _V
178	177	a1i 11	. . . . . . . . . . 11 |- ( ( T. /\ o e. ( T i^i R ) ) -> (bits o. ( o |` J ) ) e. _V )
179	172, 178	fvmpt2d 5973	. . . . . . . . . 10 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) ` o ) = (bits o. ( o |` J ) ) )
180		f1of 5829	. . . . . . . . . . . 12 |- ( ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) : ( T i^i R ) -1-1-onto-> H -> ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) : ( T i^i R ) --> H )
181	168, 180	syl 17	. . . . . . . . . . 11 |- ( T. -> ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) : ( T i^i R ) --> H )
182	181	ffvelrnda 6035	. . . . . . . . . 10 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) ` o ) e. H )
183	179, 182	eqeltrrd 2512	. . . . . . . . 9 |- ( ( T. /\ o e. ( T i^i R ) ) -> (bits o. ( o |` J ) ) e. H )
184		f1ofn 5830	. . . . . . . . . . . 12 |- ( M : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin ) -> M Fn H )
185	52, 184	ax-mp 5	. . . . . . . . . . 11 |- M Fn H
186		dffn5 5924	. . . . . . . . . . 11 |- ( M Fn H <-> M = ( r e. H |-> ( M ` r ) ) )
187	185, 186	mpbi 212	. . . . . . . . . 10 |- M = ( r e. H |-> ( M ` r ) )
188	187	a1i 11	. . . . . . . . 9 |- ( T. -> M = ( r e. H |-> ( M ` r ) ) )
189		fveq2 5879	. . . . . . . . 9 |- ( r = (bits o. ( o |` J ) ) -> ( M ` r ) = ( M ` (bits o. ( o |` J ) ) ) )
190	183, 172, 188, 189	fmptco 6069	. . . . . . . 8 |- ( T. -> ( M o. ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) ) = ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) )
191	190	trud 1447	. . . . . . 7 |- ( M o. ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) ) = ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) )
192		f1oeq1 5820	. . . . . . 7 |- ( ( M o. ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) ) = ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) -> ( ( M o. ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin ) <-> ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin ) ) )
193	191, 192	ax-mp 5	. . . . . 6 |- ( ( M o. ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin ) <-> ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin ) )
194	171, 193	mpbi 212	. . . . 5 |- ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin )
195		f1oco 5851	. . . . 5 |- ( ( ( a e. ( ~P ( J X. NN0 ) i^i Fin ) |-> ( F " a ) ) : ( ~P ( J X. NN0 ) i^i Fin ) -1-1-onto-> ( ~P NN i^i Fin ) /\ ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin ) ) -> ( ( a e. ( ~P ( J X. NN0 ) i^i Fin ) |-> ( F " a ) ) o. ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P NN i^i Fin ) )
196	46, 194, 195	mp2an 677	. . . 4 |- ( ( a e. ( ~P ( J X. NN0 ) i^i Fin ) |-> ( F " a ) ) o. ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P NN i^i Fin )
197		simpr 463	. . . . . . . . 9 |- ( ( T. /\ o e. ( T i^i R ) ) -> o e. ( T i^i R ) )
198		fvex 5889	. . . . . . . . 9 |- ( M ` (bits o. ( o |` J ) ) ) e. _V
199		eqid 2423	. . . . . . . . . 10 |- ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) = ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) )
200	199	fvmpt2 5971	. . . . . . . . 9 |- ( ( o e. ( T i^i R ) /\ ( M ` (bits o. ( o |` J ) ) ) e. _V ) -> ( ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) ` o ) = ( M ` (bits o. ( o |` J ) ) ) )
201	197, 198, 200	sylancl 667	. . . . . . . 8 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) ` o ) = ( M ` (bits o. ( o |` J ) ) ) )
202		f1of 5829	. . . . . . . . . 10 |- ( ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin ) -> ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) : ( T i^i R ) --> ( ~P ( J X. NN0 ) i^i Fin ) )
203	194, 202	mp1i 13	. . . . . . . . 9 |- ( T. -> ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) : ( T i^i R ) --> ( ~P ( J X. NN0 ) i^i Fin ) )
204	203	ffvelrnda 6035	. . . . . . . 8 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) ` o ) e. ( ~P ( J X. NN0 ) i^i Fin ) )
205	201, 204	eqeltrrd 2512	. . . . . . 7 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( M ` (bits o. ( o |` J ) ) ) e. ( ~P ( J X. NN0 ) i^i Fin ) )
206		eqidd 2424	. . . . . . 7 |- ( T. -> ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) = ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) )
207		eqidd 2424	. . . . . . 7 |- ( T. -> ( a e. ( ~P ( J X. NN0 ) i^i Fin ) |-> ( F " a ) ) = ( a e. ( ~P ( J X. NN0 ) i^i Fin ) |-> ( F " a ) ) )
208		imaeq2 5181	. . . . . . 7 |- ( a = ( M ` (bits o. ( o |` J ) ) ) -> ( F " a ) = ( F " ( M ` (bits o. ( o |` J ) ) ) ) )
209	205, 206, 207, 208	fmptco 6069	. . . . . 6 |- ( T. -> ( ( a e. ( ~P ( J X. NN0 ) i^i Fin ) |-> ( F " a ) ) o. ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) ) = ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )
210	209	trud 1447	. . . . 5 |- ( ( a e. ( ~P ( J X. NN0 ) i^i Fin ) |-> ( F " a ) ) o. ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) ) = ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) )
211		f1oeq1 5820	. . . . 5 |- ( ( ( a e. ( ~P ( J X. NN0 ) i^i Fin ) |-> ( F " a ) ) o. ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) ) = ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) -> ( ( ( a e. ( ~P ( J X. NN0 ) i^i Fin ) |-> ( F " a ) ) o. ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P NN i^i Fin ) <-> ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P NN i^i Fin ) ) )
212	210, 211	ax-mp 5	. . . 4 |- ( ( ( a e. ( ~P ( J X. NN0 ) i^i Fin ) |-> ( F " a ) ) o. ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P NN i^i Fin ) <-> ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P NN i^i Fin ) )
213	196, 212	mpbi 212	. . 3 |- ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P NN i^i Fin )
214		f1oco 5851	. . 3 |- ( ( ( (𝟭 ` NN ) |` Fin ) : ( ~P NN i^i Fin ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R ) /\ ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P NN i^i Fin ) ) -> ( ( (𝟭 ` NN ) |` Fin ) o. ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R ) )
215	41, 213, 214	mp2an 677	. 2 |- ( ( (𝟭 ` NN ) |` Fin ) o. ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R )
216		eulerpart.g	. . . 4 |- G = ( o e. ( T i^i R ) |-> ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )
217	43	mpt2exg 6880	. . . . . . . . . 10 |- ( ( J e. _V /\ NN0 e. _V ) -> F e. _V )
218	55, 57, 217	mp2an 677	. . . . . . . . 9 |- F e. _V
219		imaexg 6742	. . . . . . . . 9 |- ( F e. _V -> ( F " ( M ` (bits o. ( o |` J ) ) ) ) e. _V )
220	218, 219	ax-mp 5	. . . . . . . 8 |- ( F " ( M ` (bits o. ( o |` J ) ) ) ) e. _V
221		eqid 2423	. . . . . . . . 9 |- ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) = ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) )
222	221	fvmpt2 5971	. . . . . . . 8 |- ( ( o e. ( T i^i R ) /\ ( F " ( M ` (bits o. ( o |` J ) ) ) ) e. _V ) -> ( ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) ` o ) = ( F " ( M ` (bits o. ( o |` J ) ) ) ) )
223	197, 220, 222	sylancl 667	. . . . . . 7 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) ` o ) = ( F " ( M ` (bits o. ( o |` J ) ) ) ) )
224		f1of 5829	. . . . . . . . 9 |- ( ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P NN i^i Fin ) -> ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) : ( T i^i R ) --> ( ~P NN i^i Fin ) )
225	213, 224	mp1i 13	. . . . . . . 8 |- ( T. -> ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) : ( T i^i R ) --> ( ~P NN i^i Fin ) )
226	225	ffvelrnda 6035	. . . . . . 7 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) ` o ) e. ( ~P NN i^i Fin ) )
227	223, 226	eqeltrrd 2512	. . . . . 6 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( F " ( M ` (bits o. ( o |` J ) ) ) ) e. ( ~P NN i^i Fin ) )
228		eqidd 2424	. . . . . 6 |- ( T. -> ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) = ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )
229		indf1o 28847	. . . . . . . . . . 11 |- ( NN e. _V -> (𝟭 ` NN ) : ~P NN -1-1-onto-> ( { 0 , 1 } ^m NN ) )
230		f1ofn 5830	. . . . . . . . . . 11 |- ( (𝟭 ` NN ) : ~P NN -1-1-onto-> ( { 0 , 1 } ^m NN ) -> (𝟭 ` NN ) Fn ~P NN )
231	1, 229, 230	mp2b 10	. . . . . . . . . 10 |- (𝟭 ` NN ) Fn ~P NN
232		dffn5 5924	. . . . . . . . . 10 |- ( (𝟭 ` NN ) Fn ~P NN <-> (𝟭 ` NN ) = ( b e. ~P NN |-> ( (𝟭 ` NN ) ` b ) ) )
233	231, 232	mpbi 212	. . . . . . . . 9 |- (𝟭 ` NN ) = ( b e. ~P NN |-> ( (𝟭 ` NN ) ` b ) )
234	233	reseq1i 5118	. . . . . . . 8 |- ( (𝟭 ` NN ) |` Fin ) = ( ( b e. ~P NN |-> ( (𝟭 ` NN ) ` b ) ) |` Fin )
235		resmpt3 5172	. . . . . . . 8 |- ( ( b e. ~P NN |-> ( (𝟭 ` NN ) ` b ) ) |` Fin ) = ( b e. ( ~P NN i^i Fin ) |-> ( (𝟭 ` NN ) ` b ) )
236	234, 235	eqtri 2452	. . . . . . 7 |- ( (𝟭 ` NN ) |` Fin ) = ( b e. ( ~P NN i^i Fin ) |-> ( (𝟭 ` NN ) ` b ) )
237	236	a1i 11	. . . . . 6 |- ( T. -> ( (𝟭 ` NN ) |` Fin ) = ( b e. ( ~P NN i^i Fin ) |-> ( (𝟭 ` NN ) ` b ) ) )
238		fveq2 5879	. . . . . 6 |- ( b = ( F " ( M ` (bits o. ( o |` J ) ) ) ) -> ( (𝟭 ` NN ) ` b ) = ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )
239	227, 228, 237, 238	fmptco 6069	. . . . 5 |- ( T. -> ( ( (𝟭 ` NN ) |` Fin ) o. ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) ) = ( o e. ( T i^i R ) |-> ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) ) )
240	239	trud 1447	. . . 4 |- ( ( (𝟭 ` NN ) |` Fin ) o. ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) ) = ( o e. ( T i^i R ) |-> ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )
241	216, 240	eqtr4i 2455	. . 3 |- G = ( ( (𝟭 ` NN ) |` Fin ) o. ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )
242		f1oeq1 5820	. . 3 |- ( G = ( ( (𝟭 ` NN ) |` Fin ) o. ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) ) -> ( G : ( T i^i R ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R ) <-> ( ( (𝟭 ` NN ) |` Fin ) o. ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R ) ) )
243	241, 242	ax-mp 5	. 2 |- ( G : ( T i^i R ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R ) <-> ( ( (𝟭 ` NN ) |` Fin ) o. ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R ) )
244	215, 243	mpbir 213	1 |- G : ( T i^i R ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R )

Syntax hints:   -. wn 3   <-> wb 188   /\ wa 371   /\ w3a 983   = wceq 1438   T. wtru 1439   e. wcel 1869   {cab 2408   A.wral 2776   E.wrex 2777   {crab 2780   _Vcvv 3082   \ cdif 3434   u. cun 3435   i^i cin 3436   C_ wss 3437   (/)c0 3762   ~Pcpw 3980   {csn 3997   {cpr 3999   class class class wbr 4421   {copab 4479   |-> cmpt 4480   X. cxp 4849   `'ccnv 4850   ran crn 4852   |` cres 4853   "cima 4854   o. ccom 4855   Fun wfun 5593   Fn wfn 5594   -->wf 5595   -1-1->wf1 5596   -1-1-onto->wf1o 5598   ` cfv 5599  (class class class)co 6303   |-> cmpt2 6305   supp csupp 6923   ^m cmap 7478   Fincfn 7575   finSupp cfsupp 7887   0cc0 9541   1c1 9542   x. cmul 9546   <_ cle 9678   NNcn 10611   2c2 10661   NN0cn0 10871   ZZcz 10939   ^cexp 12273   sum_csu 13745   || cdvds 14298  bitscbits 14385  𝟭cind 28834

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-rep 4534  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658  ax-un 6595  ax-inf2 8150  ax-ac2 8895  ax-cnex 9597  ax-resscn 9598  ax-1cn 9599  ax-icn 9600  ax-addcl 9601  ax-addrcl 9602  ax-mulcl 9603  ax-mulrcl 9604  ax-mulcom 9605  ax-addass 9606  ax-mulass 9607  ax-distr 9608  ax-i2m1 9609  ax-1ne0 9610  ax-1rid 9611  ax-rnegex 9612  ax-rrecex 9613  ax-cnre 9614  ax-pre-lttri 9615  ax-pre-lttrn 9616  ax-pre-ltadd 9617  ax-pre-mulgt0 9618  ax-pre-sup 9619

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-fal 1444  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-nel 2622  df-ral 2781  df-rex 2782  df-reu 2783  df-rmo 2784  df-rab 2785  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3763  df-if 3911  df-pw 3982  df-sn 3998  df-pr 4000  df-tp 4002  df-op 4004  df-uni 4218  df-int 4254  df-iun 4299  df-disj 4393  df-br 4422  df-opab 4481  df-mpt 4482  df-tr 4517  df-eprel 4762  df-id 4766  df-po 4772  df-so 4773  df-fr 4810  df-se 4811  df-we 4812  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-pred 5397  df-ord 5443  df-on 5444  df-lim 5445  df-suc 5446  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-f1 5604  df-fo 5605  df-f1o 5606  df-fv 5607  df-isom 5608  df-riota 6265  df-ov 6306  df-oprab 6307  df-mpt2 6308  df-om 6705  df-1st 6805  df-2nd 6806  df-supp 6924  df-wrecs 7034  df-recs 7096  df-rdg 7134  df-1o 7188  df-2o 7189  df-oadd 7192  df-er 7369  df-map 7480  df-pm 7481  df-en 7576  df-dom 7577  df-sdom 7578  df-fin 7579  df-fsupp 7888  df-sup 7960  df-inf 7961  df-oi 8029  df-card 8376  df-acn 8379  df-ac 8549  df-cda 8600  df-pnf 9679  df-mnf 9680  df-xr 9681  df-ltxr 9682  df-le 9683  df-sub 9864  df-neg 9865  df-div 10272  df-nn 10612  df-2 10670  df-3 10671  df-n0 10872  df-z 10940  df-uz 11162  df-rp 11305  df-fz 11787  df-fzo 11918  df-fl 12029  df-mod 12098  df-seq 12215  df-exp 12274  df-hash 12517  df-cj 13156  df-re 13157  df-im 13158  df-sqrt 13292  df-abs 13293  df-clim 13545  df-sum 13746  df-dvds 14299  df-bits 14388  df-ind 28835

This theorem is referenced by:  eulerpartlemgf  29214  eulerpartlemgs2  29215  eulerpartlemn  29216