Theorem eulerpartgbij 27979

Description: Lemma for eulerpart 27989: 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 10542	. . . . 5 |- NN e. _V
2		indf1ofs 27707	. . . . 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 3691	. . . . . . 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 3697	. . . . . . 7 |- ( ( { 0 , 1 } ^m NN ) i^i R ) = ( ( { 0 , 1 } ^m NN ) i^i { f | ( `' f " NN ) e. Fin } )
7		dfrab2 3774	. . . . . . 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 2506	. . . . . 6 |- ( ( { 0 , 1 } ^m NN ) i^i R ) = { f e. ( { 0 , 1 } ^m NN ) | ( `' f " NN ) e. Fin }
9		elmapi 7440	. . . . . . . . . 10 |- ( f e. ( { 0 , 1 } ^m NN ) -> f : NN --> { 0 , 1 } )
10		ffun 5733	. . . . . . . . . 10 |- ( f : NN --> { 0 , 1 } -> Fun f )
11	9, 10	syl 16	. . . . . . . . 9 |- ( f e. ( { 0 , 1 } ^m NN ) -> Fun f )
12		frn 5737	. . . . . . . . . 10 |- ( f : NN --> { 0 , 1 } -> ran f C_ { 0 , 1 } )
13	9, 12	syl 16	. . . . . . . . 9 |- ( f e. ( { 0 , 1 } ^m NN ) -> ran f C_ { 0 , 1 } )
14		fimacnvinrn2 27177	. . . . . . . . . 10 |- ( ( Fun f /\ ran f C_ { 0 , 1 } ) -> ( `' f " NN ) = ( `' f " ( NN i^i { 0 , 1 } ) ) )
15		df-pr 4030	. . . . . . . . . . . . . 14 |- { 0 , 1 } = ( { 0 } u. { 1 } )
16	15	ineq2i 3697	. . . . . . . . . . . . 13 |- ( NN i^i { 0 , 1 } ) = ( NN i^i ( { 0 } u. { 1 } ) )
17		indi 3744	. . . . . . . . . . . . 13 |- ( NN i^i ( { 0 } u. { 1 } ) ) = ( ( NN i^i { 0 } ) u. ( NN i^i { 1 } ) )
18		0nnn 10567	. . . . . . . . . . . . . . 15 |- -. 0 e. NN
19		disjsn 4088	. . . . . . . . . . . . . . 15 |- ( ( NN i^i { 0 } ) = (/) <-> -. 0 e. NN )
20	18, 19	mpbir 209	. . . . . . . . . . . . . 14 |- ( NN i^i { 0 } ) = (/)
21		1nn 10547	. . . . . . . . . . . . . . . . 17 |- 1 e. NN
22		1ex 9591	. . . . . . . . . . . . . . . . . 18 |- 1 e. _V
23	22	snss 4151	. . . . . . . . . . . . . . . . 17 |- ( 1 e. NN <-> { 1 } C_ NN )
24	21, 23	mpbi 208	. . . . . . . . . . . . . . . 16 |- { 1 } C_ NN
25		dfss 3491	. . . . . . . . . . . . . . . 16 |- ( { 1 } C_ NN <-> { 1 } = ( { 1 } i^i NN ) )
26	24, 25	mpbi 208	. . . . . . . . . . . . . . 15 |- { 1 } = ( { 1 } i^i NN )
27		eqcom 2476	. . . . . . . . . . . . . . . 16 |- ( { 1 } = ( { 1 } i^i NN ) <-> ( { 1 } i^i NN ) = { 1 } )
28		incom 3691	. . . . . . . . . . . . . . . . 17 |- ( { 1 } i^i NN ) = ( NN i^i { 1 } )
29	28	eqeq1i 2474	. . . . . . . . . . . . . . . 16 |- ( ( { 1 } i^i NN ) = { 1 } <-> ( NN i^i { 1 } ) = { 1 } )
30	27, 29	bitri 249	. . . . . . . . . . . . . . 15 |- ( { 1 } = ( { 1 } i^i NN ) <-> ( NN i^i { 1 } ) = { 1 } )
31	26, 30	mpbi 208	. . . . . . . . . . . . . 14 |- ( NN i^i { 1 } ) = { 1 }
32	20, 31	uneq12i 3656	. . . . . . . . . . . . 13 |- ( ( NN i^i { 0 } ) u. ( NN i^i { 1 } ) ) = ( (/) u. { 1 } )
33	16, 17, 32	3eqtri 2500	. . . . . . . . . . . 12 |- ( NN i^i { 0 , 1 } ) = ( (/) u. { 1 } )
34		uncom 3648	. . . . . . . . . . . 12 |- ( (/) u. { 1 } ) = ( { 1 } u. (/) )
35		un0 3810	. . . . . . . . . . . 12 |- ( { 1 } u. (/) ) = { 1 }
36	33, 34, 35	3eqtri 2500	. . . . . . . . . . 11 |- ( NN i^i { 0 , 1 } ) = { 1 }
37	36	imaeq2i 5335	. . . . . . . . . 10 |- ( `' f " ( NN i^i { 0 , 1 } ) ) = ( `' f " { 1 } )
38	14, 37	syl6eq 2524	. . . . . . . . 9 |- ( ( Fun f /\ ran f C_ { 0 , 1 } ) -> ( `' f " NN ) = ( `' f " { 1 } ) )
39	11, 13, 38	syl2anc 661	. . . . . . . 8 |- ( f e. ( { 0 , 1 } ^m NN ) -> ( `' f " NN ) = ( `' f " { 1 } ) )
40	39	eleq1d 2536	. . . . . . 7 |- ( f e. ( { 0 , 1 } ^m NN ) -> ( ( `' f " NN ) e. Fin <-> ( `' f " { 1 } ) e. Fin ) )
41	40	rabbiia 3102	. . . . . 6 |- { f e. ( { 0 , 1 } ^m NN ) | ( `' f " NN ) e. Fin } = { f e. ( { 0 , 1 } ^m NN ) | ( `' f " { 1 } ) e. Fin }
42	8, 41	eqtr2i 2497	. . . . 5 |- { f e. ( { 0 , 1 } ^m NN ) | ( `' f " { 1 } ) e. Fin } = ( ( { 0 , 1 } ^m NN ) i^i R )
43		f1oeq3 5809	. . . . 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 ) ) )
44	42, 43	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 ) )
45	3, 44	mpbi 208	. . 3 |- ( (𝟭 ` NN ) |` Fin ) : ( ~P NN i^i Fin ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R )
46		eulerpart.j	. . . . . . 7 |- J = { z e. NN | -. 2 || z }
47		eulerpart.f	. . . . . . 7 |- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )
48	46, 47	oddpwdc 27961	. . . . . 6 |- F : ( J X. NN0 ) -1-1-onto-> NN
49		f1opwfi 7824	. . . . . 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 ) )
50	48, 49	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 )
51		eulerpart.p	. . . . . . . 8 |- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }
52		eulerpart.o	. . . . . . . 8 |- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }
53		eulerpart.d	. . . . . . . 8 |- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }
54		eulerpart.h	. . . . . . . 8 |- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }
55		eulerpart.m	. . . . . . . 8 |- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )
56	51, 52, 53, 46, 47, 54, 55	eulerpartlem1 27974	. . . . . . 7 |- M : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin )
57		bitsf1o 13954	. . . . . . . . . . . . . 14 |- (bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin )
58	57	a1i 11	. . . . . . . . . . . . 13 |- ( T. -> (bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) )
59	1	rabex 4598	. . . . . . . . . . . . . . 15 |- { z e. NN | -. 2 || z } e. _V
60	46, 59	eqeltri 2551	. . . . . . . . . . . . . 14 |- J e. _V
61	60	a1i 11	. . . . . . . . . . . . 13 |- ( T. -> J e. _V )
62		nn0ex 10801	. . . . . . . . . . . . . 14 |- NN0 e. _V
63	62	a1i 11	. . . . . . . . . . . . 13 |- ( T. -> NN0 e. _V )
64	62	pwex 4630	. . . . . . . . . . . . . . 15 |- ~P NN0 e. _V
65	64	inex1 4588	. . . . . . . . . . . . . 14 |- ( ~P NN0 i^i Fin ) e. _V
66	65	a1i 11	. . . . . . . . . . . . 13 |- ( T. -> ( ~P NN0 i^i Fin ) e. _V )
67		0nn0 10810	. . . . . . . . . . . . . 14 |- 0 e. NN0
68	67	a1i 11	. . . . . . . . . . . . 13 |- ( T. -> 0 e. NN0 )
69		fvres 5880	. . . . . . . . . . . . . . 15 |- ( 0 e. NN0 -> ( (bits |` NN0 ) ` 0 ) = (bits ` 0 ) )
70	67, 69	ax-mp 5	. . . . . . . . . . . . . 14 |- ( (bits |` NN0 ) ` 0 ) = (bits ` 0 )
71		0bits 13948	. . . . . . . . . . . . . 14 |- (bits ` 0 ) = (/)
72	70, 71	eqtr2i 2497	. . . . . . . . . . . . 13 |- (/) = ( (bits |` NN0 ) ` 0 )
73		elmapi 7440	. . . . . . . . . . . . . . . . 17 |- ( f e. ( NN0 ^m J ) -> f : J --> NN0 )
74		frnnn0supp 10849	. . . . . . . . . . . . . . . . . 18 |- ( ( J e. _V /\ f : J --> NN0 ) -> ( f supp 0 ) = ( `' f " NN ) )
75	60, 74	mpan 670	. . . . . . . . . . . . . . . . 17 |- ( f : J --> NN0 -> ( f supp 0 ) = ( `' f " NN ) )
76	73, 75	syl 16	. . . . . . . . . . . . . . . 16 |- ( f e. ( NN0 ^m J ) -> ( f supp 0 ) = ( `' f " NN ) )
77	76	eleq1d 2536	. . . . . . . . . . . . . . 15 |- ( f e. ( NN0 ^m J ) -> ( ( f supp 0 ) e. Fin <-> ( `' f " NN ) e. Fin ) )
78	77	rabbiia 3102	. . . . . . . . . . . . . 14 |- { f e. ( NN0 ^m J ) | ( f supp 0 ) e. Fin } = { f e. ( NN0 ^m J ) | ( `' f " NN ) e. Fin }
79		elmapfun 7442	. . . . . . . . . . . . . . . 16 |- ( f e. ( NN0 ^m J ) -> Fun f )
80		vex 3116	. . . . . . . . . . . . . . . . 17 |- f e. _V
81		funisfsupp 7834	. . . . . . . . . . . . . . . . 17 |- ( ( Fun f /\ f e. _V /\ 0 e. NN0 ) -> ( f finSupp 0 <-> ( f supp 0 ) e. Fin ) )
82	80, 67, 81	mp3an23 1316	. . . . . . . . . . . . . . . 16 |- ( Fun f -> ( f finSupp 0 <-> ( f supp 0 ) e. Fin ) )
83	79, 82	syl 16	. . . . . . . . . . . . . . 15 |- ( f e. ( NN0 ^m J ) -> ( f finSupp 0 <-> ( f supp 0 ) e. Fin ) )
84	83	rabbiia 3102	. . . . . . . . . . . . . 14 |- { f e. ( NN0 ^m J ) | f finSupp 0 } = { f e. ( NN0 ^m J ) | ( f supp 0 ) e. Fin }
85		incom 3691	. . . . . . . . . . . . . . 15 |- ( { f | ( `' f " NN ) e. Fin } i^i ( NN0 ^m J ) ) = ( ( NN0 ^m J ) i^i { f | ( `' f " NN ) e. Fin } )
86		dfrab2 3774	. . . . . . . . . . . . . . 15 |- { f e. ( NN0 ^m J ) | ( `' f " NN ) e. Fin } = ( { f | ( `' f " NN ) e. Fin } i^i ( NN0 ^m J ) )
87	5	ineq2i 3697	. . . . . . . . . . . . . . 15 |- ( ( NN0 ^m J ) i^i R ) = ( ( NN0 ^m J ) i^i { f | ( `' f " NN ) e. Fin } )
88	85, 86, 87	3eqtr4ri 2507	. . . . . . . . . . . . . 14 |- ( ( NN0 ^m J ) i^i R ) = { f e. ( NN0 ^m J ) | ( `' f " NN ) e. Fin }
89	78, 84, 88	3eqtr4ri 2507	. . . . . . . . . . . . 13 |- ( ( NN0 ^m J ) i^i R ) = { f e. ( NN0 ^m J ) | f finSupp 0 }
90		elmapfun 7442	. . . . . . . . . . . . . . 15 |- ( r e. ( ( ~P NN0 i^i Fin ) ^m J ) -> Fun r )
91		vex 3116	. . . . . . . . . . . . . . . . 17 |- r e. _V
92		0ex 4577	. . . . . . . . . . . . . . . . 17 |- (/) e. _V
93		funisfsupp 7834	. . . . . . . . . . . . . . . . 17 |- ( ( Fun r /\ r e. _V /\ (/) e. _V ) -> ( r finSupp (/) <-> ( r supp (/) ) e. Fin ) )
94	91, 92, 93	mp3an23 1316	. . . . . . . . . . . . . . . 16 |- ( Fun r -> ( r finSupp (/) <-> ( r supp (/) ) e. Fin ) )
95	94	bicomd 201	. . . . . . . . . . . . . . 15 |- ( Fun r -> ( ( r supp (/) ) e. Fin <-> r finSupp (/) ) )
96	90, 95	syl 16	. . . . . . . . . . . . . 14 |- ( r e. ( ( ~P NN0 i^i Fin ) ^m J ) -> ( ( r supp (/) ) e. Fin <-> r finSupp (/) ) )
97	96	rabbiia 3102	. . . . . . . . . . . . 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 (/) }
98	58, 61, 63, 66, 68, 72, 89, 97	fcobijfs 27249	. . . . . . . . . . . 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 } )
99		inss1 3718	. . . . . . . . . . . . . . . . 17 |- ( ( NN0 ^m J ) i^i R ) C_ ( NN0 ^m J )
100	99	sseli 3500	. . . . . . . . . . . . . . . 16 |- ( f e. ( ( NN0 ^m J ) i^i R ) -> f e. ( NN0 ^m J ) )
101		frn 5737	. . . . . . . . . . . . . . . . 17 |- ( f : J --> NN0 -> ran f C_ NN0 )
102		cores 5510	. . . . . . . . . . . . . . . . 17 |- ( ran f C_ NN0 -> ( (bits |` NN0 ) o. f ) = (bits o. f ) )
103	73, 101, 102	3syl 20	. . . . . . . . . . . . . . . 16 |- ( f e. ( NN0 ^m J ) -> ( (bits |` NN0 ) o. f ) = (bits o. f ) )
104	100, 103	syl 16	. . . . . . . . . . . . . . 15 |- ( f e. ( ( NN0 ^m J ) i^i R ) -> ( (bits |` NN0 ) o. f ) = (bits o. f ) )
105	104	mpteq2ia 4529	. . . . . . . . . . . . . 14 |- ( f e. ( ( NN0 ^m J ) i^i R ) |-> ( (bits |` NN0 ) o. f ) ) = ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) )
106	105	eqcomi 2480	. . . . . . . . . . . . 13 |- ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) = ( f e. ( ( NN0 ^m J ) i^i R ) |-> ( (bits |` NN0 ) o. f ) )
107		f1oeq1 5807	. . . . . . . . . . . . 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 } ) )
108	106, 107	mp1i 12	. . . . . . . . . . . 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 } ) )
109	98, 108	mpbird 232	. . . . . . . . . . 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 } )
110	109	trud 1388	. . . . . . . . . 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 }
111		ssrab2 3585	. . . . . . . . . . . . . . . 16 |- { z e. NN | -. 2 || z } C_ NN
112	46, 111	eqsstri 3534	. . . . . . . . . . . . . . 15 |- J C_ NN
113	1, 62, 112	3pm3.2i 1174	. . . . . . . . . . . . . 14 |- ( NN e. _V /\ NN0 e. _V /\ J C_ NN )
114		eulerpart.t	. . . . . . . . . . . . . . . 16 |- T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }
115		cnveq 5176	. . . . . . . . . . . . . . . . . . 19 |- ( f = o -> `' f = `' o )
116		dfn2 10808	. . . . . . . . . . . . . . . . . . . 20 |- NN = ( NN0 \ { 0 } )
117	116	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( f = o -> NN = ( NN0 \ { 0 } ) )
118	115, 117	imaeq12d 5338	. . . . . . . . . . . . . . . . . 18 |- ( f = o -> ( `' f " NN ) = ( `' o " ( NN0 \ { 0 } ) ) )
119	118	sseq1d 3531	. . . . . . . . . . . . . . . . 17 |- ( f = o -> ( ( `' f " NN ) C_ J <-> ( `' o " ( NN0 \ { 0 } ) ) C_ J ) )
120	119	cbvrabv 3112	. . . . . . . . . . . . . . . 16 |- { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J } = { o e. ( NN0 ^m NN ) | ( `' o " ( NN0 \ { 0 } ) ) C_ J }
121	114, 120	eqtri 2496	. . . . . . . . . . . . . . 15 |- T = { o e. ( NN0 ^m NN ) | ( `' o " ( NN0 \ { 0 } ) ) C_ J }
122		eqid 2467	. . . . . . . . . . . . . . 15 |- ( o e. T |-> ( o |` J ) ) = ( o e. T |-> ( o |` J ) )
123	121, 122	resf1o 27253	. . . . . . . . . . . . . 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 ) )
124	113, 67, 123	mp2an 672	. . . . . . . . . . . . 13 |- ( o e. T |-> ( o |` J ) ) : T -1-1-onto-> ( NN0 ^m J )
125		f1of1 5815	. . . . . . . . . . . . 13 |- ( ( o e. T |-> ( o |` J ) ) : T -1-1-onto-> ( NN0 ^m J ) -> ( o e. T |-> ( o |` J ) ) : T -1-1-> ( NN0 ^m J ) )
126	124, 125	ax-mp 5	. . . . . . . . . . . 12 |- ( o e. T |-> ( o |` J ) ) : T -1-1-> ( NN0 ^m J )
127		inss1 3718	. . . . . . . . . . . 12 |- ( T i^i R ) C_ T
128		f1ores 5830	. . . . . . . . . . . 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 ) ) )
129	126, 127, 128	mp2an 672	. . . . . . . . . . 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 ) )
130		vex 3116	. . . . . . . . . . . . . . . . . 18 |- o e. _V
131	130	resex 5317	. . . . . . . . . . . . . . . . 17 |- ( o |` J ) e. _V
132	131, 122	fnmpti 5709	. . . . . . . . . . . . . . . 16 |- ( o e. T |-> ( o |` J ) ) Fn T
133		fvelimab 5923	. . . . . . . . . . . . . . . 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 ) )
134	132, 127, 133	mp2an 672	. . . . . . . . . . . . . . 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 )
135		eqid 2467	. . . . . . . . . . . . . . . . 17 |- ( m e. ( T i^i R ) |-> ( m |` J ) ) = ( m e. ( T i^i R ) |-> ( m |` J ) )
136		vex 3116	. . . . . . . . . . . . . . . . . 18 |- m e. _V
137	136	resex 5317	. . . . . . . . . . . . . . . . 17 |- ( m |` J ) e. _V
138	135, 137	elrnmpti 5253	. . . . . . . . . . . . . . . 16 |- ( f e. ran ( m e. ( T i^i R ) |-> ( m |` J ) ) <-> E. m e. ( T i^i R ) f = ( m |` J ) )
139	51, 52, 53, 46, 47, 54, 55, 5, 114	eulerpartlemt 27978	. . . . . . . . . . . . . . . . 17 |- ( ( NN0 ^m J ) i^i R ) = ran ( m e. ( T i^i R ) |-> ( m |` J ) )
140	139	eleq2i 2545	. . . . . . . . . . . . . . . 16 |- ( f e. ( ( NN0 ^m J ) i^i R ) <-> f e. ran ( m e. ( T i^i R ) |-> ( m |` J ) ) )
141	127	sseli 3500	. . . . . . . . . . . . . . . . . . 19 |- ( m e. ( T i^i R ) -> m e. T )
142		reseq1 5267	. . . . . . . . . . . . . . . . . . . . 21 |- ( o = m -> ( o |` J ) = ( m |` J ) )
143	142, 122, 137	fvmpt 5950	. . . . . . . . . . . . . . . . . . . 20 |- ( m e. T -> ( ( o e. T |-> ( o |` J ) ) ` m ) = ( m |` J ) )
144	143	eqeq1d 2469	. . . . . . . . . . . . . . . . . . 19 |- ( m e. T -> ( ( ( o e. T |-> ( o |` J ) ) ` m ) = f <-> ( m |` J ) = f ) )
145	141, 144	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( m e. ( T i^i R ) -> ( ( ( o e. T |-> ( o |` J ) ) ` m ) = f <-> ( m |` J ) = f ) )
146		eqcom 2476	. . . . . . . . . . . . . . . . . . 19 |- ( ( m |` J ) = f <-> f = ( m |` J ) )
147	146	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( m e. ( T i^i R ) -> ( ( m |` J ) = f <-> f = ( m |` J ) ) )
148	145, 147	bitrd 253	. . . . . . . . . . . . . . . . 17 |- ( m e. ( T i^i R ) -> ( ( ( o e. T |-> ( o |` J ) ) ` m ) = f <-> f = ( m |` J ) ) )
149	148	rexbiia 2964	. . . . . . . . . . . . . . . 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 ) )
150	138, 140, 149	3bitr4ri 278	. . . . . . . . . . . . . . 15 |- ( E. m e. ( T i^i R ) ( ( o e. T |-> ( o |` J ) ) ` m ) = f <-> f e. ( ( NN0 ^m J ) i^i R ) )
151	134, 150	bitri 249	. . . . . . . . . . . . . 14 |- ( f e. ( ( o e. T |-> ( o |` J ) ) " ( T i^i R ) ) <-> f e. ( ( NN0 ^m J ) i^i R ) )
152	151	eqriv 2463	. . . . . . . . . . . . 13 |- ( ( o e. T |-> ( o |` J ) ) " ( T i^i R ) ) = ( ( NN0 ^m J ) i^i R )
153		f1oeq3 5809	. . . . . . . . . . . . 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 ) ) )
154	152, 153	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 ) )
155		resmpt 5323	. . . . . . . . . . . . . 14 |- ( ( T i^i R ) C_ T -> ( ( o e. T |-> ( o |` J ) ) |` ( T i^i R ) ) = ( o e. ( T i^i R ) |-> ( o |` J ) ) )
156	127, 155	ax-mp 5	. . . . . . . . . . . . 13 |- ( ( o e. T |-> ( o |` J ) ) |` ( T i^i R ) ) = ( o e. ( T i^i R ) |-> ( o |` J ) )
157		f1oeq1 5807	. . . . . . . . . . . . 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 ) ) )
158	156, 157	ax-mp 5	. . . . . . . . . . . 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 ) )
159	154, 158	bitri 249	. . . . . . . . . . 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 ) )
160	129, 159	mpbi 208	. . . . . . . . . 10 |- ( o e. ( T i^i R ) |-> ( o |` J ) ) : ( T i^i R ) -1-1-onto-> ( ( NN0 ^m J ) i^i R )
161		f1oco 5838	. . . . . . . . . 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 } )
162	110, 160, 161	mp2an 672	. . . . . . . . 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 }
163		f1of 5816	. . . . . . . . . . . . . . 15 |- ( ( 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 ) )
164		eqid 2467	. . . . . . . . . . . . . . . . 17 |- ( o e. ( T i^i R ) |-> ( o |` J ) ) = ( o e. ( T i^i R ) |-> ( o |` J ) )
165	164	fmpt 6042	. . . . . . . . . . . . . . . 16 |- ( 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 ) )
166	165	biimpri 206	. . . . . . . . . . . . . . 15 |- ( ( 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 ) )
167	160, 163, 166	mp2b 10	. . . . . . . . . . . . . 14 |- A. o e. ( T i^i R ) ( o |` J ) e. ( ( NN0 ^m J ) i^i R )
168	167	a1i 11	. . . . . . . . . . . . 13 |- ( T. -> A. o e. ( T i^i R ) ( o |` J ) e. ( ( NN0 ^m J ) i^i R ) )
169	168	r19.21bi 2833	. . . . . . . . . . . 12 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( o |` J ) e. ( ( NN0 ^m J ) i^i R ) )
170		eqidd 2468	. . . . . . . . . . . 12 |- ( T. -> ( o e. ( T i^i R ) |-> ( o |` J ) ) = ( o e. ( T i^i R ) |-> ( o |` J ) ) )
171		eqidd 2468	. . . . . . . . . . . 12 |- ( T. -> ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) = ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) )
172		coeq2 5161	. . . . . . . . . . . 12 |- ( f = ( o |` J ) -> (bits o. f ) = (bits o. ( o |` J ) ) )
173	169, 170, 171, 172	fmptco 6054	. . . . . . . . . . 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 ) ) ) )
174	173	eqcomd 2475	. . . . . . . . . 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 ) ) ) )
175		eqidd 2468	. . . . . . . . . 10 |- ( T. -> ( T i^i R ) = ( T i^i R ) )
176	54	a1i 11	. . . . . . . . . 10 |- ( T. -> H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin } )
177	174, 175, 176	f1oeq123d 5813	. . . . . . . . 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 } ) )
178	162, 177	mpbiri 233	. . . . . . . 8 |- ( T. -> ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) : ( T i^i R ) -1-1-onto-> H )
179	178	trud 1388	. . . . . . 7 |- ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) : ( T i^i R ) -1-1-onto-> H
180		f1oco 5838	. . . . . . 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 ) )
181	56, 179, 180	mp2an 672	. . . . . 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 )
182		eqidd 2468	. . . . . . . . . . 11 |- ( T. -> ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) = ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) )
183		bitsf 13936	. . . . . . . . . . . . . 14 |- bits : ZZ --> ~P NN0
184		zex 10873	. . . . . . . . . . . . . 14 |- ZZ e. _V
185		fex 6133	. . . . . . . . . . . . . 14 |- ( (bits : ZZ --> ~P NN0 /\ ZZ e. _V ) -> bits e. _V )
186	183, 184, 185	mp2an 672	. . . . . . . . . . . . 13 |- bits e. _V
187	186, 131	coex 6736	. . . . . . . . . . . 12 |- (bits o. ( o |` J ) ) e. _V
188	187	a1i 11	. . . . . . . . . . 11 |- ( ( T. /\ o e. ( T i^i R ) ) -> (bits o. ( o |` J ) ) e. _V )
189	182, 188	fvmpt2d 5959	. . . . . . . . . 10 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) ` o ) = (bits o. ( o |` J ) ) )
190		f1of 5816	. . . . . . . . . . . 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 )
191	179, 190	mp1i 12	. . . . . . . . . . 11 |- ( T. -> ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) : ( T i^i R ) --> H )
192	191	ffvelrnda 6021	. . . . . . . . . 10 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) ` o ) e. H )
193	189, 192	eqeltrrd 2556	. . . . . . . . 9 |- ( ( T. /\ o e. ( T i^i R ) ) -> (bits o. ( o |` J ) ) e. H )
194		f1ofn 5817	. . . . . . . . . . . 12 |- ( M : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin ) -> M Fn H )
195	56, 194	ax-mp 5	. . . . . . . . . . 11 |- M Fn H
196		dffn5 5913	. . . . . . . . . . 11 |- ( M Fn H <-> M = ( r e. H |-> ( M ` r ) ) )
197	195, 196	mpbi 208	. . . . . . . . . 10 |- M = ( r e. H |-> ( M ` r ) )
198	197	a1i 11	. . . . . . . . 9 |- ( T. -> M = ( r e. H |-> ( M ` r ) ) )
199		fveq2 5866	. . . . . . . . 9 |- ( r = (bits o. ( o |` J ) ) -> ( M ` r ) = ( M ` (bits o. ( o |` J ) ) ) )
200	193, 182, 198, 199	fmptco 6054	. . . . . . . 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 ) ) ) ) )
201	200	trud 1388	. . . . . . 7 |- ( M o. ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) ) = ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) )
202		f1oeq1 5807	. . . . . . 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 ) ) )
203	201, 202	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 ) )
204	181, 203	mpbi 208	. . . . 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 )
205		f1oco 5838	. . . . 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 ) )
206	50, 204, 205	mp2an 672	. . . 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 )
207		simpr 461	. . . . . . . . 9 |- ( ( T. /\ o e. ( T i^i R ) ) -> o e. ( T i^i R ) )
208		fvex 5876	. . . . . . . . . 10 |- ( M ` (bits o. ( o |` J ) ) ) e. _V
209	208	a1i 11	. . . . . . . . 9 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( M ` (bits o. ( o |` J ) ) ) e. _V )
210		eqid 2467	. . . . . . . . . 10 |- ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) = ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) )
211	210	fvmpt2 5957	. . . . . . . . 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 ) ) ) )
212	207, 209, 211	syl2anc 661	. . . . . . . 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 ) ) ) )
213		f1of 5816	. . . . . . . . . 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 ) )
214	204, 213	mp1i 12	. . . . . . . . 9 |- ( T. -> ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) : ( T i^i R ) --> ( ~P ( J X. NN0 ) i^i Fin ) )
215	214	ffvelrnda 6021	. . . . . . . 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 ) )
216	212, 215	eqeltrrd 2556	. . . . . . 7 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( M ` (bits o. ( o |` J ) ) ) e. ( ~P ( J X. NN0 ) i^i Fin ) )
217		eqidd 2468	. . . . . . 7 |- ( T. -> ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) = ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) )
218		eqidd 2468	. . . . . . 7 |- ( T. -> ( a e. ( ~P ( J X. NN0 ) i^i Fin ) |-> ( F " a ) ) = ( a e. ( ~P ( J X. NN0 ) i^i Fin ) |-> ( F " a ) ) )
219		imaeq2 5333	. . . . . . 7 |- ( a = ( M ` (bits o. ( o |` J ) ) ) -> ( F " a ) = ( F " ( M ` (bits o. ( o |` J ) ) ) ) )
220	216, 217, 218, 219	fmptco 6054	. . . . . 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 ) ) ) ) ) )
221	220	trud 1388	. . . . 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 ) ) ) ) )
222		f1oeq1 5807	. . . . 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 ) ) )
223	221, 222	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 ) )
224	206, 223	mpbi 208	. . 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 )
225		f1oco 5838	. . 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 ) )
226	45, 224, 225	mp2an 672	. 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 )
227		eulerpart.g	. . . 4 |- G = ( o e. ( T i^i R ) |-> ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )
228	47	mpt2exg 6858	. . . . . . . . . . 11 |- ( ( J e. _V /\ NN0 e. _V ) -> F e. _V )
229	60, 62, 228	mp2an 672	. . . . . . . . . 10 |- F e. _V
230		imaexg 6721	. . . . . . . . . 10 |- ( F e. _V -> ( F " ( M ` (bits o. ( o |` J ) ) ) ) e. _V )
231	229, 230	ax-mp 5	. . . . . . . . 9 |- ( F " ( M ` (bits o. ( o |` J ) ) ) ) e. _V
232	231	a1i 11	. . . . . . . 8 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( F " ( M ` (bits o. ( o |` J ) ) ) ) e. _V )
233		eqid 2467	. . . . . . . . 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 ) ) ) ) )
234	233	fvmpt2 5957	. . . . . . . 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 ) ) ) ) )
235	207, 232, 234	syl2anc 661	. . . . . . 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 ) ) ) ) )
236		f1of 5816	. . . . . . . . 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 ) )
237	224, 236	mp1i 12	. . . . . . . 8 |- ( T. -> ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) : ( T i^i R ) --> ( ~P NN i^i Fin ) )
238	237	ffvelrnda 6021	. . . . . . 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 ) )
239	235, 238	eqeltrrd 2556	. . . . . 6 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( F " ( M ` (bits o. ( o |` J ) ) ) ) e. ( ~P NN i^i Fin ) )
240		eqidd 2468	. . . . . 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 ) ) ) ) ) )
241		indf1o 27705	. . . . . . . . . . 11 |- ( NN e. _V -> (𝟭 ` NN ) : ~P NN -1-1-onto-> ( { 0 , 1 } ^m NN ) )
242		f1ofn 5817	. . . . . . . . . . 11 |- ( (𝟭 ` NN ) : ~P NN -1-1-onto-> ( { 0 , 1 } ^m NN ) -> (𝟭 ` NN ) Fn ~P NN )
243	1, 241, 242	mp2b 10	. . . . . . . . . 10 |- (𝟭 ` NN ) Fn ~P NN
244		dffn5 5913	. . . . . . . . . 10 |- ( (𝟭 ` NN ) Fn ~P NN <-> (𝟭 ` NN ) = ( b e. ~P NN |-> ( (𝟭 ` NN ) ` b ) ) )
245	243, 244	mpbi 208	. . . . . . . . 9 |- (𝟭 ` NN ) = ( b e. ~P NN |-> ( (𝟭 ` NN ) ` b ) )
246	245	reseq1i 5269	. . . . . . . 8 |- ( (𝟭 ` NN ) |` Fin ) = ( ( b e. ~P NN |-> ( (𝟭 ` NN ) ` b ) ) |` Fin )
247		resmpt3 5324	. . . . . . . 8 |- ( ( b e. ~P NN |-> ( (𝟭 ` NN ) ` b ) ) |` Fin ) = ( b e. ( ~P NN i^i Fin ) |-> ( (𝟭 ` NN ) ` b ) )
248	246, 247	eqtri 2496	. . . . . . 7 |- ( (𝟭 ` NN ) |` Fin ) = ( b e. ( ~P NN i^i Fin ) |-> ( (𝟭 ` NN ) ` b ) )
249	248	a1i 11	. . . . . 6 |- ( T. -> ( (𝟭 ` NN ) |` Fin ) = ( b e. ( ~P NN i^i Fin ) |-> ( (𝟭 ` NN ) ` b ) ) )
250		fveq2 5866	. . . . . 6 |- ( b = ( F " ( M ` (bits o. ( o |` J ) ) ) ) -> ( (𝟭 ` NN ) ` b ) = ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )
251	239, 240, 249, 250	fmptco 6054	. . . . 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 ) ) ) ) ) ) )
252	251	trud 1388	. . . 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 ) ) ) ) ) )
253	227, 252	eqtr4i 2499	. . 3 |- G = ( ( (𝟭 ` NN ) |` Fin ) o. ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )
254		f1oeq1 5807	. . 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 ) ) )
255	253, 254	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 ) )
256	226, 255	mpbir 209	1 |- G : ( T i^i R ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R )

Syntax hints:   -. wn 3   <-> wb 184   /\ wa 369   /\ w3a 973   = wceq 1379   T. wtru 1380   e. wcel 1767   {cab 2452   A.wral 2814   E.wrex 2815   {crab 2818   _Vcvv 3113   \ cdif 3473   u. cun 3474   i^i cin 3475   C_ wss 3476   (/)c0 3785   ~Pcpw 4010   {csn 4027   {cpr 4029   class class class wbr 4447   {copab 4504   |-> cmpt 4505   X. cxp 4997   `'ccnv 4998   ran crn 5000   |` cres 5001   "cima 5002   o. ccom 5003   Fun wfun 5582   Fn wfn 5583   -->wf 5584   -1-1->wf1 5585   -1-1-onto->wf1o 5587   ` cfv 5588  (class class class)co 6284   |-> cmpt2 6286   supp csupp 6901   ^m cmap 7420   Fincfn 7516   finSupp cfsupp 7829   0cc0 9492   1c1 9493   x. cmul 9497   <_ cle 9629   NNcn 10536   2c2 10585   NN0cn0 10795   ZZcz 10864   ^cexp 12134   sum_csu 13471   || cdivides 13847  bitscbits 13928  𝟭cind 27692

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576  ax-inf2 8058  ax-ac2 8843  ax-cnex 9548  ax-resscn 9549  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-addrcl 9553  ax-mulcl 9554  ax-mulrcl 9555  ax-mulcom 9556  ax-addass 9557  ax-mulass 9558  ax-distr 9559  ax-i2m1 9560  ax-1ne0 9561  ax-1rid 9562  ax-rnegex 9563  ax-rrecex 9564  ax-cnre 9565  ax-pre-lttri 9566  ax-pre-lttrn 9567  ax-pre-ltadd 9568  ax-pre-mulgt0 9569  ax-pre-sup 9570

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-fal 1385  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-disj 4418  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-se 4839  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-isom 5597  df-riota 6245  df-ov 6287  df-oprab 6288  df-mpt2 6289  df-om 6685  df-1st 6784  df-2nd 6785  df-supp 6902  df-recs 7042  df-rdg 7076  df-1o 7130  df-2o 7131  df-oadd 7134  df-er 7311  df-map 7422  df-pm 7423  df-en 7517  df-dom 7518  df-sdom 7519  df-fin 7520  df-fsupp 7830  df-sup 7901  df-oi 7935  df-card 8320  df-acn 8323  df-ac 8497  df-cda 8548  df-pnf 9630  df-mnf 9631  df-xr 9632  df-ltxr 9633  df-le 9634  df-sub 9807  df-neg 9808  df-div 10207  df-nn 10537  df-2 10594  df-3 10595  df-n0 10796  df-z 10865  df-uz 11083  df-rp 11221  df-fz 11673  df-fzo 11793  df-fl 11897  df-mod 11965  df-seq 12076  df-exp 12135  df-hash 12374  df-cj 12895  df-re 12896  df-im 12897  df-sqrt 13031  df-abs 13032  df-clim 13274  df-sum 13472  df-dvds 13848  df-bits 13931  df-ind 27693

This theorem is referenced by:  eulerpartlemgf  27986  eulerpartlemgs2  27987  eulerpartlemn  27988