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		fcdmnn0supp	|- ( ( 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	94 69 95 96	4syl	|- ( f e. ( ( NN0 ^m J ) i^i R ) -> ( ( bits |` NN0 ) o. f ) = ( bits o. f ) )
98	97	mpteq2ia	|- ( 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	|- ( 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	|- ( ( 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	|- ( 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	93 101	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 } )
103	102	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 }
104		ssrab2	|- { z e. NN | -. 2 || z } C_ NN
105	4 104	eqsstri	|- J C_ NN
106	11 58 105	3pm3.2i	|- ( NN e. _V /\ NN0 e. _V /\ J C_ NN )
107		cnveq	|- ( f = o -> `' f = `' o )
108		dfn2	|- NN = ( NN0 \ { 0 } )
109	108	a1i	|- ( f = o -> NN = ( NN0 \ { 0 } ) )
110	107 109	imaeq12d	|- ( f = o -> ( `' f " NN ) = ( `' o " ( NN0 \ { 0 } ) ) )
111	110	sseq1d	|- ( f = o -> ( ( `' f " NN ) C_ J <-> ( `' o " ( NN0 \ { 0 } ) ) C_ J ) )
112	111	cbvrabv	|- { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J } = { o e. ( NN0 ^m NN ) | ( `' o " ( NN0 \ { 0 } ) ) C_ J }
113	9 112	eqtri	|- T = { o e. ( NN0 ^m NN ) | ( `' o " ( NN0 \ { 0 } ) ) C_ J }
114		eqid	|- ( o e. T |-> ( o |` J ) ) = ( o e. T |-> ( o |` J ) )
115	113 114	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 ) )
116	106 63 115	mp2an	|- ( o e. T |-> ( o |` J ) ) : T -1-1-onto-> ( NN0 ^m J )
117		f1of1	|- ( ( o e. T |-> ( o |` J ) ) : T -1-1-onto-> ( NN0 ^m J ) -> ( o e. T |-> ( o |` J ) ) : T -1-1-> ( NN0 ^m J ) )
118	116 117	ax-mp	|- ( o e. T |-> ( o |` J ) ) : T -1-1-> ( NN0 ^m J )
119		inss1	|- ( T i^i R ) C_ T
120		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 ) ) )
121	118 119 120	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 ) )
122		vex	|- o e. _V
123	122	resex	|- ( o |` J ) e. _V
124	123 114	fnmpti	|- ( o e. T |-> ( o |` J ) ) Fn T
125		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 ) )
126	124 119 125	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 )
127		eqid	|- ( m e. ( T i^i R ) |-> ( m |` J ) ) = ( m e. ( T i^i R ) |-> ( m |` J ) )
128		vex	|- m e. _V
129	128	resex	|- ( m |` J ) e. _V
130	127 129	elrnmpti	|- ( f e. ran ( m e. ( T i^i R ) |-> ( m |` J ) ) <-> E. m e. ( T i^i R ) f = ( m |` J ) )
131	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 ) )
132	131	eleq2i	|- ( f e. ( ( NN0 ^m J ) i^i R ) <-> f e. ran ( m e. ( T i^i R ) |-> ( m |` J ) ) )
133		elinel1	|- ( m e. ( T i^i R ) -> m e. T )
134	114	fvtresfn	|- ( m e. T -> ( ( o e. T |-> ( o |` J ) ) ` m ) = ( m |` J ) )
135	134	eqeq1d	|- ( m e. T -> ( ( ( o e. T |-> ( o |` J ) ) ` m ) = f <-> ( m |` J ) = f ) )
136	133 135	syl	|- ( m e. ( T i^i R ) -> ( ( ( o e. T |-> ( o |` J ) ) ` m ) = f <-> ( m |` J ) = f ) )
137		eqcom	|- ( ( m |` J ) = f <-> f = ( m |` J ) )
138	136 137	bitrdi	|- ( m e. ( T i^i R ) -> ( ( ( o e. T |-> ( o |` J ) ) ` m ) = f <-> f = ( m |` J ) ) )
139	138	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 ) )
140	130 132 139	3bitr4ri	|- ( E. m e. ( T i^i R ) ( ( o e. T |-> ( o |` J ) ) ` m ) = f <-> f e. ( ( NN0 ^m J ) i^i R ) )
141	126 140	bitri	|- ( f e. ( ( o e. T |-> ( o |` J ) ) " ( T i^i R ) ) <-> f e. ( ( NN0 ^m J ) i^i R ) )
142	141	eqriv	|- ( ( o e. T |-> ( o |` J ) ) " ( T i^i R ) ) = ( ( NN0 ^m J ) i^i R )
143		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 ) ) )
144	142 143	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 ) )
145		resmpt	|- ( ( T i^i R ) C_ T -> ( ( o e. T |-> ( o |` J ) ) |` ( T i^i R ) ) = ( o e. ( T i^i R ) |-> ( o |` J ) ) )
146		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 ) ) )
147	119 145 146	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 ) )
148	144 147	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 ) )
149	121 148	mpbi	|- ( o e. ( T i^i R ) |-> ( o |` J ) ) : ( T i^i R ) -1-1-onto-> ( ( NN0 ^m J ) i^i R )
150		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 } )
151	103 149 150	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 }
152		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 ) )
153		eqid	|- ( o e. ( T i^i R ) |-> ( o |` J ) ) = ( o e. ( T i^i R ) |-> ( o |` J ) )
154	153	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 ) )
155	154	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 ) )
156	149 152 155	mp2b	|- A. o e. ( T i^i R ) ( o |` J ) e. ( ( NN0 ^m J ) i^i R )
157	156	a1i	|- ( T. -> A. o e. ( T i^i R ) ( o |` J ) e. ( ( NN0 ^m J ) i^i R ) )
158		eqidd	|- ( T. -> ( o e. ( T i^i R ) |-> ( o |` J ) ) = ( o e. ( T i^i R ) |-> ( o |` J ) ) )
159		eqidd	|- ( T. -> ( f e. ( ( NN0 ^m J ) i^i R ) |-> ( bits o. f ) ) = ( f e. ( ( NN0 ^m J ) i^i R ) |-> ( bits o. f ) ) )
160		coeq2	|- ( f = ( o |` J ) -> ( bits o. f ) = ( bits o. ( o |` J ) ) )
161	157 158 159 160	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 ) ) ) )
162	161	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 ) ) ) )
163		eqidd	|- ( T. -> ( T i^i R ) = ( T i^i R ) )
164	6	a1i	|- ( T. -> H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin } )
165	162 163 164	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 } ) )
166	151 165	mpbiri	|- ( T. -> ( o e. ( T i^i R ) |-> ( bits o. ( o |` J ) ) ) : ( T i^i R ) -1-1-onto-> H )
167	166	mptru	|- ( o e. ( T i^i R ) |-> ( bits o. ( o |` J ) ) ) : ( T i^i R ) -1-1-onto-> H
168		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 ) )
169	53 167 168	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 )
170		eqidd	|- ( T. -> ( o e. ( T i^i R ) |-> ( bits o. ( o |` J ) ) ) = ( o e. ( T i^i R ) |-> ( bits o. ( o |` J ) ) ) )
171		bitsf	|- bits : ZZ --> ~P NN0
172		zex	|- ZZ e. _V
173		fex	|- ( ( bits : ZZ --> ~P NN0 /\ ZZ e. _V ) -> bits e. _V )
174	171 172 173	mp2an	|- bits e. _V
175	174 123	coex	|- ( bits o. ( o |` J ) ) e. _V
176	175	a1i	|- ( ( T. /\ o e. ( T i^i R ) ) -> ( bits o. ( o |` J ) ) e. _V )
177	170 176	fvmpt2d	|- ( ( T. /\ o e. ( T i^i R ) ) -> ( ( o e. ( T i^i R ) |-> ( bits o. ( o |` J ) ) ) ` o ) = ( bits o. ( o |` J ) ) )
178		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 )
179	166 178	syl	|- ( T. -> ( o e. ( T i^i R ) |-> ( bits o. ( o |` J ) ) ) : ( T i^i R ) --> H )
180	179	ffvelcdmda	|- ( ( T. /\ o e. ( T i^i R ) ) -> ( ( o e. ( T i^i R ) |-> ( bits o. ( o |` J ) ) ) ` o ) e. H )
181	177 180	eqeltrrd	|- ( ( T. /\ o e. ( T i^i R ) ) -> ( bits o. ( o |` J ) ) e. H )
182		f1ofn	|- ( M : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin ) -> M Fn H )
183	53 182	ax-mp	|- M Fn H
184		dffn5	|- ( M Fn H <-> M = ( r e. H |-> ( M ` r ) ) )
185	183 184	mpbi	|- M = ( r e. H |-> ( M ` r ) )
186	185	a1i	|- ( T. -> M = ( r e. H |-> ( M ` r ) ) )
187		fveq2	|- ( r = ( bits o. ( o |` J ) ) -> ( M ` r ) = ( M ` ( bits o. ( o |` J ) ) ) )
188	181 170 186 187	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 ) ) ) ) )
189	188	mptru	|- ( M o. ( o e. ( T i^i R ) |-> ( bits o. ( o |` J ) ) ) ) = ( o e. ( T i^i R ) |-> ( M ` ( bits o. ( o |` J ) ) ) )
190		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 ) ) )
191	189 190	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 ) )
192	169 191	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 )
193		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 ) )
194	52 192 193	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 )
195		simpr	|- ( ( T. /\ o e. ( T i^i R ) ) -> o e. ( T i^i R ) )
196		fvex	|- ( M ` ( bits o. ( o |` J ) ) ) e. _V
197		eqid	|- ( o e. ( T i^i R ) |-> ( M ` ( bits o. ( o |` J ) ) ) ) = ( o e. ( T i^i R ) |-> ( M ` ( bits o. ( o |` J ) ) ) )
198	197	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 ) ) ) )
199	195 196 198	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 ) ) ) )
200		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 ) )
201	192 200	mp1i	|- ( T. -> ( o e. ( T i^i R ) |-> ( M ` ( bits o. ( o |` J ) ) ) ) : ( T i^i R ) --> ( ~P ( J X. NN0 ) i^i Fin ) )
202	201	ffvelcdmda	|- ( ( 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 ) )
203	199 202	eqeltrrd	|- ( ( T. /\ o e. ( T i^i R ) ) -> ( M ` ( bits o. ( o |` J ) ) ) e. ( ~P ( J X. NN0 ) i^i Fin ) )
204		eqidd	|- ( T. -> ( o e. ( T i^i R ) |-> ( M ` ( bits o. ( o |` J ) ) ) ) = ( o e. ( T i^i R ) |-> ( M ` ( bits o. ( o |` J ) ) ) ) )
205		eqidd	|- ( T. -> ( a e. ( ~P ( J X. NN0 ) i^i Fin ) |-> ( F " a ) ) = ( a e. ( ~P ( J X. NN0 ) i^i Fin ) |-> ( F " a ) ) )
206		imaeq2	|- ( a = ( M ` ( bits o. ( o |` J ) ) ) -> ( F " a ) = ( F " ( M ` ( bits o. ( o |` J ) ) ) ) )
207	203 204 205 206	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 ) ) ) ) ) )
208	207	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 ) ) ) ) )
209		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 ) ) )
210	208 209	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 ) )
211	194 210	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 )
212		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 ) )
213	49 211 212	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 )
214	5	mpoexg	|- ( ( J e. _V /\ NN0 e. _V ) -> F e. _V )
215	56 58 214	mp2an	|- F e. _V
216		imaexg	|- ( F e. _V -> ( F " ( M ` ( bits o. ( o |` J ) ) ) ) e. _V )
217	215 216	ax-mp	|- ( F " ( M ` ( bits o. ( o |` J ) ) ) ) e. _V
218		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 ) ) ) ) )
219	218	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 ) ) ) ) )
220	195 217 219	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 ) ) ) ) )
221		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 ) )
222	211 221	mp1i	|- ( T. -> ( o e. ( T i^i R ) |-> ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) : ( T i^i R ) --> ( ~P NN i^i Fin ) )
223	222	ffvelcdmda	|- ( ( 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 ) )
224	220 223	eqeltrrd	|- ( ( T. /\ o e. ( T i^i R ) ) -> ( F " ( M ` ( bits o. ( o |` J ) ) ) ) e. ( ~P NN i^i Fin ) )
225		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 ) ) ) ) ) )
226		indf1o	|- ( NN e. _V -> ( _Ind ` NN ) : ~P NN -1-1-onto-> ( { 0 , 1 } ^m NN ) )
227		f1ofn	|- ( ( _Ind ` NN ) : ~P NN -1-1-onto-> ( { 0 , 1 } ^m NN ) -> ( _Ind ` NN ) Fn ~P NN )
228	11 226 227	mp2b	|- ( _Ind ` NN ) Fn ~P NN
229		dffn5	|- ( ( _Ind ` NN ) Fn ~P NN <-> ( _Ind ` NN ) = ( b e. ~P NN |-> ( ( _Ind ` NN ) ` b ) ) )
230	228 229	mpbi	|- ( _Ind ` NN ) = ( b e. ~P NN |-> ( ( _Ind ` NN ) ` b ) )
231	230	reseq1i	|- ( ( _Ind ` NN ) |` Fin ) = ( ( b e. ~P NN |-> ( ( _Ind ` NN ) ` b ) ) |` Fin )
232		resmpt3	|- ( ( b e. ~P NN |-> ( ( _Ind ` NN ) ` b ) ) |` Fin ) = ( b e. ( ~P NN i^i Fin ) |-> ( ( _Ind ` NN ) ` b ) )
233	231 232	eqtri	|- ( ( _Ind ` NN ) |` Fin ) = ( b e. ( ~P NN i^i Fin ) |-> ( ( _Ind ` NN ) ` b ) )
234	233	a1i	|- ( T. -> ( ( _Ind ` NN ) |` Fin ) = ( b e. ( ~P NN i^i Fin ) |-> ( ( _Ind ` NN ) ` b ) ) )
235		fveq2	|- ( b = ( F " ( M ` ( bits o. ( o |` J ) ) ) ) -> ( ( _Ind ` NN ) ` b ) = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) )
236	224 225 234 235	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 ) ) ) ) ) ) )
237	236	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 ) ) ) ) ) )
238	10 237	eqtr4i	|- G = ( ( ( _Ind ` NN ) |` Fin ) o. ( o e. ( T i^i R ) |-> ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) )
239		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 ) ) )
240	238 239	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 ) )
241	213 240	mpbir	|- G : ( T i^i R ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R )