Theorem eulerpartgbij 29278

Description: Lemma for eulerpart 29288: 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 10637	. . . . 5 |- NN e. _V
2		indf1ofs 28921	. . . . 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 3616	. . . . . . 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 3622	. . . . . . 7 |- ( ( { 0 , 1 } ^m NN ) i^i R ) = ( ( { 0 , 1 } ^m NN ) i^i { f | ( `' f " NN ) e. Fin } )
7		dfrab2 3710	. . . . . . 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 2503	. . . . . 6 |- ( ( { 0 , 1 } ^m NN ) i^i R ) = { f e. ( { 0 , 1 } ^m NN ) | ( `' f " NN ) e. Fin }
9		elmapfun 7513	. . . . . . . . 9 |- ( f e. ( { 0 , 1 } ^m NN ) -> Fun f )
10		elmapi 7511	. . . . . . . . . 10 |- ( f e. ( { 0 , 1 } ^m NN ) -> f : NN --> { 0 , 1 } )
11		frn 5747	. . . . . . . . . 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 28312	. . . . . . . . . 10 |- ( ( Fun f /\ ran f C_ { 0 , 1 } ) -> ( `' f " NN ) = ( `' f " ( NN i^i { 0 , 1 } ) ) )
14		df-pr 3962	. . . . . . . . . . . . . 14 |- { 0 , 1 } = ( { 0 } u. { 1 } )
15	14	ineq2i 3622	. . . . . . . . . . . . 13 |- ( NN i^i { 0 , 1 } ) = ( NN i^i ( { 0 } u. { 1 } ) )
16		indi 3680	. . . . . . . . . . . . 13 |- ( NN i^i ( { 0 } u. { 1 } ) ) = ( ( NN i^i { 0 } ) u. ( NN i^i { 1 } ) )
17		0nnn 10663	. . . . . . . . . . . . . . 15 |- -. 0 e. NN
18		disjsn 4023	. . . . . . . . . . . . . . 15 |- ( ( NN i^i { 0 } ) = (/) <-> -. 0 e. NN )
19	17, 18	mpbir 214	. . . . . . . . . . . . . 14 |- ( NN i^i { 0 } ) = (/)
20		1nn 10642	. . . . . . . . . . . . . . . . 17 |- 1 e. NN
21		1ex 9656	. . . . . . . . . . . . . . . . . 18 |- 1 e. _V
22	21	snss 4087	. . . . . . . . . . . . . . . . 17 |- ( 1 e. NN <-> { 1 } C_ NN )
23	20, 22	mpbi 213	. . . . . . . . . . . . . . . 16 |- { 1 } C_ NN
24		dfss 3405	. . . . . . . . . . . . . . . 16 |- ( { 1 } C_ NN <-> { 1 } = ( { 1 } i^i NN ) )
25	23, 24	mpbi 213	. . . . . . . . . . . . . . 15 |- { 1 } = ( { 1 } i^i NN )
26		incom 3616	. . . . . . . . . . . . . . 15 |- ( { 1 } i^i NN ) = ( NN i^i { 1 } )
27	25, 26	eqtr2i 2494	. . . . . . . . . . . . . 14 |- ( NN i^i { 1 } ) = { 1 }
28	19, 27	uneq12i 3577	. . . . . . . . . . . . 13 |- ( ( NN i^i { 0 } ) u. ( NN i^i { 1 } ) ) = ( (/) u. { 1 } )
29	15, 16, 28	3eqtri 2497	. . . . . . . . . . . 12 |- ( NN i^i { 0 , 1 } ) = ( (/) u. { 1 } )
30		uncom 3569	. . . . . . . . . . . 12 |- ( (/) u. { 1 } ) = ( { 1 } u. (/) )
31		un0 3762	. . . . . . . . . . . 12 |- ( { 1 } u. (/) ) = { 1 }
32	29, 30, 31	3eqtri 2497	. . . . . . . . . . 11 |- ( NN i^i { 0 , 1 } ) = { 1 }
33	32	imaeq2i 5172	. . . . . . . . . 10 |- ( `' f " ( NN i^i { 0 , 1 } ) ) = ( `' f " { 1 } )
34	13, 33	syl6eq 2521	. . . . . . . . 9 |- ( ( Fun f /\ ran f C_ { 0 , 1 } ) -> ( `' f " NN ) = ( `' f " { 1 } ) )
35	9, 12, 34	syl2anc 673	. . . . . . . 8 |- ( f e. ( { 0 , 1 } ^m NN ) -> ( `' f " NN ) = ( `' f " { 1 } ) )
36	35	eleq1d 2533	. . . . . . 7 |- ( f e. ( { 0 , 1 } ^m NN ) -> ( ( `' f " NN ) e. Fin <-> ( `' f " { 1 } ) e. Fin ) )
37	36	rabbiia 3019	. . . . . 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 2494	. . . . 5 |- { f e. ( { 0 , 1 } ^m NN ) | ( `' f " { 1 } ) e. Fin } = ( ( { 0 , 1 } ^m NN ) i^i R )
39		f1oeq3 5820	. . . . 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 213	. . 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 29260	. . . . . 6 |- F : ( J X. NN0 ) -1-1-onto-> NN
45		f1opwfi 7896	. . . . . 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 29273	. . . . . . 7 |- M : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin )
53		bitsf1o 14498	. . . . . . . . . . . . . 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 4552	. . . . . . . . . . . . . 14 |- J e. _V
56	55	a1i 11	. . . . . . . . . . . . 13 |- ( T. -> J e. _V )
57		nn0ex 10899	. . . . . . . . . . . . . 14 |- NN0 e. _V
58	57	a1i 11	. . . . . . . . . . . . 13 |- ( T. -> NN0 e. _V )
59	57	pwex 4584	. . . . . . . . . . . . . . 15 |- ~P NN0 e. _V
60	59	inex1 4537	. . . . . . . . . . . . . 14 |- ( ~P NN0 i^i Fin ) e. _V
61	60	a1i 11	. . . . . . . . . . . . 13 |- ( T. -> ( ~P NN0 i^i Fin ) e. _V )
62		0nn0 10908	. . . . . . . . . . . . . 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 14492	. . . . . . . . . . . . . 14 |- (bits ` 0 ) = (/)
67	65, 66	eqtr2i 2494	. . . . . . . . . . . . 13 |- (/) = ( (bits |` NN0 ) ` 0 )
68		elmapi 7511	. . . . . . . . . . . . . . . . 17 |- ( f e. ( NN0 ^m J ) -> f : J --> NN0 )
69		frnnn0supp 10947	. . . . . . . . . . . . . . . . 17 |- ( ( J e. _V /\ f : J --> NN0 ) -> ( f supp 0 ) = ( `' f " NN ) )
70	55, 68, 69	sylancr 676	. . . . . . . . . . . . . . . 16 |- ( f e. ( NN0 ^m J ) -> ( f supp 0 ) = ( `' f " NN ) )
71	70	eleq1d 2533	. . . . . . . . . . . . . . 15 |- ( f e. ( NN0 ^m J ) -> ( ( f supp 0 ) e. Fin <-> ( `' f " NN ) e. Fin ) )
72	71	rabbiia 3019	. . . . . . . . . . . . . 14 |- { f e. ( NN0 ^m J ) | ( f supp 0 ) e. Fin } = { f e. ( NN0 ^m J ) | ( `' f " NN ) e. Fin }
73		elmapfun 7513	. . . . . . . . . . . . . . . 16 |- ( f e. ( NN0 ^m J ) -> Fun f )
74		vex 3034	. . . . . . . . . . . . . . . . 17 |- f e. _V
75		funisfsupp 7906	. . . . . . . . . . . . . . . . 17 |- ( ( Fun f /\ f e. _V /\ 0 e. NN0 ) -> ( f finSupp 0 <-> ( f supp 0 ) e. Fin ) )
76	74, 62, 75	mp3an23 1382	. . . . . . . . . . . . . . . 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 3019	. . . . . . . . . . . . . 14 |- { f e. ( NN0 ^m J ) | f finSupp 0 } = { f e. ( NN0 ^m J ) | ( f supp 0 ) e. Fin }
79		incom 3616	. . . . . . . . . . . . . . 15 |- ( { f | ( `' f " NN ) e. Fin } i^i ( NN0 ^m J ) ) = ( ( NN0 ^m J ) i^i { f | ( `' f " NN ) e. Fin } )
80		dfrab2 3710	. . . . . . . . . . . . . . 15 |- { f e. ( NN0 ^m J ) | ( `' f " NN ) e. Fin } = ( { f | ( `' f " NN ) e. Fin } i^i ( NN0 ^m J ) )
81	5	ineq2i 3622	. . . . . . . . . . . . . . 15 |- ( ( NN0 ^m J ) i^i R ) = ( ( NN0 ^m J ) i^i { f | ( `' f " NN ) e. Fin } )
82	79, 80, 81	3eqtr4ri 2504	. . . . . . . . . . . . . 14 |- ( ( NN0 ^m J ) i^i R ) = { f e. ( NN0 ^m J ) | ( `' f " NN ) e. Fin }
83	72, 78, 82	3eqtr4ri 2504	. . . . . . . . . . . . 13 |- ( ( NN0 ^m J ) i^i R ) = { f e. ( NN0 ^m J ) | f finSupp 0 }
84		elmapfun 7513	. . . . . . . . . . . . . . 15 |- ( r e. ( ( ~P NN0 i^i Fin ) ^m J ) -> Fun r )
85		vex 3034	. . . . . . . . . . . . . . . . 17 |- r e. _V
86		0ex 4528	. . . . . . . . . . . . . . . . 17 |- (/) e. _V
87		funisfsupp 7906	. . . . . . . . . . . . . . . . 17 |- ( ( Fun r /\ r e. _V /\ (/) e. _V ) -> ( r finSupp (/) <-> ( r supp (/) ) e. Fin ) )
88	85, 86, 87	mp3an23 1382	. . . . . . . . . . . . . . . 16 |- ( Fun r -> ( r finSupp (/) <-> ( r supp (/) ) e. Fin ) )
89	88	bicomd 206	. . . . . . . . . . . . . . 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 3019	. . . . . . . . . . . . 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 28386	. . . . . . . . . . . 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		elinel1 3610	. . . . . . . . . . . . . . . 16 |- ( f e. ( ( NN0 ^m J ) i^i R ) -> f e. ( NN0 ^m J ) )
94		frn 5747	. . . . . . . . . . . . . . . . 17 |- ( f : J --> NN0 -> ran f C_ NN0 )
95		cores 5345	. . . . . . . . . . . . . . . . 17 |- ( ran f C_ NN0 -> ( (bits |` NN0 ) o. f ) = (bits o. f ) )
96	68, 94, 95	3syl 18	. . . . . . . . . . . . . . . 16 |- ( f e. ( NN0 ^m J ) -> ( (bits |` NN0 ) o. f ) = (bits o. f ) )
97	93, 96	syl 17	. . . . . . . . . . . . . . 15 |- ( f e. ( ( NN0 ^m J ) i^i R ) -> ( (bits |` NN0 ) o. f ) = (bits o. f ) )
98	97	mpteq2ia 4478	. . . . . . . . . . . . . 14 |- ( f e. ( ( NN0 ^m J ) i^i R ) |-> ( (bits |` NN0 ) o. f ) ) = ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) )
99	98	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 ) )
100		f1oeq1 5818	. . . . . . . . . . . . 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 } ) )
101	99, 100	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 } ) )
102	92, 101	mpbird 240	. . . . . . . . . . 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 } )
103	102	trud 1461	. . . . . . . . . 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 }
104		ssrab2 3500	. . . . . . . . . . . . . . . 16 |- { z e. NN | -. 2 || z } C_ NN
105	42, 104	eqsstri 3448	. . . . . . . . . . . . . . 15 |- J C_ NN
106	1, 57, 105	3pm3.2i 1208	. . . . . . . . . . . . . 14 |- ( NN e. _V /\ NN0 e. _V /\ J C_ NN )
107		eulerpart.t	. . . . . . . . . . . . . . . 16 |- T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }
108		cnveq 5013	. . . . . . . . . . . . . . . . . . 19 |- ( f = o -> `' f = `' o )
109		dfn2 10906	. . . . . . . . . . . . . . . . . . . 20 |- NN = ( NN0 \ { 0 } )
110	109	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( f = o -> NN = ( NN0 \ { 0 } ) )
111	108, 110	imaeq12d 5175	. . . . . . . . . . . . . . . . . 18 |- ( f = o -> ( `' f " NN ) = ( `' o " ( NN0 \ { 0 } ) ) )
112	111	sseq1d 3445	. . . . . . . . . . . . . . . . 17 |- ( f = o -> ( ( `' f " NN ) C_ J <-> ( `' o " ( NN0 \ { 0 } ) ) C_ J ) )
113	112	cbvrabv 3030	. . . . . . . . . . . . . . . 16 |- { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J } = { o e. ( NN0 ^m NN ) | ( `' o " ( NN0 \ { 0 } ) ) C_ J }
114	107, 113	eqtri 2493	. . . . . . . . . . . . . . 15 |- T = { o e. ( NN0 ^m NN ) | ( `' o " ( NN0 \ { 0 } ) ) C_ J }
115		eqid 2471	. . . . . . . . . . . . . . 15 |- ( o e. T |-> ( o |` J ) ) = ( o e. T |-> ( o |` J ) )
116	114, 115	resf1o 28390	. . . . . . . . . . . . . 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 ) )
117	106, 62, 116	mp2an 686	. . . . . . . . . . . . 13 |- ( o e. T |-> ( o |` J ) ) : T -1-1-onto-> ( NN0 ^m J )
118		f1of1 5827	. . . . . . . . . . . . 13 |- ( ( o e. T |-> ( o |` J ) ) : T -1-1-onto-> ( NN0 ^m J ) -> ( o e. T |-> ( o |` J ) ) : T -1-1-> ( NN0 ^m J ) )
119	117, 118	ax-mp 5	. . . . . . . . . . . 12 |- ( o e. T |-> ( o |` J ) ) : T -1-1-> ( NN0 ^m J )
120		inss1 3643	. . . . . . . . . . . 12 |- ( T i^i R ) C_ T
121		f1ores 5842	. . . . . . . . . . . 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 ) ) )
122	119, 120, 121	mp2an 686	. . . . . . . . . . 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 ) )
123		vex 3034	. . . . . . . . . . . . . . . . . 18 |- o e. _V
124	123	resex 5154	. . . . . . . . . . . . . . . . 17 |- ( o |` J ) e. _V
125	124, 115	fnmpti 5716	. . . . . . . . . . . . . . . 16 |- ( o e. T |-> ( o |` J ) ) Fn T
126		fvelimab 5936	. . . . . . . . . . . . . . . 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 ) )
127	125, 120, 126	mp2an 686	. . . . . . . . . . . . . . 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 )
128		eqid 2471	. . . . . . . . . . . . . . . . 17 |- ( m e. ( T i^i R ) |-> ( m |` J ) ) = ( m e. ( T i^i R ) |-> ( m |` J ) )
129		vex 3034	. . . . . . . . . . . . . . . . . 18 |- m e. _V
130	129	resex 5154	. . . . . . . . . . . . . . . . 17 |- ( m |` J ) e. _V
131	128, 130	elrnmpti 5091	. . . . . . . . . . . . . . . 16 |- ( f e. ran ( m e. ( T i^i R ) |-> ( m |` J ) ) <-> E. m e. ( T i^i R ) f = ( m |` J ) )
132	47, 48, 49, 42, 43, 50, 51, 5, 107	eulerpartlemt 29277	. . . . . . . . . . . . . . . . 17 |- ( ( NN0 ^m J ) i^i R ) = ran ( m e. ( T i^i R ) |-> ( m |` J ) )
133	132	eleq2i 2541	. . . . . . . . . . . . . . . 16 |- ( f e. ( ( NN0 ^m J ) i^i R ) <-> f e. ran ( m e. ( T i^i R ) |-> ( m |` J ) ) )
134		elinel1 3610	. . . . . . . . . . . . . . . . . . 19 |- ( m e. ( T i^i R ) -> m e. T )
135	115	fvtresfn 5965	. . . . . . . . . . . . . . . . . . . 20 |- ( m e. T -> ( ( o e. T |-> ( o |` J ) ) ` m ) = ( m |` J ) )
136	135	eqeq1d 2473	. . . . . . . . . . . . . . . . . . 19 |- ( m e. T -> ( ( ( o e. T |-> ( o |` J ) ) ` m ) = f <-> ( m |` J ) = f ) )
137	134, 136	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( m e. ( T i^i R ) -> ( ( ( o e. T |-> ( o |` J ) ) ` m ) = f <-> ( m |` J ) = f ) )
138		eqcom 2478	. . . . . . . . . . . . . . . . . 18 |- ( ( m |` J ) = f <-> f = ( m |` J ) )
139	137, 138	syl6bb 269	. . . . . . . . . . . . . . . . 17 |- ( m e. ( T i^i R ) -> ( ( ( o e. T |-> ( o |` J ) ) ` m ) = f <-> f = ( m |` J ) ) )
140	139	rexbiia 2880	. . . . . . . . . . . . . . . 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 ) )
141	131, 133, 140	3bitr4ri 286	. . . . . . . . . . . . . . 15 |- ( E. m e. ( T i^i R ) ( ( o e. T |-> ( o |` J ) ) ` m ) = f <-> f e. ( ( NN0 ^m J ) i^i R ) )
142	127, 141	bitri 257	. . . . . . . . . . . . . 14 |- ( f e. ( ( o e. T |-> ( o |` J ) ) " ( T i^i R ) ) <-> f e. ( ( NN0 ^m J ) i^i R ) )
143	142	eqriv 2468	. . . . . . . . . . . . 13 |- ( ( o e. T |-> ( o |` J ) ) " ( T i^i R ) ) = ( ( NN0 ^m J ) i^i R )
144		f1oeq3 5820	. . . . . . . . . . . . 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 ) ) )
145	143, 144	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 ) )
146		resmpt 5160	. . . . . . . . . . . . 13 |- ( ( T i^i R ) C_ T -> ( ( o e. T |-> ( o |` J ) ) |` ( T i^i R ) ) = ( o e. ( T i^i R ) |-> ( o |` J ) ) )
147		f1oeq1 5818	. . . . . . . . . . . . 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 ) ) )
148	120, 146, 147	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 ) )
149	145, 148	bitri 257	. . . . . . . . . . 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 ) )
150	122, 149	mpbi 213	. . . . . . . . . 10 |- ( o e. ( T i^i R ) |-> ( o |` J ) ) : ( T i^i R ) -1-1-onto-> ( ( NN0 ^m J ) i^i R )
151		f1oco 5850	. . . . . . . . . 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 } )
152	103, 150, 151	mp2an 686	. . . . . . . . 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 }
153		f1of 5828	. . . . . . . . . . . . . 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 ) )
154		eqid 2471	. . . . . . . . . . . . . . . 16 |- ( o e. ( T i^i R ) |-> ( o |` J ) ) = ( o e. ( T i^i R ) |-> ( o |` J ) )
155	154	fmpt 6058	. . . . . . . . . . . . . . 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 ) )
156	155	biimpri 211	. . . . . . . . . . . . . 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 ) )
157	150, 153, 156	mp2b 10	. . . . . . . . . . . . 13 |- A. o e. ( T i^i R ) ( o |` J ) e. ( ( NN0 ^m J ) i^i R )
158	157	a1i 11	. . . . . . . . . . . 12 |- ( T. -> A. o e. ( T i^i R ) ( o |` J ) e. ( ( NN0 ^m J ) i^i R ) )
159		eqidd 2472	. . . . . . . . . . . 12 |- ( T. -> ( o e. ( T i^i R ) |-> ( o |` J ) ) = ( o e. ( T i^i R ) |-> ( o |` J ) ) )
160		eqidd 2472	. . . . . . . . . . . 12 |- ( T. -> ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) = ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) )
161		coeq2 4998	. . . . . . . . . . . 12 |- ( f = ( o |` J ) -> (bits o. f ) = (bits o. ( o |` J ) ) )
162	158, 159, 160, 161	fmptcof 6073	. . . . . . . . . . 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 ) ) ) )
163	162	eqcomd 2477	. . . . . . . . . 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 ) ) ) )
164		eqidd 2472	. . . . . . . . . 10 |- ( T. -> ( T i^i R ) = ( T i^i R ) )
165	50	a1i 11	. . . . . . . . . 10 |- ( T. -> H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin } )
166	163, 164, 165	f1oeq123d 5824	. . . . . . . . 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 } ) )
167	152, 166	mpbiri 241	. . . . . . . 8 |- ( T. -> ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) : ( T i^i R ) -1-1-onto-> H )
168	167	trud 1461	. . . . . . 7 |- ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) : ( T i^i R ) -1-1-onto-> H
169		f1oco 5850	. . . . . . 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 ) )
170	52, 168, 169	mp2an 686	. . . . . 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 )
171		eqidd 2472	. . . . . . . . . . 11 |- ( T. -> ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) = ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) )
172		bitsf 14479	. . . . . . . . . . . . . 14 |- bits : ZZ --> ~P NN0
173		zex 10970	. . . . . . . . . . . . . 14 |- ZZ e. _V
174		fex 6155	. . . . . . . . . . . . . 14 |- ( (bits : ZZ --> ~P NN0 /\ ZZ e. _V ) -> bits e. _V )
175	172, 173, 174	mp2an 686	. . . . . . . . . . . . 13 |- bits e. _V
176	175, 124	coex 6764	. . . . . . . . . . . 12 |- (bits o. ( o |` J ) ) e. _V
177	176	a1i 11	. . . . . . . . . . 11 |- ( ( T. /\ o e. ( T i^i R ) ) -> (bits o. ( o |` J ) ) e. _V )
178	171, 177	fvmpt2d 5974	. . . . . . . . . 10 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) ` o ) = (bits o. ( o |` J ) ) )
179		f1of 5828	. . . . . . . . . . . 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 )
180	167, 179	syl 17	. . . . . . . . . . 11 |- ( T. -> ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) : ( T i^i R ) --> H )
181	180	ffvelrnda 6037	. . . . . . . . . 10 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) ` o ) e. H )
182	178, 181	eqeltrrd 2550	. . . . . . . . 9 |- ( ( T. /\ o e. ( T i^i R ) ) -> (bits o. ( o |` J ) ) e. H )
183		f1ofn 5829	. . . . . . . . . . . 12 |- ( M : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin ) -> M Fn H )
184	52, 183	ax-mp 5	. . . . . . . . . . 11 |- M Fn H
185		dffn5 5924	. . . . . . . . . . 11 |- ( M Fn H <-> M = ( r e. H |-> ( M ` r ) ) )
186	184, 185	mpbi 213	. . . . . . . . . 10 |- M = ( r e. H |-> ( M ` r ) )
187	186	a1i 11	. . . . . . . . 9 |- ( T. -> M = ( r e. H |-> ( M ` r ) ) )
188		fveq2 5879	. . . . . . . . 9 |- ( r = (bits o. ( o |` J ) ) -> ( M ` r ) = ( M ` (bits o. ( o |` J ) ) ) )
189	182, 171, 187, 188	fmptco 6072	. . . . . . . 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 ) ) ) ) )
190	189	trud 1461	. . . . . . 7 |- ( M o. ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) ) = ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) )
191		f1oeq1 5818	. . . . . . 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 ) ) )
192	190, 191	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 ) )
193	170, 192	mpbi 213	. . . . 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 )
194		f1oco 5850	. . . . 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 ) )
195	46, 193, 194	mp2an 686	. . . 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 )
196		simpr 468	. . . . . . . . 9 |- ( ( T. /\ o e. ( T i^i R ) ) -> o e. ( T i^i R ) )
197		fvex 5889	. . . . . . . . 9 |- ( M ` (bits o. ( o |` J ) ) ) e. _V
198		eqid 2471	. . . . . . . . . 10 |- ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) = ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) )
199	198	fvmpt2 5972	. . . . . . . . 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 ) ) ) )
200	196, 197, 199	sylancl 675	. . . . . . . 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 ) ) ) )
201		f1of 5828	. . . . . . . . . 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 ) )
202	193, 201	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 ) )
203	202	ffvelrnda 6037	. . . . . . . 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 ) )
204	200, 203	eqeltrrd 2550	. . . . . . 7 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( M ` (bits o. ( o |` J ) ) ) e. ( ~P ( J X. NN0 ) i^i Fin ) )
205		eqidd 2472	. . . . . . 7 |- ( T. -> ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) = ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) )
206		eqidd 2472	. . . . . . 7 |- ( T. -> ( a e. ( ~P ( J X. NN0 ) i^i Fin ) |-> ( F " a ) ) = ( a e. ( ~P ( J X. NN0 ) i^i Fin ) |-> ( F " a ) ) )
207		imaeq2 5170	. . . . . . 7 |- ( a = ( M ` (bits o. ( o |` J ) ) ) -> ( F " a ) = ( F " ( M ` (bits o. ( o |` J ) ) ) ) )
208	204, 205, 206, 207	fmptco 6072	. . . . . 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 ) ) ) ) ) )
209	208	trud 1461	. . . . 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 ) ) ) ) )
210		f1oeq1 5818	. . . . 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 ) ) )
211	209, 210	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 ) )
212	195, 211	mpbi 213	. . 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 )
213		f1oco 5850	. . 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 ) )
214	41, 212, 213	mp2an 686	. 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 )
215		eulerpart.g	. . . 4 |- G = ( o e. ( T i^i R ) |-> ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )
216	43	mpt2exg 6887	. . . . . . . . . 10 |- ( ( J e. _V /\ NN0 e. _V ) -> F e. _V )
217	55, 57, 216	mp2an 686	. . . . . . . . 9 |- F e. _V
218		imaexg 6749	. . . . . . . . 9 |- ( F e. _V -> ( F " ( M ` (bits o. ( o |` J ) ) ) ) e. _V )
219	217, 218	ax-mp 5	. . . . . . . 8 |- ( F " ( M ` (bits o. ( o |` J ) ) ) ) e. _V
220		eqid 2471	. . . . . . . . 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 ) ) ) ) )
221	220	fvmpt2 5972	. . . . . . . 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 ) ) ) ) )
222	196, 219, 221	sylancl 675	. . . . . . 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 ) ) ) ) )
223		f1of 5828	. . . . . . . . 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 ) )
224	212, 223	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 ) )
225	224	ffvelrnda 6037	. . . . . . 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 ) )
226	222, 225	eqeltrrd 2550	. . . . . 6 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( F " ( M ` (bits o. ( o |` J ) ) ) ) e. ( ~P NN i^i Fin ) )
227		eqidd 2472	. . . . . 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 ) ) ) ) ) )
228		indf1o 28919	. . . . . . . . . . 11 |- ( NN e. _V -> (𝟭 ` NN ) : ~P NN -1-1-onto-> ( { 0 , 1 } ^m NN ) )
229		f1ofn 5829	. . . . . . . . . . 11 |- ( (𝟭 ` NN ) : ~P NN -1-1-onto-> ( { 0 , 1 } ^m NN ) -> (𝟭 ` NN ) Fn ~P NN )
230	1, 228, 229	mp2b 10	. . . . . . . . . 10 |- (𝟭 ` NN ) Fn ~P NN
231		dffn5 5924	. . . . . . . . . 10 |- ( (𝟭 ` NN ) Fn ~P NN <-> (𝟭 ` NN ) = ( b e. ~P NN |-> ( (𝟭 ` NN ) ` b ) ) )
232	230, 231	mpbi 213	. . . . . . . . 9 |- (𝟭 ` NN ) = ( b e. ~P NN |-> ( (𝟭 ` NN ) ` b ) )
233	232	reseq1i 5107	. . . . . . . 8 |- ( (𝟭 ` NN ) |` Fin ) = ( ( b e. ~P NN |-> ( (𝟭 ` NN ) ` b ) ) |` Fin )
234		resmpt3 5161	. . . . . . . 8 |- ( ( b e. ~P NN |-> ( (𝟭 ` NN ) ` b ) ) |` Fin ) = ( b e. ( ~P NN i^i Fin ) |-> ( (𝟭 ` NN ) ` b ) )
235	233, 234	eqtri 2493	. . . . . . 7 |- ( (𝟭 ` NN ) |` Fin ) = ( b e. ( ~P NN i^i Fin ) |-> ( (𝟭 ` NN ) ` b ) )
236	235	a1i 11	. . . . . 6 |- ( T. -> ( (𝟭 ` NN ) |` Fin ) = ( b e. ( ~P NN i^i Fin ) |-> ( (𝟭 ` NN ) ` b ) ) )
237		fveq2 5879	. . . . . 6 |- ( b = ( F " ( M ` (bits o. ( o |` J ) ) ) ) -> ( (𝟭 ` NN ) ` b ) = ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )
238	226, 227, 236, 237	fmptco 6072	. . . . 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 ) ) ) ) ) ) )
239	238	trud 1461	. . . 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 ) ) ) ) ) )
240	215, 239	eqtr4i 2496	. . 3 |- G = ( ( (𝟭 ` NN ) |` Fin ) o. ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )
241		f1oeq1 5818	. . 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 ) ) )
242	240, 241	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 ) )
243	214, 242	mpbir 214	1 |- G : ( T i^i R ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R )

Syntax hints:   -. wn 3   <-> wb 189   /\ wa 376   /\ w3a 1007   = wceq 1452   T. wtru 1453   e. wcel 1904   {cab 2457   A.wral 2756   E.wrex 2757   {crab 2760   _Vcvv 3031   \ cdif 3387   u. cun 3388   i^i cin 3389   C_ wss 3390   (/)c0 3722   ~Pcpw 3942   {csn 3959   {cpr 3961   class class class wbr 4395   {copab 4453   |-> cmpt 4454   X. cxp 4837   `'ccnv 4838   ran crn 4840   |` cres 4841   "cima 4842   o. ccom 4843   Fun wfun 5583   Fn wfn 5584   -->wf 5585   -1-1->wf1 5586   -1-1-onto->wf1o 5588   ` cfv 5589  (class class class)co 6308   |-> cmpt2 6310   supp csupp 6933   ^m cmap 7490   Fincfn 7587   finSupp cfsupp 7901   0cc0 9557   1c1 9558   x. cmul 9562   <_ cle 9694   NNcn 10631   2c2 10681   NN0cn0 10893   ZZcz 10961   ^cexp 12310   sum_csu 13829   || cdvds 14382  bitscbits 14471  𝟭cind 28906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-inf2 8164  ax-ac2 8911  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634  ax-pre-sup 9635

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-fal 1458  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-disj 4367  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-se 4799  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-1st 6812  df-2nd 6813  df-supp 6934  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-2o 7201  df-oadd 7204  df-er 7381  df-map 7492  df-pm 7493  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-fsupp 7902  df-sup 7974  df-inf 7975  df-oi 8043  df-card 8391  df-acn 8394  df-ac 8565  df-cda 8616  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-div 10292  df-nn 10632  df-2 10690  df-3 10691  df-n0 10894  df-z 10962  df-uz 11183  df-rp 11326  df-fz 11811  df-fzo 11943  df-fl 12061  df-mod 12130  df-seq 12252  df-exp 12311  df-hash 12554  df-cj 13239  df-re 13240  df-im 13241  df-sqrt 13375  df-abs 13376  df-clim 13629  df-sum 13830  df-dvds 14383  df-bits 14474  df-ind 28907

This theorem is referenced by:  eulerpartlemgf  29285  eulerpartlemgs2  29286  eulerpartlemn  29287