Theorem eulerpartgbij 26777

Description: Lemma for eulerpart 26787: 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 10349	. . . . 5 |- NN e. _V
2		indf1ofs 26504	. . . . 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 3564	. . . . . . 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 3570	. . . . . . 7 |- ( ( { 0 , 1 } ^m NN ) i^i R ) = ( ( { 0 , 1 } ^m NN ) i^i { f | ( `' f " NN ) e. Fin } )
7		dfrab2 3647	. . . . . . 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 2473	. . . . . 6 |- ( ( { 0 , 1 } ^m NN ) i^i R ) = { f e. ( { 0 , 1 } ^m NN ) | ( `' f " NN ) e. Fin }
9		elmapi 7255	. . . . . . . . . 10 |- ( f e. ( { 0 , 1 } ^m NN ) -> f : NN --> { 0 , 1 } )
10		ffun 5582	. . . . . . . . . 10 |- ( f : NN --> { 0 , 1 } -> Fun f )
11	9, 10	syl 16	. . . . . . . . 9 |- ( f e. ( { 0 , 1 } ^m NN ) -> Fun f )
12		frn 5586	. . . . . . . . . 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 25975	. . . . . . . . . 10 |- ( ( Fun f /\ ran f C_ { 0 , 1 } ) -> ( `' f " NN ) = ( `' f " ( NN i^i { 0 , 1 } ) ) )
15		df-pr 3901	. . . . . . . . . . . . . 14 |- { 0 , 1 } = ( { 0 } u. { 1 } )
16	15	ineq2i 3570	. . . . . . . . . . . . 13 |- ( NN i^i { 0 , 1 } ) = ( NN i^i ( { 0 } u. { 1 } ) )
17		indi 3617	. . . . . . . . . . . . 13 |- ( NN i^i ( { 0 } u. { 1 } ) ) = ( ( NN i^i { 0 } ) u. ( NN i^i { 1 } ) )
18		0nnn 10374	. . . . . . . . . . . . . . 15 |- -. 0 e. NN
19		disjsn 3957	. . . . . . . . . . . . . . 15 |- ( ( NN i^i { 0 } ) = (/) <-> -. 0 e. NN )
20	18, 19	mpbir 209	. . . . . . . . . . . . . 14 |- ( NN i^i { 0 } ) = (/)
21		1nn 10354	. . . . . . . . . . . . . . . . 17 |- 1 e. NN
22		1ex 9402	. . . . . . . . . . . . . . . . . 18 |- 1 e. _V
23	22	snss 4020	. . . . . . . . . . . . . . . . 17 |- ( 1 e. NN <-> { 1 } C_ NN )
24	21, 23	mpbi 208	. . . . . . . . . . . . . . . 16 |- { 1 } C_ NN
25		dfss 3364	. . . . . . . . . . . . . . . 16 |- ( { 1 } C_ NN <-> { 1 } = ( { 1 } i^i NN ) )
26	24, 25	mpbi 208	. . . . . . . . . . . . . . 15 |- { 1 } = ( { 1 } i^i NN )
27		eqcom 2445	. . . . . . . . . . . . . . . 16 |- ( { 1 } = ( { 1 } i^i NN ) <-> ( { 1 } i^i NN ) = { 1 } )
28		incom 3564	. . . . . . . . . . . . . . . . 17 |- ( { 1 } i^i NN ) = ( NN i^i { 1 } )
29	28	eqeq1i 2450	. . . . . . . . . . . . . . . 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 3529	. . . . . . . . . . . . 13 |- ( ( NN i^i { 0 } ) u. ( NN i^i { 1 } ) ) = ( (/) u. { 1 } )
33	16, 17, 32	3eqtri 2467	. . . . . . . . . . . 12 |- ( NN i^i { 0 , 1 } ) = ( (/) u. { 1 } )
34		uncom 3521	. . . . . . . . . . . 12 |- ( (/) u. { 1 } ) = ( { 1 } u. (/) )
35		un0 3683	. . . . . . . . . . . 12 |- ( { 1 } u. (/) ) = { 1 }
36	33, 34, 35	3eqtri 2467	. . . . . . . . . . 11 |- ( NN i^i { 0 , 1 } ) = { 1 }
37	36	imaeq2i 5188	. . . . . . . . . 10 |- ( `' f " ( NN i^i { 0 , 1 } ) ) = ( `' f " { 1 } )
38	14, 37	syl6eq 2491	. . . . . . . . 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 2509	. . . . . . 7 |- ( f e. ( { 0 , 1 } ^m NN ) -> ( ( `' f " NN ) e. Fin <-> ( `' f " { 1 } ) e. Fin ) )
41	40	rabbiia 2982	. . . . . 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 2464	. . . . 5 |- { f e. ( { 0 , 1 } ^m NN ) | ( `' f " { 1 } ) e. Fin } = ( ( { 0 , 1 } ^m NN ) i^i R )
43		f1oeq3 5655	. . . . 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 26759	. . . . . 6 |- F : ( J X. NN0 ) -1-1-onto-> NN
49		f1opwfi 7636	. . . . . 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 26772	. . . . . . 7 |- M : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin )
57		bitsf1o 13662	. . . . . . . . . . . . . 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 4464	. . . . . . . . . . . . . . 15 |- { z e. NN | -. 2 || z } e. _V
60	46, 59	eqeltri 2513	. . . . . . . . . . . . . 14 |- J e. _V
61	60	a1i 11	. . . . . . . . . . . . 13 |- ( T. -> J e. _V )
62		nn0ex 10606	. . . . . . . . . . . . . 14 |- NN0 e. _V
63	62	a1i 11	. . . . . . . . . . . . 13 |- ( T. -> NN0 e. _V )
64	62	pwex 4496	. . . . . . . . . . . . . . 15 |- ~P NN0 e. _V
65	64	inex1 4454	. . . . . . . . . . . . . 14 |- ( ~P NN0 i^i Fin ) e. _V
66	65	a1i 11	. . . . . . . . . . . . 13 |- ( T. -> ( ~P NN0 i^i Fin ) e. _V )
67		0nn0 10615	. . . . . . . . . . . . . 14 |- 0 e. NN0
68	67	a1i 11	. . . . . . . . . . . . 13 |- ( T. -> 0 e. NN0 )
69		fvres 5725	. . . . . . . . . . . . . . 15 |- ( 0 e. NN0 -> ( (bits |` NN0 ) ` 0 ) = (bits ` 0 ) )
70	67, 69	ax-mp 5	. . . . . . . . . . . . . 14 |- ( (bits |` NN0 ) ` 0 ) = (bits ` 0 )
71		0bits 13656	. . . . . . . . . . . . . 14 |- (bits ` 0 ) = (/)
72	70, 71	eqtr2i 2464	. . . . . . . . . . . . 13 |- (/) = ( (bits |` NN0 ) ` 0 )
73		elmapi 7255	. . . . . . . . . . . . . . . . 17 |- ( f e. ( NN0 ^m J ) -> f : J --> NN0 )
74		frnnn0supp 10654	. . . . . . . . . . . . . . . . . 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 2509	. . . . . . . . . . . . . . 15 |- ( f e. ( NN0 ^m J ) -> ( ( f supp 0 ) e. Fin <-> ( `' f " NN ) e. Fin ) )
78	77	rabbiia 2982	. . . . . . . . . . . . . 14 |- { f e. ( NN0 ^m J ) | ( f supp 0 ) e. Fin } = { f e. ( NN0 ^m J ) | ( `' f " NN ) e. Fin }
79		elmapfun 7257	. . . . . . . . . . . . . . . 16 |- ( f e. ( NN0 ^m J ) -> Fun f )
80		vex 2996	. . . . . . . . . . . . . . . . 17 |- f e. _V
81		funisfsupp 7646	. . . . . . . . . . . . . . . . 17 |- ( ( Fun f /\ f e. _V /\ 0 e. NN0 ) -> ( f finSupp 0 <-> ( f supp 0 ) e. Fin ) )
82	80, 67, 81	mp3an23 1306	. . . . . . . . . . . . . . . 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 2982	. . . . . . . . . . . . . 14 |- { f e. ( NN0 ^m J ) | f finSupp 0 } = { f e. ( NN0 ^m J ) | ( f supp 0 ) e. Fin }
85		incom 3564	. . . . . . . . . . . . . . 15 |- ( { f | ( `' f " NN ) e. Fin } i^i ( NN0 ^m J ) ) = ( ( NN0 ^m J ) i^i { f | ( `' f " NN ) e. Fin } )
86		dfrab2 3647	. . . . . . . . . . . . . . 15 |- { f e. ( NN0 ^m J ) | ( `' f " NN ) e. Fin } = ( { f | ( `' f " NN ) e. Fin } i^i ( NN0 ^m J ) )
87	5	ineq2i 3570	. . . . . . . . . . . . . . 15 |- ( ( NN0 ^m J ) i^i R ) = ( ( NN0 ^m J ) i^i { f | ( `' f " NN ) e. Fin } )
88	85, 86, 87	3eqtr4ri 2474	. . . . . . . . . . . . . 14 |- ( ( NN0 ^m J ) i^i R ) = { f e. ( NN0 ^m J ) | ( `' f " NN ) e. Fin }
89	78, 84, 88	3eqtr4ri 2474	. . . . . . . . . . . . 13 |- ( ( NN0 ^m J ) i^i R ) = { f e. ( NN0 ^m J ) | f finSupp 0 }
90		elmapfun 7257	. . . . . . . . . . . . . . 15 |- ( r e. ( ( ~P NN0 i^i Fin ) ^m J ) -> Fun r )
91		vex 2996	. . . . . . . . . . . . . . . . 17 |- r e. _V
92		0ex 4443	. . . . . . . . . . . . . . . . 17 |- (/) e. _V
93		funisfsupp 7646	. . . . . . . . . . . . . . . . 17 |- ( ( Fun r /\ r e. _V /\ (/) e. _V ) -> ( r finSupp (/) <-> ( r supp (/) ) e. Fin ) )
94	91, 92, 93	mp3an23 1306	. . . . . . . . . . . . . . . 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 2982	. . . . . . . . . . . . 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 26048	. . . . . . . . . . . 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 3591	. . . . . . . . . . . . . . . . 17 |- ( ( NN0 ^m J ) i^i R ) C_ ( NN0 ^m J )
100	99	sseli 3373	. . . . . . . . . . . . . . . 16 |- ( f e. ( ( NN0 ^m J ) i^i R ) -> f e. ( NN0 ^m J ) )
101		frn 5586	. . . . . . . . . . . . . . . . 17 |- ( f : J --> NN0 -> ran f C_ NN0 )
102		cores 5362	. . . . . . . . . . . . . . . . 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 4395	. . . . . . . . . . . . . 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 2447	. . . . . . . . . . . . 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 5653	. . . . . . . . . . . . 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 1378	. . . . . . . . . 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 3458	. . . . . . . . . . . . . . . 16 |- { z e. NN | -. 2 || z } C_ NN
112	46, 111	eqsstri 3407	. . . . . . . . . . . . . . 15 |- J C_ NN
113	1, 62, 112	3pm3.2i 1166	. . . . . . . . . . . . . 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 5034	. . . . . . . . . . . . . . . . . . 19 |- ( f = o -> `' f = `' o )
116		dfn2 10613	. . . . . . . . . . . . . . . . . . . 20 |- NN = ( NN0 \ { 0 } )
117	116	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( f = o -> NN = ( NN0 \ { 0 } ) )
118	115, 117	imaeq12d 5191	. . . . . . . . . . . . . . . . . 18 |- ( f = o -> ( `' f " NN ) = ( `' o " ( NN0 \ { 0 } ) ) )
119	118	sseq1d 3404	. . . . . . . . . . . . . . . . 17 |- ( f = o -> ( ( `' f " NN ) C_ J <-> ( `' o " ( NN0 \ { 0 } ) ) C_ J ) )
120	119	cbvrabv 2992	. . . . . . . . . . . . . . . 16 |- { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J } = { o e. ( NN0 ^m NN ) | ( `' o " ( NN0 \ { 0 } ) ) C_ J }
121	114, 120	eqtri 2463	. . . . . . . . . . . . . . 15 |- T = { o e. ( NN0 ^m NN ) | ( `' o " ( NN0 \ { 0 } ) ) C_ J }
122		eqid 2443	. . . . . . . . . . . . . . 15 |- ( o e. T |-> ( o |` J ) ) = ( o e. T |-> ( o |` J ) )
123	121, 122	resf1o 26052	. . . . . . . . . . . . . 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 5661	. . . . . . . . . . . . 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 3591	. . . . . . . . . . . 12 |- ( T i^i R ) C_ T
128		f1ores 5676	. . . . . . . . . . . 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 2996	. . . . . . . . . . . . . . . . . 18 |- o e. _V
131	130	resex 5171	. . . . . . . . . . . . . . . . 17 |- ( o |` J ) e. _V
132	131, 122	fnmpti 5560	. . . . . . . . . . . . . . . 16 |- ( o e. T |-> ( o |` J ) ) Fn T
133		fvelimab 5768	. . . . . . . . . . . . . . . 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 2443	. . . . . . . . . . . . . . . . 17 |- ( m e. ( T i^i R ) |-> ( m |` J ) ) = ( m e. ( T i^i R ) |-> ( m |` J ) )
136		vex 2996	. . . . . . . . . . . . . . . . . 18 |- m e. _V
137	136	resex 5171	. . . . . . . . . . . . . . . . 17 |- ( m |` J ) e. _V
138	135, 137	elrnmpti 5111	. . . . . . . . . . . . . . . 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 26776	. . . . . . . . . . . . . . . . 17 |- ( ( NN0 ^m J ) i^i R ) = ran ( m e. ( T i^i R ) |-> ( m |` J ) )
140	139	eleq2i 2507	. . . . . . . . . . . . . . . 16 |- ( f e. ( ( NN0 ^m J ) i^i R ) <-> f e. ran ( m e. ( T i^i R ) |-> ( m |` J ) ) )
141	127	sseli 3373	. . . . . . . . . . . . . . . . . . 19 |- ( m e. ( T i^i R ) -> m e. T )
142		reseq1 5125	. . . . . . . . . . . . . . . . . . . . 21 |- ( o = m -> ( o |` J ) = ( m |` J ) )
143	142, 122, 137	fvmpt 5795	. . . . . . . . . . . . . . . . . . . 20 |- ( m e. T -> ( ( o e. T |-> ( o |` J ) ) ` m ) = ( m |` J ) )
144	143	eqeq1d 2451	. . . . . . . . . . . . . . . . . . 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 2445	. . . . . . . . . . . . . . . . . . 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 2769	. . . . . . . . . . . . . . . 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 2440	. . . . . . . . . . . . 13 |- ( ( o e. T |-> ( o |` J ) ) " ( T i^i R ) ) = ( ( NN0 ^m J ) i^i R )
153		f1oeq3 5655	. . . . . . . . . . . . 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 5177	. . . . . . . . . . . . . 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 5653	. . . . . . . . . . . . 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 5684	. . . . . . . . . 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 5662	. . . . . . . . . . . . . . 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 2443	. . . . . . . . . . . . . . . . 17 |- ( o e. ( T i^i R ) |-> ( o |` J ) ) = ( o e. ( T i^i R ) |-> ( o |` J ) )
165	164	fmpt 5885	. . . . . . . . . . . . . . . 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 2835	. . . . . . . . . . . 12 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( o |` J ) e. ( ( NN0 ^m J ) i^i R ) )
170		eqidd 2444	. . . . . . . . . . . 12 |- ( T. -> ( o e. ( T i^i R ) |-> ( o |` J ) ) = ( o e. ( T i^i R ) |-> ( o |` J ) ) )
171		eqidd 2444	. . . . . . . . . . . 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 5019	. . . . . . . . . . . 12 |- ( f = ( o |` J ) -> (bits o. f ) = (bits o. ( o |` J ) ) )
173	169, 170, 171, 172	fmptco 5897	. . . . . . . . . . 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 2448	. . . . . . . . . 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 2444	. . . . . . . . . 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 5659	. . . . . . . . 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 1378	. . . . . . 7 |- ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) : ( T i^i R ) -1-1-onto-> H
180		f1oco 5684	. . . . . . 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 2444	. . . . . . . . . . 11 |- ( T. -> ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) = ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) )
183		bitsf 13644	. . . . . . . . . . . . . 14 |- bits : ZZ --> ~P NN0
184		zex 10676	. . . . . . . . . . . . . 14 |- ZZ e. _V
185		fex 5971	. . . . . . . . . . . . . 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 6550	. . . . . . . . . . . 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 5804	. . . . . . . . . 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 5662	. . . . . . . . . . . 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 5864	. . . . . . . . . 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 2518	. . . . . . . . 9 |- ( ( T. /\ o e. ( T i^i R ) ) -> (bits o. ( o |` J ) ) e. H )
194		f1ofn 5663	. . . . . . . . . . . 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 5758	. . . . . . . . . . 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 5712	. . . . . . . . 9 |- ( r = (bits o. ( o |` J ) ) -> ( M ` r ) = ( M ` (bits o. ( o |` J ) ) ) )
200	193, 182, 198, 199	fmptco 5897	. . . . . . . 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 1378	. . . . . . 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 5653	. . . . . . 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 5684	. . . . 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 5722	. . . . . . . . . 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 2443	. . . . . . . . . 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 5802	. . . . . . . . 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 5662	. . . . . . . . . 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 5864	. . . . . . . 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 2518	. . . . . . 7 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( M ` (bits o. ( o |` J ) ) ) e. ( ~P ( J X. NN0 ) i^i Fin ) )
217		eqidd 2444	. . . . . . 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 2444	. . . . . . 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 5186	. . . . . . 7 |- ( a = ( M ` (bits o. ( o |` J ) ) ) -> ( F " a ) = ( F " ( M ` (bits o. ( o |` J ) ) ) ) )
220	216, 217, 218, 219	fmptco 5897	. . . . . 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 1378	. . . . 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 5653	. . . . 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 5684	. . 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 6669	. . . . . . . . . . 11 |- ( ( J e. _V /\ NN0 e. _V ) -> F e. _V )
229	60, 62, 228	mp2an 672	. . . . . . . . . 10 |- F e. _V
230		imaexg 6536	. . . . . . . . . 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 2443	. . . . . . . . 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 5802	. . . . . . . 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 5662	. . . . . . . . 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 5864	. . . . . . 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 2518	. . . . . 6 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( F " ( M ` (bits o. ( o |` J ) ) ) ) e. ( ~P NN i^i Fin ) )
240		eqidd 2444	. . . . . 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 26502	. . . . . . . . . . 11 |- ( NN e. _V -> (𝟭 ` NN ) : ~P NN -1-1-onto-> ( { 0 , 1 } ^m NN ) )
242		f1ofn 5663	. . . . . . . . . . 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 5758	. . . . . . . . . 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 5127	. . . . . . . 8 |- ( (𝟭 ` NN ) |` Fin ) = ( ( b e. ~P NN |-> ( (𝟭 ` NN ) ` b ) ) |` Fin )
247		resmpt3 5178	. . . . . . . 8 |- ( ( b e. ~P NN |-> ( (𝟭 ` NN ) ` b ) ) |` Fin ) = ( b e. ( ~P NN i^i Fin ) |-> ( (𝟭 ` NN ) ` b ) )
248	246, 247	eqtri 2463	. . . . . . 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 5712	. . . . . 6 |- ( b = ( F " ( M ` (bits o. ( o |` J ) ) ) ) -> ( (𝟭 ` NN ) ` b ) = ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )
251	239, 240, 249, 250	fmptco 5897	. . . . 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 1378	. . . 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 2466	. . 3 |- G = ( ( (𝟭 ` NN ) |` Fin ) o. ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )
254		f1oeq1 5653	. . 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 965   = wceq 1369   T. wtru 1370   e. wcel 1756   {cab 2429   A.wral 2736   E.wrex 2737   {crab 2740   _Vcvv 2993   \ cdif 3346   u. cun 3347   i^i cin 3348   C_ wss 3349   (/)c0 3658   ~Pcpw 3881   {csn 3898   {cpr 3900   class class class wbr 4313   {copab 4370   e. cmpt 4371   X. cxp 4859   `'ccnv 4860   ran crn 4862   |` cres 4863   "cima 4864   o. ccom 4865   Fun wfun 5433   Fn wfn 5434   -->wf 5435   -1-1->wf1 5436   -1-1-onto->wf1o 5438   ` cfv 5439  (class class class)co 6112   e. cmpt2 6114   supp csupp 6711   ^m cmap 7235   Fincfn 7331   finSupp cfsupp 7641   0cc0 9303   1c1 9304   x. cmul 9308   <_ cle 9440   NNcn 10343   2c2 10392   NN0cn0 10600   ZZcz 10667   ^cexp 11886   sum_csu 13184   || cdivides 13556  bitscbits 13636  𝟭cind 26489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4424  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552  ax-un 6393  ax-inf2 7868  ax-ac2 8653  ax-cnex 9359  ax-resscn 9360  ax-1cn 9361  ax-icn 9362  ax-addcl 9363  ax-addrcl 9364  ax-mulcl 9365  ax-mulrcl 9366  ax-mulcom 9367  ax-addass 9368  ax-mulass 9369  ax-distr 9370  ax-i2m1 9371  ax-1ne0 9372  ax-1rid 9373  ax-rnegex 9374  ax-rrecex 9375  ax-cnre 9376  ax-pre-lttri 9377  ax-pre-lttrn 9378  ax-pre-ltadd 9379  ax-pre-mulgt0 9380  ax-pre-sup 9381

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-nel 2623  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 2995  df-sbc 3208  df-csb 3310  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-pss 3365  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-tp 3903  df-op 3905  df-uni 4113  df-int 4150  df-iun 4194  df-disj 4284  df-br 4314  df-opab 4372  df-mpt 4373  df-tr 4407  df-eprel 4653  df-id 4657  df-po 4662  df-so 4663  df-fr 4700  df-se 4701  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-iota 5402  df-fun 5441  df-fn 5442  df-f 5443  df-f1 5444  df-fo 5445  df-f1o 5446  df-fv 5447  df-isom 5448  df-riota 6073  df-ov 6115  df-oprab 6116  df-mpt2 6117  df-om 6498  df-1st 6598  df-2nd 6599  df-supp 6712  df-recs 6853  df-rdg 6887  df-1o 6941  df-2o 6942  df-oadd 6945  df-er 7122  df-map 7237  df-pm 7238  df-en 7332  df-dom 7333  df-sdom 7334  df-fin 7335  df-fsupp 7642  df-sup 7712  df-oi 7745  df-card 8130  df-acn 8133  df-ac 8307  df-cda 8358  df-pnf 9441  df-mnf 9442  df-xr 9443  df-ltxr 9444  df-le 9445  df-sub 9618  df-neg 9619  df-div 10015  df-nn 10344  df-2 10401  df-3 10402  df-n0 10601  df-z 10668  df-uz 10883  df-rp 11013  df-fz 11459  df-fzo 11570  df-fl 11663  df-mod 11730  df-seq 11828  df-exp 11887  df-hash 12125  df-cj 12609  df-re 12610  df-im 12611  df-sqr 12745  df-abs 12746  df-clim 12987  df-sum 13185  df-dvds 13557  df-bits 13639  df-ind 26490

This theorem is referenced by:  eulerpartlemgf  26784  eulerpartlemgs2  26785  eulerpartlemn  26786