Theorem eulerpartgbij 28830

Description: Lemma for eulerpart 28840: 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 10584	. . . . 5 |- NN e. _V
2		indf1ofs 28486	. . . . 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 3634	. . . . . . 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 3640	. . . . . . 7 |- ( ( { 0 , 1 } ^m NN ) i^i R ) = ( ( { 0 , 1 } ^m NN ) i^i { f | ( `' f " NN ) e. Fin } )
7		dfrab2 3728	. . . . . . 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 2443	. . . . . 6 |- ( ( { 0 , 1 } ^m NN ) i^i R ) = { f e. ( { 0 , 1 } ^m NN ) | ( `' f " NN ) e. Fin }
9		elmapfun 7482	. . . . . . . . 9 |- ( f e. ( { 0 , 1 } ^m NN ) -> Fun f )
10		elmapi 7480	. . . . . . . . . 10 |- ( f e. ( { 0 , 1 } ^m NN ) -> f : NN --> { 0 , 1 } )
11		frn 5722	. . . . . . . . . 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 27932	. . . . . . . . . 10 |- ( ( Fun f /\ ran f C_ { 0 , 1 } ) -> ( `' f " NN ) = ( `' f " ( NN i^i { 0 , 1 } ) ) )
14		df-pr 3977	. . . . . . . . . . . . . 14 |- { 0 , 1 } = ( { 0 } u. { 1 } )
15	14	ineq2i 3640	. . . . . . . . . . . . 13 |- ( NN i^i { 0 , 1 } ) = ( NN i^i ( { 0 } u. { 1 } ) )
16		indi 3698	. . . . . . . . . . . . 13 |- ( NN i^i ( { 0 } u. { 1 } ) ) = ( ( NN i^i { 0 } ) u. ( NN i^i { 1 } ) )
17		0nnn 10610	. . . . . . . . . . . . . . 15 |- -. 0 e. NN
18		disjsn 4034	. . . . . . . . . . . . . . 15 |- ( ( NN i^i { 0 } ) = (/) <-> -. 0 e. NN )
19	17, 18	mpbir 211	. . . . . . . . . . . . . 14 |- ( NN i^i { 0 } ) = (/)
20		1nn 10589	. . . . . . . . . . . . . . . . 17 |- 1 e. NN
21		1ex 9623	. . . . . . . . . . . . . . . . . 18 |- 1 e. _V
22	21	snss 4098	. . . . . . . . . . . . . . . . 17 |- ( 1 e. NN <-> { 1 } C_ NN )
23	20, 22	mpbi 210	. . . . . . . . . . . . . . . 16 |- { 1 } C_ NN
24		dfss 3431	. . . . . . . . . . . . . . . 16 |- ( { 1 } C_ NN <-> { 1 } = ( { 1 } i^i NN ) )
25	23, 24	mpbi 210	. . . . . . . . . . . . . . 15 |- { 1 } = ( { 1 } i^i NN )
26		incom 3634	. . . . . . . . . . . . . . 15 |- ( { 1 } i^i NN ) = ( NN i^i { 1 } )
27	25, 26	eqtr2i 2434	. . . . . . . . . . . . . 14 |- ( NN i^i { 1 } ) = { 1 }
28	19, 27	uneq12i 3597	. . . . . . . . . . . . 13 |- ( ( NN i^i { 0 } ) u. ( NN i^i { 1 } ) ) = ( (/) u. { 1 } )
29	15, 16, 28	3eqtri 2437	. . . . . . . . . . . 12 |- ( NN i^i { 0 , 1 } ) = ( (/) u. { 1 } )
30		uncom 3589	. . . . . . . . . . . 12 |- ( (/) u. { 1 } ) = ( { 1 } u. (/) )
31		un0 3766	. . . . . . . . . . . 12 |- ( { 1 } u. (/) ) = { 1 }
32	29, 30, 31	3eqtri 2437	. . . . . . . . . . 11 |- ( NN i^i { 0 , 1 } ) = { 1 }
33	32	imaeq2i 5157	. . . . . . . . . 10 |- ( `' f " ( NN i^i { 0 , 1 } ) ) = ( `' f " { 1 } )
34	13, 33	syl6eq 2461	. . . . . . . . 9 |- ( ( Fun f /\ ran f C_ { 0 , 1 } ) -> ( `' f " NN ) = ( `' f " { 1 } ) )
35	9, 12, 34	syl2anc 661	. . . . . . . 8 |- ( f e. ( { 0 , 1 } ^m NN ) -> ( `' f " NN ) = ( `' f " { 1 } ) )
36	35	eleq1d 2473	. . . . . . 7 |- ( f e. ( { 0 , 1 } ^m NN ) -> ( ( `' f " NN ) e. Fin <-> ( `' f " { 1 } ) e. Fin ) )
37	36	rabbiia 3050	. . . . . 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 2434	. . . . 5 |- { f e. ( { 0 , 1 } ^m NN ) | ( `' f " { 1 } ) e. Fin } = ( ( { 0 , 1 } ^m NN ) i^i R )
39		f1oeq3 5794	. . . . 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 210	. . 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 28812	. . . . . 6 |- F : ( J X. NN0 ) -1-1-onto-> NN
45		f1opwfi 7860	. . . . . 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 28825	. . . . . . 7 |- M : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin )
53		bitsf1o 14306	. . . . . . . . . . . . . 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 4549	. . . . . . . . . . . . . 14 |- J e. _V
56	55	a1i 11	. . . . . . . . . . . . 13 |- ( T. -> J e. _V )
57		nn0ex 10844	. . . . . . . . . . . . . 14 |- NN0 e. _V
58	57	a1i 11	. . . . . . . . . . . . 13 |- ( T. -> NN0 e. _V )
59	57	pwex 4579	. . . . . . . . . . . . . . 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 10853	. . . . . . . . . . . . . 14 |- 0 e. NN0
63	62	a1i 11	. . . . . . . . . . . . 13 |- ( T. -> 0 e. NN0 )
64		fvres 5865	. . . . . . . . . . . . . . 15 |- ( 0 e. NN0 -> ( (bits |` NN0 ) ` 0 ) = (bits ` 0 ) )
65	62, 64	ax-mp 5	. . . . . . . . . . . . . 14 |- ( (bits |` NN0 ) ` 0 ) = (bits ` 0 )
66		0bits 14300	. . . . . . . . . . . . . 14 |- (bits ` 0 ) = (/)
67	65, 66	eqtr2i 2434	. . . . . . . . . . . . 13 |- (/) = ( (bits |` NN0 ) ` 0 )
68		elmapi 7480	. . . . . . . . . . . . . . . . 17 |- ( f e. ( NN0 ^m J ) -> f : J --> NN0 )
69		frnnn0supp 10892	. . . . . . . . . . . . . . . . 17 |- ( ( J e. _V /\ f : J --> NN0 ) -> ( f supp 0 ) = ( `' f " NN ) )
70	55, 68, 69	sylancr 663	. . . . . . . . . . . . . . . 16 |- ( f e. ( NN0 ^m J ) -> ( f supp 0 ) = ( `' f " NN ) )
71	70	eleq1d 2473	. . . . . . . . . . . . . . 15 |- ( f e. ( NN0 ^m J ) -> ( ( f supp 0 ) e. Fin <-> ( `' f " NN ) e. Fin ) )
72	71	rabbiia 3050	. . . . . . . . . . . . . 14 |- { f e. ( NN0 ^m J ) | ( f supp 0 ) e. Fin } = { f e. ( NN0 ^m J ) | ( `' f " NN ) e. Fin }
73		elmapfun 7482	. . . . . . . . . . . . . . . 16 |- ( f e. ( NN0 ^m J ) -> Fun f )
74		vex 3064	. . . . . . . . . . . . . . . . 17 |- f e. _V
75		funisfsupp 7870	. . . . . . . . . . . . . . . . 17 |- ( ( Fun f /\ f e. _V /\ 0 e. NN0 ) -> ( f finSupp 0 <-> ( f supp 0 ) e. Fin ) )
76	74, 62, 75	mp3an23 1320	. . . . . . . . . . . . . . . 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 3050	. . . . . . . . . . . . . 14 |- { f e. ( NN0 ^m J ) | f finSupp 0 } = { f e. ( NN0 ^m J ) | ( f supp 0 ) e. Fin }
79		incom 3634	. . . . . . . . . . . . . . 15 |- ( { f | ( `' f " NN ) e. Fin } i^i ( NN0 ^m J ) ) = ( ( NN0 ^m J ) i^i { f | ( `' f " NN ) e. Fin } )
80		dfrab2 3728	. . . . . . . . . . . . . . 15 |- { f e. ( NN0 ^m J ) | ( `' f " NN ) e. Fin } = ( { f | ( `' f " NN ) e. Fin } i^i ( NN0 ^m J ) )
81	5	ineq2i 3640	. . . . . . . . . . . . . . 15 |- ( ( NN0 ^m J ) i^i R ) = ( ( NN0 ^m J ) i^i { f | ( `' f " NN ) e. Fin } )
82	79, 80, 81	3eqtr4ri 2444	. . . . . . . . . . . . . 14 |- ( ( NN0 ^m J ) i^i R ) = { f e. ( NN0 ^m J ) | ( `' f " NN ) e. Fin }
83	72, 78, 82	3eqtr4ri 2444	. . . . . . . . . . . . 13 |- ( ( NN0 ^m J ) i^i R ) = { f e. ( NN0 ^m J ) | f finSupp 0 }
84		elmapfun 7482	. . . . . . . . . . . . . . 15 |- ( r e. ( ( ~P NN0 i^i Fin ) ^m J ) -> Fun r )
85		vex 3064	. . . . . . . . . . . . . . . . 17 |- r e. _V
86		0ex 4528	. . . . . . . . . . . . . . . . 17 |- (/) e. _V
87		funisfsupp 7870	. . . . . . . . . . . . . . . . 17 |- ( ( Fun r /\ r e. _V /\ (/) e. _V ) -> ( r finSupp (/) <-> ( r supp (/) ) e. Fin ) )
88	85, 86, 87	mp3an23 1320	. . . . . . . . . . . . . . . 16 |- ( Fun r -> ( r finSupp (/) <-> ( r supp (/) ) e. Fin ) )
89	88	bicomd 203	. . . . . . . . . . . . . . 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 3050	. . . . . . . . . . . . 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 28009	. . . . . . . . . . . 12 |- ( T. -> ( f e. ( ( NN0 ^m J ) i^i R ) |-> ( (bits |` NN0 ) o. f ) ) : ( ( NN0 ^m J ) i^i R ) -1-1-onto-> { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin } )
93		inss1 3661	. . . . . . . . . . . . . . . . 17 |- ( ( NN0 ^m J ) i^i R ) C_ ( NN0 ^m J )
94	93	sseli 3440	. . . . . . . . . . . . . . . 16 |- ( f e. ( ( NN0 ^m J ) i^i R ) -> f e. ( NN0 ^m J ) )
95		frn 5722	. . . . . . . . . . . . . . . . 17 |- ( f : J --> NN0 -> ran f C_ NN0 )
96		cores 5328	. . . . . . . . . . . . . . . . 17 |- ( ran f C_ NN0 -> ( (bits |` NN0 ) o. f ) = (bits o. f ) )
97	68, 95, 96	3syl 18	. . . . . . . . . . . . . . . 16 |- ( f e. ( NN0 ^m J ) -> ( (bits |` NN0 ) o. f ) = (bits o. f ) )
98	94, 97	syl 17	. . . . . . . . . . . . . . 15 |- ( f e. ( ( NN0 ^m J ) i^i R ) -> ( (bits |` NN0 ) o. f ) = (bits o. f ) )
99	98	mpteq2ia 4479	. . . . . . . . . . . . . 14 |- ( f e. ( ( NN0 ^m J ) i^i R ) |-> ( (bits |` NN0 ) o. f ) ) = ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) )
100	99	eqcomi 2417	. . . . . . . . . . . . 13 |- ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) = ( f e. ( ( NN0 ^m J ) i^i R ) |-> ( (bits |` NN0 ) o. f ) )
101		f1oeq1 5792	. . . . . . . . . . . . 13 |- ( ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) = ( f e. ( ( NN0 ^m J ) i^i R ) |-> ( (bits |` NN0 ) o. f ) ) -> ( ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) : ( ( NN0 ^m J ) i^i R ) -1-1-onto-> { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin } <-> ( f e. ( ( NN0 ^m J ) i^i R ) |-> ( (bits |` NN0 ) o. f ) ) : ( ( NN0 ^m J ) i^i R ) -1-1-onto-> { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin } ) )
102	100, 101	mp1i 13	. . . . . . . . . . . 12 |- ( T. -> ( ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) : ( ( NN0 ^m J ) i^i R ) -1-1-onto-> { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin } <-> ( f e. ( ( NN0 ^m J ) i^i R ) |-> ( (bits |` NN0 ) o. f ) ) : ( ( NN0 ^m J ) i^i R ) -1-1-onto-> { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin } ) )
103	92, 102	mpbird 234	. . . . . . . . . . 11 |- ( T. -> ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) : ( ( NN0 ^m J ) i^i R ) -1-1-onto-> { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin } )
104	103	trud 1416	. . . . . . . . . 10 |- ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) : ( ( NN0 ^m J ) i^i R ) -1-1-onto-> { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }
105		ssrab2 3526	. . . . . . . . . . . . . . . 16 |- { z e. NN | -. 2 || z } C_ NN
106	42, 105	eqsstri 3474	. . . . . . . . . . . . . . 15 |- J C_ NN
107	1, 57, 106	3pm3.2i 1177	. . . . . . . . . . . . . 14 |- ( NN e. _V /\ NN0 e. _V /\ J C_ NN )
108		eulerpart.t	. . . . . . . . . . . . . . . 16 |- T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }
109		cnveq 4999	. . . . . . . . . . . . . . . . . . 19 |- ( f = o -> `' f = `' o )
110		dfn2 10851	. . . . . . . . . . . . . . . . . . . 20 |- NN = ( NN0 \ { 0 } )
111	110	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( f = o -> NN = ( NN0 \ { 0 } ) )
112	109, 111	imaeq12d 5160	. . . . . . . . . . . . . . . . . 18 |- ( f = o -> ( `' f " NN ) = ( `' o " ( NN0 \ { 0 } ) ) )
113	112	sseq1d 3471	. . . . . . . . . . . . . . . . 17 |- ( f = o -> ( ( `' f " NN ) C_ J <-> ( `' o " ( NN0 \ { 0 } ) ) C_ J ) )
114	113	cbvrabv 3060	. . . . . . . . . . . . . . . 16 |- { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J } = { o e. ( NN0 ^m NN ) | ( `' o " ( NN0 \ { 0 } ) ) C_ J }
115	108, 114	eqtri 2433	. . . . . . . . . . . . . . 15 |- T = { o e. ( NN0 ^m NN ) | ( `' o " ( NN0 \ { 0 } ) ) C_ J }
116		eqid 2404	. . . . . . . . . . . . . . 15 |- ( o e. T |-> ( o |` J ) ) = ( o e. T |-> ( o |` J ) )
117	115, 116	resf1o 28013	. . . . . . . . . . . . . 14 |- ( ( ( NN e. _V /\ NN0 e. _V /\ J C_ NN ) /\ 0 e. NN0 ) -> ( o e. T |-> ( o |` J ) ) : T -1-1-onto-> ( NN0 ^m J ) )
118	107, 62, 117	mp2an 672	. . . . . . . . . . . . 13 |- ( o e. T |-> ( o |` J ) ) : T -1-1-onto-> ( NN0 ^m J )
119		f1of1 5800	. . . . . . . . . . . . 13 |- ( ( o e. T |-> ( o |` J ) ) : T -1-1-onto-> ( NN0 ^m J ) -> ( o e. T |-> ( o |` J ) ) : T -1-1-> ( NN0 ^m J ) )
120	118, 119	ax-mp 5	. . . . . . . . . . . 12 |- ( o e. T |-> ( o |` J ) ) : T -1-1-> ( NN0 ^m J )
121		inss1 3661	. . . . . . . . . . . 12 |- ( T i^i R ) C_ T
122		f1ores 5815	. . . . . . . . . . . 12 |- ( ( ( o e. T |-> ( o |` J ) ) : T -1-1-> ( NN0 ^m J ) /\ ( T i^i R ) C_ T ) -> ( ( o e. T |-> ( o |` J ) ) |` ( T i^i R ) ) : ( T i^i R ) -1-1-onto-> ( ( o e. T |-> ( o |` J ) ) " ( T i^i R ) ) )
123	120, 121, 122	mp2an 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 ) )
124		vex 3064	. . . . . . . . . . . . . . . . . 18 |- o e. _V
125	124	resex 5139	. . . . . . . . . . . . . . . . 17 |- ( o |` J ) e. _V
126	125, 116	fnmpti 5694	. . . . . . . . . . . . . . . 16 |- ( o e. T |-> ( o |` J ) ) Fn T
127		fvelimab 5907	. . . . . . . . . . . . . . . 16 |- ( ( ( o e. T |-> ( o |` J ) ) Fn T /\ ( T i^i R ) C_ T ) -> ( f e. ( ( o e. T |-> ( o |` J ) ) " ( T i^i R ) ) <-> E. m e. ( T i^i R ) ( ( o e. T |-> ( o |` J ) ) ` m ) = f ) )
128	126, 121, 127	mp2an 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 )
129		eqid 2404	. . . . . . . . . . . . . . . . 17 |- ( m e. ( T i^i R ) |-> ( m |` J ) ) = ( m e. ( T i^i R ) |-> ( m |` J ) )
130		vex 3064	. . . . . . . . . . . . . . . . . 18 |- m e. _V
131	130	resex 5139	. . . . . . . . . . . . . . . . 17 |- ( m |` J ) e. _V
132	129, 131	elrnmpti 5076	. . . . . . . . . . . . . . . 16 |- ( f e. ran ( m e. ( T i^i R ) |-> ( m |` J ) ) <-> E. m e. ( T i^i R ) f = ( m |` J ) )
133	47, 48, 49, 42, 43, 50, 51, 5, 108	eulerpartlemt 28829	. . . . . . . . . . . . . . . . 17 |- ( ( NN0 ^m J ) i^i R ) = ran ( m e. ( T i^i R ) |-> ( m |` J ) )
134	133	eleq2i 2482	. . . . . . . . . . . . . . . 16 |- ( f e. ( ( NN0 ^m J ) i^i R ) <-> f e. ran ( m e. ( T i^i R ) |-> ( m |` J ) ) )
135	121	sseli 3440	. . . . . . . . . . . . . . . . . . 19 |- ( m e. ( T i^i R ) -> m e. T )
136	116	fvtresfn 5936	. . . . . . . . . . . . . . . . . . . 20 |- ( m e. T -> ( ( o e. T |-> ( o |` J ) ) ` m ) = ( m |` J ) )
137	136	eqeq1d 2406	. . . . . . . . . . . . . . . . . . 19 |- ( m e. T -> ( ( ( o e. T |-> ( o |` J ) ) ` m ) = f <-> ( m |` J ) = f ) )
138	135, 137	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( m e. ( T i^i R ) -> ( ( ( o e. T |-> ( o |` J ) ) ` m ) = f <-> ( m |` J ) = f ) )
139		eqcom 2413	. . . . . . . . . . . . . . . . . 18 |- ( ( m |` J ) = f <-> f = ( m |` J ) )
140	138, 139	syl6bb 263	. . . . . . . . . . . . . . . . 17 |- ( m e. ( T i^i R ) -> ( ( ( o e. T |-> ( o |` J ) ) ` m ) = f <-> f = ( m |` J ) ) )
141	140	rexbiia 2907	. . . . . . . . . . . . . . . 16 |- ( E. m e. ( T i^i R ) ( ( o e. T |-> ( o |` J ) ) ` m ) = f <-> E. m e. ( T i^i R ) f = ( m |` J ) )
142	132, 134, 141	3bitr4ri 280	. . . . . . . . . . . . . . 15 |- ( E. m e. ( T i^i R ) ( ( o e. T |-> ( o |` J ) ) ` m ) = f <-> f e. ( ( NN0 ^m J ) i^i R ) )
143	128, 142	bitri 251	. . . . . . . . . . . . . 14 |- ( f e. ( ( o e. T |-> ( o |` J ) ) " ( T i^i R ) ) <-> f e. ( ( NN0 ^m J ) i^i R ) )
144	143	eqriv 2400	. . . . . . . . . . . . 13 |- ( ( o e. T |-> ( o |` J ) ) " ( T i^i R ) ) = ( ( NN0 ^m J ) i^i R )
145		f1oeq3 5794	. . . . . . . . . . . . 13 |- ( ( ( o e. T |-> ( o |` J ) ) " ( T i^i R ) ) = ( ( NN0 ^m J ) i^i R ) -> ( ( ( o e. T |-> ( o |` J ) ) |` ( T i^i R ) ) : ( T i^i R ) -1-1-onto-> ( ( o e. T |-> ( o |` J ) ) " ( T i^i R ) ) <-> ( ( o e. T |-> ( o |` J ) ) |` ( T i^i R ) ) : ( T i^i R ) -1-1-onto-> ( ( NN0 ^m J ) i^i R ) ) )
146	144, 145	ax-mp 5	. . . . . . . . . . . 12 |- ( ( ( o e. T |-> ( o |` J ) ) |` ( T i^i R ) ) : ( T i^i R ) -1-1-onto-> ( ( o e. T |-> ( o |` J ) ) " ( T i^i R ) ) <-> ( ( o e. T |-> ( o |` J ) ) |` ( T i^i R ) ) : ( T i^i R ) -1-1-onto-> ( ( NN0 ^m J ) i^i R ) )
147		resmpt 5145	. . . . . . . . . . . . 13 |- ( ( T i^i R ) C_ T -> ( ( o e. T |-> ( o |` J ) ) |` ( T i^i R ) ) = ( o e. ( T i^i R ) |-> ( o |` J ) ) )
148		f1oeq1 5792	. . . . . . . . . . . . 13 |- ( ( ( o e. T |-> ( o |` J ) ) |` ( T i^i R ) ) = ( o e. ( T i^i R ) |-> ( o |` J ) ) -> ( ( ( o e. T |-> ( o |` J ) ) |` ( T i^i R ) ) : ( T i^i R ) -1-1-onto-> ( ( NN0 ^m J ) i^i R ) <-> ( o e. ( T i^i R ) |-> ( o |` J ) ) : ( T i^i R ) -1-1-onto-> ( ( NN0 ^m J ) i^i R ) ) )
149	121, 147, 148	mp2b 10	. . . . . . . . . . . 12 |- ( ( ( o e. T |-> ( o |` J ) ) |` ( T i^i R ) ) : ( T i^i R ) -1-1-onto-> ( ( NN0 ^m J ) i^i R ) <-> ( o e. ( T i^i R ) |-> ( o |` J ) ) : ( T i^i R ) -1-1-onto-> ( ( NN0 ^m J ) i^i R ) )
150	146, 149	bitri 251	. . . . . . . . . . 11 |- ( ( ( o e. T |-> ( o |` J ) ) |` ( T i^i R ) ) : ( T i^i R ) -1-1-onto-> ( ( o e. T |-> ( o |` J ) ) " ( T i^i R ) ) <-> ( o e. ( T i^i R ) |-> ( o |` J ) ) : ( T i^i R ) -1-1-onto-> ( ( NN0 ^m J ) i^i R ) )
151	123, 150	mpbi 210	. . . . . . . . . 10 |- ( o e. ( T i^i R ) |-> ( o |` J ) ) : ( T i^i R ) -1-1-onto-> ( ( NN0 ^m J ) i^i R )
152		f1oco 5823	. . . . . . . . . 10 |- ( ( ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) : ( ( NN0 ^m J ) i^i R ) -1-1-onto-> { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin } /\ ( o e. ( T i^i R ) |-> ( o |` J ) ) : ( T i^i R ) -1-1-onto-> ( ( NN0 ^m J ) i^i R ) ) -> ( ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) o. ( o e. ( T i^i R ) |-> ( o |` J ) ) ) : ( T i^i R ) -1-1-onto-> { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin } )
153	104, 151, 152	mp2an 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 }
154		f1of 5801	. . . . . . . . . . . . . 14 |- ( ( o e. ( T i^i R ) |-> ( o |` J ) ) : ( T i^i R ) -1-1-onto-> ( ( NN0 ^m J ) i^i R ) -> ( o e. ( T i^i R ) |-> ( o |` J ) ) : ( T i^i R ) --> ( ( NN0 ^m J ) i^i R ) )
155		eqid 2404	. . . . . . . . . . . . . . . 16 |- ( o e. ( T i^i R ) |-> ( o |` J ) ) = ( o e. ( T i^i R ) |-> ( o |` J ) )
156	155	fmpt 6032	. . . . . . . . . . . . . . 15 |- ( A. o e. ( T i^i R ) ( o |` J ) e. ( ( NN0 ^m J ) i^i R ) <-> ( o e. ( T i^i R ) |-> ( o |` J ) ) : ( T i^i R ) --> ( ( NN0 ^m J ) i^i R ) )
157	156	biimpri 208	. . . . . . . . . . . . . 14 |- ( ( o e. ( T i^i R ) |-> ( o |` J ) ) : ( T i^i R ) --> ( ( NN0 ^m J ) i^i R ) -> A. o e. ( T i^i R ) ( o |` J ) e. ( ( NN0 ^m J ) i^i R ) )
158	151, 154, 157	mp2b 10	. . . . . . . . . . . . 13 |- A. o e. ( T i^i R ) ( o |` J ) e. ( ( NN0 ^m J ) i^i R )
159	158	a1i 11	. . . . . . . . . . . 12 |- ( T. -> A. o e. ( T i^i R ) ( o |` J ) e. ( ( NN0 ^m J ) i^i R ) )
160		eqidd 2405	. . . . . . . . . . . 12 |- ( T. -> ( o e. ( T i^i R ) |-> ( o |` J ) ) = ( o e. ( T i^i R ) |-> ( o |` J ) ) )
161		eqidd 2405	. . . . . . . . . . . 12 |- ( T. -> ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) = ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) )
162		coeq2 4984	. . . . . . . . . . . 12 |- ( f = ( o |` J ) -> (bits o. f ) = (bits o. ( o |` J ) ) )
163	159, 160, 161, 162	fmptcof 6046	. . . . . . . . . . 11 |- ( T. -> ( ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) o. ( o e. ( T i^i R ) |-> ( o |` J ) ) ) = ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) )
164	163	eqcomd 2412	. . . . . . . . . 10 |- ( T. -> ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) = ( ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) o. ( o e. ( T i^i R ) |-> ( o |` J ) ) ) )
165		eqidd 2405	. . . . . . . . . 10 |- ( T. -> ( T i^i R ) = ( T i^i R ) )
166	50	a1i 11	. . . . . . . . . 10 |- ( T. -> H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin } )
167	164, 165, 166	f1oeq123d 5798	. . . . . . . . 9 |- ( T. -> ( ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) : ( T i^i R ) -1-1-onto-> H <-> ( ( f e. ( ( NN0 ^m J ) i^i R ) |-> (bits o. f ) ) o. ( o e. ( T i^i R ) |-> ( o |` J ) ) ) : ( T i^i R ) -1-1-onto-> { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin } ) )
168	153, 167	mpbiri 235	. . . . . . . 8 |- ( T. -> ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) : ( T i^i R ) -1-1-onto-> H )
169	168	trud 1416	. . . . . . 7 |- ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) : ( T i^i R ) -1-1-onto-> H
170		f1oco 5823	. . . . . . 7 |- ( ( M : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin ) /\ ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) : ( T i^i R ) -1-1-onto-> H ) -> ( M o. ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin ) )
171	52, 169, 170	mp2an 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 )
172		eqidd 2405	. . . . . . . . . . 11 |- ( T. -> ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) = ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) )
173		bitsf 14288	. . . . . . . . . . . . . 14 |- bits : ZZ --> ~P NN0
174		zex 10916	. . . . . . . . . . . . . 14 |- ZZ e. _V
175		fex 6128	. . . . . . . . . . . . . 14 |- ( (bits : ZZ --> ~P NN0 /\ ZZ e. _V ) -> bits e. _V )
176	173, 174, 175	mp2an 672	. . . . . . . . . . . . 13 |- bits e. _V
177	176, 125	coex 6738	. . . . . . . . . . . 12 |- (bits o. ( o |` J ) ) e. _V
178	177	a1i 11	. . . . . . . . . . 11 |- ( ( T. /\ o e. ( T i^i R ) ) -> (bits o. ( o |` J ) ) e. _V )
179	172, 178	fvmpt2d 5945	. . . . . . . . . 10 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) ` o ) = (bits o. ( o |` J ) ) )
180		f1of 5801	. . . . . . . . . . . 12 |- ( ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) : ( T i^i R ) -1-1-onto-> H -> ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) : ( T i^i R ) --> H )
181	168, 180	syl 17	. . . . . . . . . . 11 |- ( T. -> ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) : ( T i^i R ) --> H )
182	181	ffvelrnda 6011	. . . . . . . . . 10 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) ` o ) e. H )
183	179, 182	eqeltrrd 2493	. . . . . . . . 9 |- ( ( T. /\ o e. ( T i^i R ) ) -> (bits o. ( o |` J ) ) e. H )
184		f1ofn 5802	. . . . . . . . . . . 12 |- ( M : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin ) -> M Fn H )
185	52, 184	ax-mp 5	. . . . . . . . . . 11 |- M Fn H
186		dffn5 5896	. . . . . . . . . . 11 |- ( M Fn H <-> M = ( r e. H |-> ( M ` r ) ) )
187	185, 186	mpbi 210	. . . . . . . . . 10 |- M = ( r e. H |-> ( M ` r ) )
188	187	a1i 11	. . . . . . . . 9 |- ( T. -> M = ( r e. H |-> ( M ` r ) ) )
189		fveq2 5851	. . . . . . . . 9 |- ( r = (bits o. ( o |` J ) ) -> ( M ` r ) = ( M ` (bits o. ( o |` J ) ) ) )
190	183, 172, 188, 189	fmptco 6045	. . . . . . . 8 |- ( T. -> ( M o. ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) ) = ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) )
191	190	trud 1416	. . . . . . 7 |- ( M o. ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) ) = ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) )
192		f1oeq1 5792	. . . . . . 7 |- ( ( M o. ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) ) = ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) -> ( ( M o. ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin ) <-> ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin ) ) )
193	191, 192	ax-mp 5	. . . . . 6 |- ( ( M o. ( o e. ( T i^i R ) |-> (bits o. ( o |` J ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin ) <-> ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin ) )
194	171, 193	mpbi 210	. . . . 5 |- ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin )
195		f1oco 5823	. . . . 5 |- ( ( ( a e. ( ~P ( J X. NN0 ) i^i Fin ) |-> ( F " a ) ) : ( ~P ( J X. NN0 ) i^i Fin ) -1-1-onto-> ( ~P NN i^i Fin ) /\ ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin ) ) -> ( ( a e. ( ~P ( J X. NN0 ) i^i Fin ) |-> ( F " a ) ) o. ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P NN i^i Fin ) )
196	46, 194, 195	mp2an 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 )
197		simpr 461	. . . . . . . . 9 |- ( ( T. /\ o e. ( T i^i R ) ) -> o e. ( T i^i R ) )
198		fvex 5861	. . . . . . . . 9 |- ( M ` (bits o. ( o |` J ) ) ) e. _V
199		eqid 2404	. . . . . . . . . 10 |- ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) = ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) )
200	199	fvmpt2 5943	. . . . . . . . 9 |- ( ( o e. ( T i^i R ) /\ ( M ` (bits o. ( o |` J ) ) ) e. _V ) -> ( ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) ` o ) = ( M ` (bits o. ( o |` J ) ) ) )
201	197, 198, 200	sylancl 662	. . . . . . . 8 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) ` o ) = ( M ` (bits o. ( o |` J ) ) ) )
202		f1of 5801	. . . . . . . . . 10 |- ( ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin ) -> ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) : ( T i^i R ) --> ( ~P ( J X. NN0 ) i^i Fin ) )
203	194, 202	mp1i 13	. . . . . . . . 9 |- ( T. -> ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) : ( T i^i R ) --> ( ~P ( J X. NN0 ) i^i Fin ) )
204	203	ffvelrnda 6011	. . . . . . . 8 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) ` o ) e. ( ~P ( J X. NN0 ) i^i Fin ) )
205	201, 204	eqeltrrd 2493	. . . . . . 7 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( M ` (bits o. ( o |` J ) ) ) e. ( ~P ( J X. NN0 ) i^i Fin ) )
206		eqidd 2405	. . . . . . 7 |- ( T. -> ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) = ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) )
207		eqidd 2405	. . . . . . 7 |- ( T. -> ( a e. ( ~P ( J X. NN0 ) i^i Fin ) |-> ( F " a ) ) = ( a e. ( ~P ( J X. NN0 ) i^i Fin ) |-> ( F " a ) ) )
208		imaeq2 5155	. . . . . . 7 |- ( a = ( M ` (bits o. ( o |` J ) ) ) -> ( F " a ) = ( F " ( M ` (bits o. ( o |` J ) ) ) ) )
209	205, 206, 207, 208	fmptco 6045	. . . . . 6 |- ( T. -> ( ( a e. ( ~P ( J X. NN0 ) i^i Fin ) |-> ( F " a ) ) o. ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) ) = ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )
210	209	trud 1416	. . . . 5 |- ( ( a e. ( ~P ( J X. NN0 ) i^i Fin ) |-> ( F " a ) ) o. ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) ) = ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) )
211		f1oeq1 5792	. . . . 5 |- ( ( ( a e. ( ~P ( J X. NN0 ) i^i Fin ) |-> ( F " a ) ) o. ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) ) = ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) -> ( ( ( a e. ( ~P ( J X. NN0 ) i^i Fin ) |-> ( F " a ) ) o. ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P NN i^i Fin ) <-> ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P NN i^i Fin ) ) )
212	210, 211	ax-mp 5	. . . 4 |- ( ( ( a e. ( ~P ( J X. NN0 ) i^i Fin ) |-> ( F " a ) ) o. ( o e. ( T i^i R ) |-> ( M ` (bits o. ( o |` J ) ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P NN i^i Fin ) <-> ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P NN i^i Fin ) )
213	196, 212	mpbi 210	. . 3 |- ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P NN i^i Fin )
214		f1oco 5823	. . 3 |- ( ( ( (𝟭 ` NN ) |` Fin ) : ( ~P NN i^i Fin ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R ) /\ ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P NN i^i Fin ) ) -> ( ( (𝟭 ` NN ) |` Fin ) o. ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R ) )
215	41, 213, 214	mp2an 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 )
216		eulerpart.g	. . . 4 |- G = ( o e. ( T i^i R ) |-> ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )
217	43	mpt2exg 6861	. . . . . . . . . 10 |- ( ( J e. _V /\ NN0 e. _V ) -> F e. _V )
218	55, 57, 217	mp2an 672	. . . . . . . . 9 |- F e. _V
219		imaexg 6723	. . . . . . . . 9 |- ( F e. _V -> ( F " ( M ` (bits o. ( o |` J ) ) ) ) e. _V )
220	218, 219	ax-mp 5	. . . . . . . 8 |- ( F " ( M ` (bits o. ( o |` J ) ) ) ) e. _V
221		eqid 2404	. . . . . . . . 9 |- ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) = ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) )
222	221	fvmpt2 5943	. . . . . . . 8 |- ( ( o e. ( T i^i R ) /\ ( F " ( M ` (bits o. ( o |` J ) ) ) ) e. _V ) -> ( ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) ` o ) = ( F " ( M ` (bits o. ( o |` J ) ) ) ) )
223	197, 220, 222	sylancl 662	. . . . . . 7 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) ` o ) = ( F " ( M ` (bits o. ( o |` J ) ) ) ) )
224		f1of 5801	. . . . . . . . 9 |- ( ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ~P NN i^i Fin ) -> ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) : ( T i^i R ) --> ( ~P NN i^i Fin ) )
225	213, 224	mp1i 13	. . . . . . . 8 |- ( T. -> ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) : ( T i^i R ) --> ( ~P NN i^i Fin ) )
226	225	ffvelrnda 6011	. . . . . . 7 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) ` o ) e. ( ~P NN i^i Fin ) )
227	223, 226	eqeltrrd 2493	. . . . . 6 |- ( ( T. /\ o e. ( T i^i R ) ) -> ( F " ( M ` (bits o. ( o |` J ) ) ) ) e. ( ~P NN i^i Fin ) )
228		eqidd 2405	. . . . . 6 |- ( T. -> ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) = ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )
229		indf1o 28484	. . . . . . . . . . 11 |- ( NN e. _V -> (𝟭 ` NN ) : ~P NN -1-1-onto-> ( { 0 , 1 } ^m NN ) )
230		f1ofn 5802	. . . . . . . . . . 11 |- ( (𝟭 ` NN ) : ~P NN -1-1-onto-> ( { 0 , 1 } ^m NN ) -> (𝟭 ` NN ) Fn ~P NN )
231	1, 229, 230	mp2b 10	. . . . . . . . . 10 |- (𝟭 ` NN ) Fn ~P NN
232		dffn5 5896	. . . . . . . . . 10 |- ( (𝟭 ` NN ) Fn ~P NN <-> (𝟭 ` NN ) = ( b e. ~P NN |-> ( (𝟭 ` NN ) ` b ) ) )
233	231, 232	mpbi 210	. . . . . . . . 9 |- (𝟭 ` NN ) = ( b e. ~P NN |-> ( (𝟭 ` NN ) ` b ) )
234	233	reseq1i 5092	. . . . . . . 8 |- ( (𝟭 ` NN ) |` Fin ) = ( ( b e. ~P NN |-> ( (𝟭 ` NN ) ` b ) ) |` Fin )
235		resmpt3 5146	. . . . . . . 8 |- ( ( b e. ~P NN |-> ( (𝟭 ` NN ) ` b ) ) |` Fin ) = ( b e. ( ~P NN i^i Fin ) |-> ( (𝟭 ` NN ) ` b ) )
236	234, 235	eqtri 2433	. . . . . . 7 |- ( (𝟭 ` NN ) |` Fin ) = ( b e. ( ~P NN i^i Fin ) |-> ( (𝟭 ` NN ) ` b ) )
237	236	a1i 11	. . . . . 6 |- ( T. -> ( (𝟭 ` NN ) |` Fin ) = ( b e. ( ~P NN i^i Fin ) |-> ( (𝟭 ` NN ) ` b ) ) )
238		fveq2 5851	. . . . . 6 |- ( b = ( F " ( M ` (bits o. ( o |` J ) ) ) ) -> ( (𝟭 ` NN ) ` b ) = ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )
239	227, 228, 237, 238	fmptco 6045	. . . . 5 |- ( T. -> ( ( (𝟭 ` NN ) |` Fin ) o. ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) ) = ( o e. ( T i^i R ) |-> ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) ) )
240	239	trud 1416	. . . 4 |- ( ( (𝟭 ` NN ) |` Fin ) o. ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) ) = ( o e. ( T i^i R ) |-> ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )
241	216, 240	eqtr4i 2436	. . 3 |- G = ( ( (𝟭 ` NN ) |` Fin ) o. ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )
242		f1oeq1 5792	. . 3 |- ( G = ( ( (𝟭 ` NN ) |` Fin ) o. ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) ) -> ( G : ( T i^i R ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R ) <-> ( ( (𝟭 ` NN ) |` Fin ) o. ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R ) ) )
243	241, 242	ax-mp 5	. 2 |- ( G : ( T i^i R ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R ) <-> ( ( (𝟭 ` NN ) |` Fin ) o. ( o e. ( T i^i R ) |-> ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) ) : ( T i^i R ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R ) )
244	215, 243	mpbir 211	1 |- G : ( T i^i R ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R )

Syntax hints:   -. wn 3   <-> wb 186   /\ wa 369   /\ w3a 976   = wceq 1407   T. wtru 1408   e. wcel 1844   {cab 2389   A.wral 2756   E.wrex 2757   {crab 2760   _Vcvv 3061   \ cdif 3413   u. cun 3414   i^i cin 3415   C_ wss 3416   (/)c0 3740   ~Pcpw 3957   {csn 3974   {cpr 3976   class class class wbr 4397   {copab 4454   |-> cmpt 4455   X. cxp 4823   `'ccnv 4824   ran crn 4826   |` cres 4827   "cima 4828   o. ccom 4829   Fun wfun 5565   Fn wfn 5566   -->wf 5567   -1-1->wf1 5568   -1-1-onto->wf1o 5570   ` cfv 5571  (class class class)co 6280   |-> cmpt2 6282   supp csupp 6904   ^m cmap 7459   Fincfn 7556   finSupp cfsupp 7865   0cc0 9524   1c1 9525   x. cmul 9529   <_ cle 9661   NNcn 10578   2c2 10628   NN0cn0 10838   ZZcz 10907   ^cexp 12212   sum_csu 13659   || cdvds 14197  bitscbits 14280  𝟭cind 28471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-8 1846  ax-9 1848  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382  ax-rep 4509  ax-sep 4519  ax-nul 4527  ax-pow 4574  ax-pr 4632  ax-un 6576  ax-inf2 8093  ax-ac2 8877  ax-cnex 9580  ax-resscn 9581  ax-1cn 9582  ax-icn 9583  ax-addcl 9584  ax-addrcl 9585  ax-mulcl 9586  ax-mulrcl 9587  ax-mulcom 9588  ax-addass 9589  ax-mulass 9590  ax-distr 9591  ax-i2m1 9592  ax-1ne0 9593  ax-1rid 9594  ax-rnegex 9595  ax-rrecex 9596  ax-cnre 9597  ax-pre-lttri 9598  ax-pre-lttrn 9599  ax-pre-ltadd 9600  ax-pre-mulgt0 9601  ax-pre-sup 9602

This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-3or 977  df-3an 978  df-tru 1410  df-fal 1413  df-ex 1636  df-nf 1640  df-sb 1766  df-eu 2244  df-mo 2245  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-ne 2602  df-nel 2603  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3063  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3741  df-if 3888  df-pw 3959  df-sn 3975  df-pr 3977  df-tp 3979  df-op 3981  df-uni 4194  df-int 4230  df-iun 4275  df-disj 4369  df-br 4398  df-opab 4456  df-mpt 4457  df-tr 4492  df-eprel 4736  df-id 4740  df-po 4746  df-so 4747  df-fr 4784  df-se 4785  df-we 4786  df-xp 4831  df-rel 4832  df-cnv 4833  df-co 4834  df-dm 4835  df-rn 4836  df-res 4837  df-ima 4838  df-pred 5369  df-ord 5415  df-on 5416  df-lim 5417  df-suc 5418  df-iota 5535  df-fun 5573  df-fn 5574  df-f 5575  df-f1 5576  df-fo 5577  df-f1o 5578  df-fv 5579  df-isom 5580  df-riota 6242  df-ov 6283  df-oprab 6284  df-mpt2 6285  df-om 6686  df-1st 6786  df-2nd 6787  df-supp 6905  df-wrecs 7015  df-recs 7077  df-rdg 7115  df-1o 7169  df-2o 7170  df-oadd 7173  df-er 7350  df-map 7461  df-pm 7462  df-en 7557  df-dom 7558  df-sdom 7559  df-fin 7560  df-fsupp 7866  df-sup 7937  df-oi 7971  df-card 8354  df-acn 8357  df-ac 8531  df-cda 8582  df-pnf 9662  df-mnf 9663  df-xr 9664  df-ltxr 9665  df-le 9666  df-sub 9845  df-neg 9846  df-div 10250  df-nn 10579  df-2 10637  df-3 10638  df-n0 10839  df-z 10908  df-uz 11130  df-rp 11268  df-fz 11729  df-fzo 11857  df-fl 11968  df-mod 12037  df-seq 12154  df-exp 12213  df-hash 12455  df-cj 13083  df-re 13084  df-im 13085  df-sqrt 13219  df-abs 13220  df-clim 13462  df-sum 13660  df-dvds 14198  df-bits 14283  df-ind 28472

This theorem is referenced by:  eulerpartlemgf  28837  eulerpartlemgs2  28838  eulerpartlemn  28839