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 ) |