Metamath Proof Explorer


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 )