Theorem eulerpartgbij

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

	Ref	Expression
Hypotheses	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 ) |-> ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) )
Assertion	eulerpartgbij	|- G : ( T i^i R ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R )

Proof

Step	Hyp	Ref	Expression
1		eulerpart.p	|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }
2		eulerpart.o	|- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }
3		eulerpart.d	|- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }
4		eulerpart.j	|- J = { z e. NN | -. 2 || z }
5		eulerpart.f	|- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )
6		eulerpart.h	|- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }
7		eulerpart.m	|- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )
8		eulerpart.r	|- R = { f | ( `' f " NN ) e. Fin }
9		eulerpart.t	|- T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }
10		eulerpart.g	|- G = ( o e. ( T i^i R ) |-> ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) )
11		nnex	|- NN e. _V
12		indf1ofs	|- ( NN e. _V -> ( ( _Ind ` NN ) |` Fin ) : ( ~P NN i^i Fin ) -1-1-onto-> { f e. ( { 0 , 1 } ^m NN ) | ( `' f " { 1 } ) e. Fin } )
13	11 12	ax-mp	|- ( ( _Ind ` NN ) |` Fin ) : ( ~P NN i^i Fin ) -1-1-onto-> { f e. ( { 0 , 1 } ^m NN ) | ( `' f " { 1 } ) e. Fin }
14		incom	|- ( ( { 0 , 1 } ^m NN ) i^i { f | ( `' f " NN ) e. Fin } ) = ( { f | ( `' f " NN ) e. Fin } i^i ( { 0 , 1 } ^m NN ) )
15	8	ineq2i	|- ( ( { 0 , 1 } ^m NN ) i^i R ) = ( ( { 0 , 1 } ^m NN ) i^i { f | ( `' f " NN ) e. Fin } )
16		dfrab2	|- { f e. ( { 0 , 1 } ^m NN ) | ( `' f " NN ) e. Fin } = ( { f | ( `' f " NN ) e. Fin } i^i ( { 0 , 1 } ^m NN ) )
17	14 15 16	3eqtr4i	|- ( ( { 0 , 1 } ^m NN ) i^i R ) = { f e. ( { 0 , 1 } ^m NN ) | ( `' f " NN ) e. Fin }
18		elmapfun	|- ( f e. ( { 0 , 1 } ^m NN ) -> Fun f )
19		elmapi	|- ( f e. ( { 0 , 1 } ^m NN ) -> f : NN --> { 0 , 1 } )
20	19	frnd	|- ( f e. ( { 0 , 1 } ^m NN ) -> ran f C_ { 0 , 1 } )
21		fimacnvinrn2	|- ( ( Fun f /\ ran f C_ { 0 , 1 } ) -> ( `' f " NN ) = ( `' f " ( NN i^i { 0 , 1 } ) ) )
22		df-pr	|- { 0 , 1 } = ( { 0 } u. { 1 } )
23	22	ineq2i	|- ( NN i^i { 0 , 1 } ) = ( NN i^i ( { 0 } u. { 1 } ) )
24		indi	|- ( NN i^i ( { 0 } u. { 1 } ) ) = ( ( NN i^i { 0 } ) u. ( NN i^i { 1 } ) )
25		0nnn	|- -. 0 e. NN
26		disjsn	|- ( ( NN i^i { 0 } ) = (/) <-> -. 0 e. NN )
27	25 26	mpbir	|- ( NN i^i { 0 } ) = (/)
28		1nn	|- 1 e. NN
29		1ex	|- 1 e. _V
30	29	snss	|- ( 1 e. NN <-> { 1 } C_ NN )
31	28 30	mpbi	|- { 1 } C_ NN
32		dfss	|- ( { 1 } C_ NN <-> { 1 } = ( { 1 } i^i NN ) )
33	31 32	mpbi	|- { 1 } = ( { 1 } i^i NN )
34		incom	|- ( { 1 } i^i NN ) = ( NN i^i { 1 } )
35	33 34	eqtr2i	|- ( NN i^i { 1 } ) = { 1 }
36	27 35	uneq12i	|- ( ( NN i^i { 0 } ) u. ( NN i^i { 1 } ) ) = ( (/) u. { 1 } )
37	23 24 36	3eqtri	|- ( NN i^i { 0 , 1 } ) = ( (/) u. { 1 } )
38		uncom	|- ( (/) u. { 1 } ) = ( { 1 } u. (/) )
39		un0	|- ( { 1 } u. (/) ) = { 1 }
40	37 38 39	3eqtri	|- ( NN i^i { 0 , 1 } ) = { 1 }
41	40	imaeq2i	|- ( `' f " ( NN i^i { 0 , 1 } ) ) = ( `' f " { 1 } )
42	21 41	eqtrdi	|- ( ( Fun f /\ ran f C_ { 0 , 1 } ) -> ( `' f " NN ) = ( `' f " { 1 } ) )
43	18 20 42	syl2anc	|- ( f e. ( { 0 , 1 } ^m NN ) -> ( `' f " NN ) = ( `' f " { 1 } ) )
44	43	eleq1d	|- ( f e. ( { 0 , 1 } ^m NN ) -> ( ( `' f " NN ) e. Fin <-> ( `' f " { 1 } ) e. Fin ) )
45	44	rabbiia	|- { f e. ( { 0 , 1 } ^m NN ) | ( `' f " NN ) e. Fin } = { f e. ( { 0 , 1 } ^m NN ) | ( `' f " { 1 } ) e. Fin }
46	17 45	eqtr2i	|- { f e. ( { 0 , 1 } ^m NN ) | ( `' f " { 1 } ) e. Fin } = ( ( { 0 , 1 } ^m NN ) i^i R )
47		f1oeq3	|- ( { f e. ( { 0 , 1 } ^m NN ) | ( `' f " { 1 } ) e. Fin } = ( ( { 0 , 1 } ^m NN ) i^i R ) -> ( ( ( _Ind ` NN ) |` Fin ) : ( ~P NN i^i Fin ) -1-1-onto-> { f e. ( { 0 , 1 } ^m NN ) | ( `' f " { 1 } ) e. Fin } <-> ( ( _Ind ` NN ) |` Fin ) : ( ~P NN i^i Fin ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R ) ) )
48	46 47	ax-mp	|- ( ( ( _Ind ` NN ) |` Fin ) : ( ~P NN i^i Fin ) -1-1-onto-> { f e. ( { 0 , 1 } ^m NN ) | ( `' f " { 1 } ) e. Fin } <-> ( ( _Ind ` NN ) |` Fin ) : ( ~P NN i^i Fin ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R ) )
49	13 48	mpbi	|- ( ( _Ind ` NN ) |` Fin ) : ( ~P NN i^i Fin ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R )
50	4 5	oddpwdc	|- F : ( J X. NN0 ) -1-1-onto-> NN
51		f1opwfi	|- ( 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 ) )
52	50 51	ax-mp	|- ( 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 )
53	1 2 3 4 5 6 7	eulerpartlem1	|- M : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin )
54		bitsf1o	|- ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin )
55	54	a1i	|- ( T. -> ( bits |` NN0 ) : NN0 -1-1-onto-> ( ~P NN0 i^i Fin ) )
56	4 11	rabex2	|- J e. _V
57	56	a1i	|- ( T. -> J e. _V )
58		nn0ex	|- NN0 e. _V
59	58	a1i	|- ( T. -> NN0 e. _V )
60	58	pwex	|- ~P NN0 e. _V
61	60	inex1	|- ( ~P NN0 i^i Fin ) e. _V
62	61	a1i	|- ( T. -> ( ~P NN0 i^i Fin ) e. _V )
63		0nn0	|- 0 e. NN0
64	63	a1i	|- ( T. -> 0 e. NN0 )
65		fvres	|- ( 0 e. NN0 -> ( ( bits |` NN0 ) ` 0 ) = ( bits ` 0 ) )
66	63 65	ax-mp	|- ( ( bits |` NN0 ) ` 0 ) = ( bits ` 0 )
67		0bits	|- ( bits ` 0 ) = (/)
68	66 67	eqtr2i	|- (/) = ( ( bits |` NN0 ) ` 0 )
69		elmapi	|- ( f e. ( NN0 ^m J ) -> f : J --> NN0 )
70		frnnn0supp	|- ( ( J e. _V /\ f : J --> NN0 ) -> ( f supp 0 ) = ( `' f " NN ) )
71	56 69 70	sylancr	|- ( f e. ( NN0 ^m J ) -> ( f supp 0 ) = ( `' f " NN ) )
72	71	eleq1d	|- ( f e. ( NN0 ^m J ) -> ( ( f supp 0 ) e. Fin <-> ( `' f " NN ) e. Fin ) )
73	72	rabbiia	|- { f e. ( NN0 ^m J ) | ( f supp 0 ) e. Fin } = { f e. ( NN0 ^m J ) | ( `' f " NN ) e. Fin }
74		elmapfun	|- ( f e. ( NN0 ^m J ) -> Fun f )
75		vex	|- f e. _V
76		funisfsupp	|- ( ( Fun f /\ f e. _V /\ 0 e. NN0 ) -> ( f finSupp 0 <-> ( f supp 0 ) e. Fin ) )
77	75 63 76	mp3an23	|- ( Fun f -> ( f finSupp 0 <-> ( f supp 0 ) e. Fin ) )
78	74 77	syl	|- ( f e. ( NN0 ^m J ) -> ( f finSupp 0 <-> ( f supp 0 ) e. Fin ) )
79	78	rabbiia	|- { f e. ( NN0 ^m J ) | f finSupp 0 } = { f e. ( NN0 ^m J ) | ( f supp 0 ) e. Fin }
80		incom	|- ( { f | ( `' f " NN ) e. Fin } i^i ( NN0 ^m J ) ) = ( ( NN0 ^m J ) i^i { f | ( `' f " NN ) e. Fin } )
81		dfrab2	|- { f e. ( NN0 ^m J ) | ( `' f " NN ) e. Fin } = ( { f | ( `' f " NN ) e. Fin } i^i ( NN0 ^m J ) )
82	8	ineq2i	|- ( ( NN0 ^m J ) i^i R ) = ( ( NN0 ^m J ) i^i { f | ( `' f " NN ) e. Fin } )
83	80 81 82	3eqtr4ri	|- ( ( NN0 ^m J ) i^i R ) = { f e. ( NN0 ^m J ) | ( `' f " NN ) e. Fin }
84	73 79 83	3eqtr4ri	|- ( ( NN0 ^m J ) i^i R ) = { f e. ( NN0 ^m J ) | f finSupp 0 }
85		elmapfun	|- ( r e. ( ( ~P NN0 i^i Fin ) ^m J ) -> Fun r )
86		vex	|- r e. _V
87		0ex	|- (/) e. _V
88		funisfsupp	|- ( ( Fun r /\ r e. _V /\ (/) e. _V ) -> ( r finSupp (/) <-> ( r supp (/) ) e. Fin ) )
89	86 87 88	mp3an23	|- ( Fun r -> ( r finSupp (/) <-> ( r supp (/) ) e. Fin ) )
90	89	bicomd	|- ( Fun r -> ( ( r supp (/) ) e. Fin <-> r finSupp (/) ) )
91	85 90	syl	|- ( r e. ( ( ~P NN0 i^i Fin ) ^m J ) -> ( ( r supp (/) ) e. Fin <-> r finSupp (/) ) )
92	91	rabbiia	|- { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin } = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | r finSupp (/) }
93	55 57 59 62 64 68 84 92	fcobijfs	|- ( 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 } )
94		elinel1	|- ( f e. ( ( NN0 ^m J ) i^i R ) -> f e. ( NN0 ^m J ) )
95		frn	|- ( f : J --> NN0 -> ran f C_ NN0 )
96		cores	|- ( ran f C_ NN0 -> ( ( bits |` NN0 ) o. f ) = ( bits o. f ) )
97	69 95 96	3syl	|- ( f e. ( NN0 ^m J ) -> ( ( bits |` NN0 ) o. f ) = ( bits o. f ) )
98	94 97	syl	|- ( f e. ( ( NN0 ^m J ) i^i R ) -> ( ( bits |` NN0 ) o. f ) = ( bits o. f ) )
99	98	mpteq2ia	|- ( 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	|- ( 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	|- ( ( 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	|- ( 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	93 102	mpbird	|- ( 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	mptru	|- ( 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	|- { z e. NN | -. 2 || z } C_ NN
106	4 105	eqsstri	|- J C_ NN
107	11 58 106	3pm3.2i	|- ( NN e. _V /\ NN0 e. _V /\ J C_ NN )
108		cnveq	|- ( f = o -> `' f = `' o )
109		dfn2	|- NN = ( NN0 \ { 0 } )
110	109	a1i	|- ( f = o -> NN = ( NN0 \ { 0 } ) )
111	108 110	imaeq12d	|- ( f = o -> ( `' f " NN ) = ( `' o " ( NN0 \ { 0 } ) ) )
112	111	sseq1d	|- ( f = o -> ( ( `' f " NN ) C_ J <-> ( `' o " ( NN0 \ { 0 } ) ) C_ J ) )
113	112	cbvrabv	|- { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J } = { o e. ( NN0 ^m NN ) | ( `' o " ( NN0 \ { 0 } ) ) C_ J }
114	9 113	eqtri	|- T = { o e. ( NN0 ^m NN ) | ( `' o " ( NN0 \ { 0 } ) ) C_ J }
115		eqid	|- ( o e. T |-> ( o |` J ) ) = ( o e. T |-> ( o |` J ) )
116	114 115	resf1o	|- ( ( ( 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	107 63 116	mp2an	|- ( o e. T |-> ( o |` J ) ) : T -1-1-onto-> ( NN0 ^m J )
118		f1of1	|- ( ( 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	|- ( o e. T |-> ( o |` J ) ) : T -1-1-> ( NN0 ^m J )
120		inss1	|- ( T i^i R ) C_ T
121		f1ores	|- ( ( ( 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	|- ( ( 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	|- o e. _V
124	123	resex	|- ( o |` J ) e. _V
125	124 115	fnmpti	|- ( o e. T |-> ( o |` J ) ) Fn T
126		fvelimab	|- ( ( ( 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	|- ( 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	|- ( m e. ( T i^i R ) |-> ( m |` J ) ) = ( m e. ( T i^i R ) |-> ( m |` J ) )
129		vex	|- m e. _V
130	129	resex	|- ( m |` J ) e. _V
131	128 130	elrnmpti	|- ( f e. ran ( m e. ( T i^i R ) |-> ( m |` J ) ) <-> E. m e. ( T i^i R ) f = ( m |` J ) )
132	1 2 3 4 5 6 7 8 9	eulerpartlemt	|- ( ( NN0 ^m J ) i^i R ) = ran ( m e. ( T i^i R ) |-> ( m |` J ) )
133	132	eleq2i	|- ( f e. ( ( NN0 ^m J ) i^i R ) <-> f e. ran ( m e. ( T i^i R ) |-> ( m |` J ) ) )
134		elinel1	|- ( m e. ( T i^i R ) -> m e. T )
135	115	fvtresfn	|- ( m e. T -> ( ( o e. T |-> ( o |` J ) ) ` m ) = ( m |` J ) )
136	135	eqeq1d	|- ( m e. T -> ( ( ( o e. T |-> ( o |` J ) ) ` m ) = f <-> ( m |` J ) = f ) )
137	134 136	syl	|- ( m e. ( T i^i R ) -> ( ( ( o e. T |-> ( o |` J ) ) ` m ) = f <-> ( m |` J ) = f ) )
138		eqcom	|- ( ( m |` J ) = f <-> f = ( m |` J ) )
139	137 138	bitrdi	|- ( m e. ( T i^i R ) -> ( ( ( o e. T |-> ( o |` J ) ) ` m ) = f <-> f = ( m |` J ) ) )
140	139	rexbiia	|- ( 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	|- ( 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	|- ( f e. ( ( o e. T |-> ( o |` J ) ) " ( T i^i R ) ) <-> f e. ( ( NN0 ^m J ) i^i R ) )
143	142	eqriv	|- ( ( o e. T |-> ( o |` J ) ) " ( T i^i R ) ) = ( ( NN0 ^m J ) i^i R )
144		f1oeq3	|- ( ( ( 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	|- ( ( ( 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	|- ( ( 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	|- ( ( ( 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	|- ( ( ( 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	|- ( ( ( 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	|- ( o e. ( T i^i R ) |-> ( o |` J ) ) : ( T i^i R ) -1-1-onto-> ( ( NN0 ^m J ) i^i R )
151		f1oco	|- ( ( ( 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	104 150 151	mp2an	|- ( ( 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	|- ( ( 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	|- ( o e. ( T i^i R ) |-> ( o |` J ) ) = ( o e. ( T i^i R ) |-> ( o |` J ) )
155	154	fmpt	|- ( 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	|- ( ( 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	|- A. o e. ( T i^i R ) ( o |` J ) e. ( ( NN0 ^m J ) i^i R )
158	157	a1i	|- ( T. -> A. o e. ( T i^i R ) ( o |` J ) e. ( ( NN0 ^m J ) i^i R ) )
159		eqidd	|- ( T. -> ( o e. ( T i^i R ) |-> ( o |` J ) ) = ( o e. ( T i^i R ) |-> ( o |` J ) ) )
160		eqidd	|- ( 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	|- ( f = ( o |` J ) -> ( bits o. f ) = ( bits o. ( o |` J ) ) )
162	158 159 160 161	fmptcof	|- ( 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	|- ( 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	|- ( T. -> ( T i^i R ) = ( T i^i R ) )
165	6	a1i	|- ( T. -> H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin } )
166	163 164 165	f1oeq123d	|- ( 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	|- ( T. -> ( o e. ( T i^i R ) |-> ( bits o. ( o |` J ) ) ) : ( T i^i R ) -1-1-onto-> H )
168	167	mptru	|- ( o e. ( T i^i R ) |-> ( bits o. ( o |` J ) ) ) : ( T i^i R ) -1-1-onto-> H
169		f1oco	|- ( ( 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	53 168 169	mp2an	|- ( 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	|- ( T. -> ( o e. ( T i^i R ) |-> ( bits o. ( o |` J ) ) ) = ( o e. ( T i^i R ) |-> ( bits o. ( o |` J ) ) ) )
172		bitsf	|- bits : ZZ --> ~P NN0
173		zex	|- ZZ e. _V
174		fex	|- ( ( bits : ZZ --> ~P NN0 /\ ZZ e. _V ) -> bits e. _V )
175	172 173 174	mp2an	|- bits e. _V
176	175 124	coex	|- ( bits o. ( o |` J ) ) e. _V
177	176	a1i	|- ( ( T. /\ o e. ( T i^i R ) ) -> ( bits o. ( o |` J ) ) e. _V )
178	171 177	fvmpt2d	|- ( ( T. /\ o e. ( T i^i R ) ) -> ( ( o e. ( T i^i R ) |-> ( bits o. ( o |` J ) ) ) ` o ) = ( bits o. ( o |` J ) ) )
179		f1of	|- ( ( 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	|- ( T. -> ( o e. ( T i^i R ) |-> ( bits o. ( o |` J ) ) ) : ( T i^i R ) --> H )
181	180	ffvelrnda	|- ( ( T. /\ o e. ( T i^i R ) ) -> ( ( o e. ( T i^i R ) |-> ( bits o. ( o |` J ) ) ) ` o ) e. H )
182	178 181	eqeltrrd	|- ( ( T. /\ o e. ( T i^i R ) ) -> ( bits o. ( o |` J ) ) e. H )
183		f1ofn	|- ( M : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin ) -> M Fn H )
184	53 183	ax-mp	|- M Fn H
185		dffn5	|- ( M Fn H <-> M = ( r e. H |-> ( M ` r ) ) )
186	184 185	mpbi	|- M = ( r e. H |-> ( M ` r ) )
187	186	a1i	|- ( T. -> M = ( r e. H |-> ( M ` r ) ) )
188		fveq2	|- ( r = ( bits o. ( o |` J ) ) -> ( M ` r ) = ( M ` ( bits o. ( o |` J ) ) ) )
189	182 171 187 188	fmptco	|- ( 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	mptru	|- ( 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	|- ( ( 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	|- ( ( 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	|- ( 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	|- ( ( ( 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	52 193 194	mp2an	|- ( ( 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	|- ( ( T. /\ o e. ( T i^i R ) ) -> o e. ( T i^i R ) )
197		fvex	|- ( M ` ( bits o. ( o |` J ) ) ) e. _V
198		eqid	|- ( 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	|- ( ( 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	|- ( ( 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	|- ( ( 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	|- ( 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	|- ( ( 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	|- ( ( T. /\ o e. ( T i^i R ) ) -> ( M ` ( bits o. ( o |` J ) ) ) e. ( ~P ( J X. NN0 ) i^i Fin ) )
205		eqidd	|- ( 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	|- ( 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	|- ( a = ( M ` ( bits o. ( o |` J ) ) ) -> ( F " a ) = ( F " ( M ` ( bits o. ( o |` J ) ) ) ) )
208	204 205 206 207	fmptco	|- ( 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	mptru	|- ( ( 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	|- ( ( ( 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	|- ( ( ( 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	|- ( 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	|- ( ( ( ( _Ind ` 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 ) ) -> ( ( ( _Ind ` 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	49 212 213	mp2an	|- ( ( ( _Ind ` 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	5	mpoexg	|- ( ( J e. _V /\ NN0 e. _V ) -> F e. _V )
216	56 58 215	mp2an	|- F e. _V
217		imaexg	|- ( F e. _V -> ( F " ( M ` ( bits o. ( o |` J ) ) ) ) e. _V )
218	216 217	ax-mp	|- ( F " ( M ` ( bits o. ( o |` J ) ) ) ) e. _V
219		eqid	|- ( o e. ( T i^i R ) |-> ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) = ( o e. ( T i^i R ) |-> ( F " ( M ` ( bits o. ( o |` J ) ) ) ) )
220	219	fvmpt2	|- ( ( 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 ) ) ) ) )
221	196 218 220	sylancl	|- ( ( 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 ) ) ) ) )
222		f1of	|- ( ( 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 ) )
223	212 222	mp1i	|- ( T. -> ( o e. ( T i^i R ) |-> ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) : ( T i^i R ) --> ( ~P NN i^i Fin ) )
224	223	ffvelrnda	|- ( ( 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 ) )
225	221 224	eqeltrrd	|- ( ( T. /\ o e. ( T i^i R ) ) -> ( F " ( M ` ( bits o. ( o |` J ) ) ) ) e. ( ~P NN i^i Fin ) )
226		eqidd	|- ( 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 ) ) ) ) ) )
227		indf1o	|- ( NN e. _V -> ( _Ind ` NN ) : ~P NN -1-1-onto-> ( { 0 , 1 } ^m NN ) )
228		f1ofn	|- ( ( _Ind ` NN ) : ~P NN -1-1-onto-> ( { 0 , 1 } ^m NN ) -> ( _Ind ` NN ) Fn ~P NN )
229	11 227 228	mp2b	|- ( _Ind ` NN ) Fn ~P NN
230		dffn5	|- ( ( _Ind ` NN ) Fn ~P NN <-> ( _Ind ` NN ) = ( b e. ~P NN |-> ( ( _Ind ` NN ) ` b ) ) )
231	229 230	mpbi	|- ( _Ind ` NN ) = ( b e. ~P NN |-> ( ( _Ind ` NN ) ` b ) )
232	231	reseq1i	|- ( ( _Ind ` NN ) |` Fin ) = ( ( b e. ~P NN |-> ( ( _Ind ` NN ) ` b ) ) |` Fin )
233		resmpt3	|- ( ( b e. ~P NN |-> ( ( _Ind ` NN ) ` b ) ) |` Fin ) = ( b e. ( ~P NN i^i Fin ) |-> ( ( _Ind ` NN ) ` b ) )
234	232 233	eqtri	|- ( ( _Ind ` NN ) |` Fin ) = ( b e. ( ~P NN i^i Fin ) |-> ( ( _Ind ` NN ) ` b ) )
235	234	a1i	|- ( T. -> ( ( _Ind ` NN ) |` Fin ) = ( b e. ( ~P NN i^i Fin ) |-> ( ( _Ind ` NN ) ` b ) ) )
236		fveq2	|- ( b = ( F " ( M ` ( bits o. ( o |` J ) ) ) ) -> ( ( _Ind ` NN ) ` b ) = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) )
237	225 226 235 236	fmptco	|- ( T. -> ( ( ( _Ind ` NN ) |` Fin ) o. ( o e. ( T i^i R ) |-> ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) ) = ( o e. ( T i^i R ) |-> ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) ) )
238	237	mptru	|- ( ( ( _Ind ` NN ) |` Fin ) o. ( o e. ( T i^i R ) |-> ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) ) = ( o e. ( T i^i R ) |-> ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) )
239	10 238	eqtr4i	|- G = ( ( ( _Ind ` NN ) |` Fin ) o. ( o e. ( T i^i R ) |-> ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) )
240		f1oeq1	|- ( G = ( ( ( _Ind ` 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 ) <-> ( ( ( _Ind ` 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 ) ) )
241	239 240	ax-mp	|- ( G : ( T i^i R ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R ) <-> ( ( ( _Ind ` 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	214 241	mpbir	|- G : ( T i^i R ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R )