Step |
Hyp |
Ref |
Expression |
1 |
|
efgval.w |
|- W = ( _I ` Word ( I X. 2o ) ) |
2 |
|
efgval.r |
|- .~ = ( ~FG ` I ) |
3 |
|
efgval2.m |
|- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) |
4 |
|
efgval2.t |
|- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) ) |
5 |
1 2
|
efgval |
|- .~ = |^| { r | ( r Er W /\ A. x e. W A. m e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) } |
6 |
1 2 3 4
|
efgtf |
|- ( x e. W -> ( ( T ` x ) = ( m e. ( 0 ... ( # ` x ) ) , u e. ( I X. 2o ) |-> ( x splice <. m , m , <" u ( M ` u ) "> >. ) ) /\ ( T ` x ) : ( ( 0 ... ( # ` x ) ) X. ( I X. 2o ) ) --> W ) ) |
7 |
6
|
simpld |
|- ( x e. W -> ( T ` x ) = ( m e. ( 0 ... ( # ` x ) ) , u e. ( I X. 2o ) |-> ( x splice <. m , m , <" u ( M ` u ) "> >. ) ) ) |
8 |
7
|
rneqd |
|- ( x e. W -> ran ( T ` x ) = ran ( m e. ( 0 ... ( # ` x ) ) , u e. ( I X. 2o ) |-> ( x splice <. m , m , <" u ( M ` u ) "> >. ) ) ) |
9 |
8
|
sseq1d |
|- ( x e. W -> ( ran ( T ` x ) C_ [ x ] r <-> ran ( m e. ( 0 ... ( # ` x ) ) , u e. ( I X. 2o ) |-> ( x splice <. m , m , <" u ( M ` u ) "> >. ) ) C_ [ x ] r ) ) |
10 |
|
dfss3 |
|- ( ran ( m e. ( 0 ... ( # ` x ) ) , u e. ( I X. 2o ) |-> ( x splice <. m , m , <" u ( M ` u ) "> >. ) ) C_ [ x ] r <-> A. a e. ran ( m e. ( 0 ... ( # ` x ) ) , u e. ( I X. 2o ) |-> ( x splice <. m , m , <" u ( M ` u ) "> >. ) ) a e. [ x ] r ) |
11 |
|
ovex |
|- ( x splice <. m , m , <" u ( M ` u ) "> >. ) e. _V |
12 |
11
|
rgen2w |
|- A. m e. ( 0 ... ( # ` x ) ) A. u e. ( I X. 2o ) ( x splice <. m , m , <" u ( M ` u ) "> >. ) e. _V |
13 |
|
eqid |
|- ( m e. ( 0 ... ( # ` x ) ) , u e. ( I X. 2o ) |-> ( x splice <. m , m , <" u ( M ` u ) "> >. ) ) = ( m e. ( 0 ... ( # ` x ) ) , u e. ( I X. 2o ) |-> ( x splice <. m , m , <" u ( M ` u ) "> >. ) ) |
14 |
|
vex |
|- a e. _V |
15 |
|
vex |
|- x e. _V |
16 |
14 15
|
elec |
|- ( a e. [ x ] r <-> x r a ) |
17 |
|
breq2 |
|- ( a = ( x splice <. m , m , <" u ( M ` u ) "> >. ) -> ( x r a <-> x r ( x splice <. m , m , <" u ( M ` u ) "> >. ) ) ) |
18 |
16 17
|
syl5bb |
|- ( a = ( x splice <. m , m , <" u ( M ` u ) "> >. ) -> ( a e. [ x ] r <-> x r ( x splice <. m , m , <" u ( M ` u ) "> >. ) ) ) |
19 |
13 18
|
ralrnmpo |
|- ( A. m e. ( 0 ... ( # ` x ) ) A. u e. ( I X. 2o ) ( x splice <. m , m , <" u ( M ` u ) "> >. ) e. _V -> ( A. a e. ran ( m e. ( 0 ... ( # ` x ) ) , u e. ( I X. 2o ) |-> ( x splice <. m , m , <" u ( M ` u ) "> >. ) ) a e. [ x ] r <-> A. m e. ( 0 ... ( # ` x ) ) A. u e. ( I X. 2o ) x r ( x splice <. m , m , <" u ( M ` u ) "> >. ) ) ) |
20 |
12 19
|
ax-mp |
|- ( A. a e. ran ( m e. ( 0 ... ( # ` x ) ) , u e. ( I X. 2o ) |-> ( x splice <. m , m , <" u ( M ` u ) "> >. ) ) a e. [ x ] r <-> A. m e. ( 0 ... ( # ` x ) ) A. u e. ( I X. 2o ) x r ( x splice <. m , m , <" u ( M ` u ) "> >. ) ) |
21 |
|
id |
|- ( u = <. a , b >. -> u = <. a , b >. ) |
22 |
|
fveq2 |
|- ( u = <. a , b >. -> ( M ` u ) = ( M ` <. a , b >. ) ) |
23 |
|
df-ov |
|- ( a M b ) = ( M ` <. a , b >. ) |
24 |
22 23
|
eqtr4di |
|- ( u = <. a , b >. -> ( M ` u ) = ( a M b ) ) |
25 |
21 24
|
s2eqd |
|- ( u = <. a , b >. -> <" u ( M ` u ) "> = <" <. a , b >. ( a M b ) "> ) |
26 |
25
|
oteq3d |
|- ( u = <. a , b >. -> <. m , m , <" u ( M ` u ) "> >. = <. m , m , <" <. a , b >. ( a M b ) "> >. ) |
27 |
26
|
oveq2d |
|- ( u = <. a , b >. -> ( x splice <. m , m , <" u ( M ` u ) "> >. ) = ( x splice <. m , m , <" <. a , b >. ( a M b ) "> >. ) ) |
28 |
27
|
breq2d |
|- ( u = <. a , b >. -> ( x r ( x splice <. m , m , <" u ( M ` u ) "> >. ) <-> x r ( x splice <. m , m , <" <. a , b >. ( a M b ) "> >. ) ) ) |
29 |
28
|
ralxp |
|- ( A. u e. ( I X. 2o ) x r ( x splice <. m , m , <" u ( M ` u ) "> >. ) <-> A. a e. I A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. ( a M b ) "> >. ) ) |
30 |
|
eqidd |
|- ( ( a e. I /\ b e. 2o ) -> <. a , b >. = <. a , b >. ) |
31 |
3
|
efgmval |
|- ( ( a e. I /\ b e. 2o ) -> ( a M b ) = <. a , ( 1o \ b ) >. ) |
32 |
30 31
|
s2eqd |
|- ( ( a e. I /\ b e. 2o ) -> <" <. a , b >. ( a M b ) "> = <" <. a , b >. <. a , ( 1o \ b ) >. "> ) |
33 |
32
|
oteq3d |
|- ( ( a e. I /\ b e. 2o ) -> <. m , m , <" <. a , b >. ( a M b ) "> >. = <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) |
34 |
33
|
oveq2d |
|- ( ( a e. I /\ b e. 2o ) -> ( x splice <. m , m , <" <. a , b >. ( a M b ) "> >. ) = ( x splice <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) |
35 |
34
|
breq2d |
|- ( ( a e. I /\ b e. 2o ) -> ( x r ( x splice <. m , m , <" <. a , b >. ( a M b ) "> >. ) <-> x r ( x splice <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) ) |
36 |
35
|
ralbidva |
|- ( a e. I -> ( A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. ( a M b ) "> >. ) <-> A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) ) |
37 |
36
|
ralbiia |
|- ( A. a e. I A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. ( a M b ) "> >. ) <-> A. a e. I A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) |
38 |
29 37
|
bitri |
|- ( A. u e. ( I X. 2o ) x r ( x splice <. m , m , <" u ( M ` u ) "> >. ) <-> A. a e. I A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) |
39 |
38
|
ralbii |
|- ( A. m e. ( 0 ... ( # ` x ) ) A. u e. ( I X. 2o ) x r ( x splice <. m , m , <" u ( M ` u ) "> >. ) <-> A. m e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) |
40 |
20 39
|
bitri |
|- ( A. a e. ran ( m e. ( 0 ... ( # ` x ) ) , u e. ( I X. 2o ) |-> ( x splice <. m , m , <" u ( M ` u ) "> >. ) ) a e. [ x ] r <-> A. m e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) |
41 |
10 40
|
bitri |
|- ( ran ( m e. ( 0 ... ( # ` x ) ) , u e. ( I X. 2o ) |-> ( x splice <. m , m , <" u ( M ` u ) "> >. ) ) C_ [ x ] r <-> A. m e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) |
42 |
9 41
|
bitrdi |
|- ( x e. W -> ( ran ( T ` x ) C_ [ x ] r <-> A. m e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) ) |
43 |
42
|
ralbiia |
|- ( A. x e. W ran ( T ` x ) C_ [ x ] r <-> A. x e. W A. m e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) |
44 |
43
|
anbi2i |
|- ( ( r Er W /\ A. x e. W ran ( T ` x ) C_ [ x ] r ) <-> ( r Er W /\ A. x e. W A. m e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) ) |
45 |
44
|
abbii |
|- { r | ( r Er W /\ A. x e. W ran ( T ` x ) C_ [ x ] r ) } = { r | ( r Er W /\ A. x e. W A. m e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) } |
46 |
45
|
inteqi |
|- |^| { r | ( r Er W /\ A. x e. W ran ( T ` x ) C_ [ x ] r ) } = |^| { r | ( r Er W /\ A. x e. W A. m e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) } |
47 |
5 46
|
eqtr4i |
|- .~ = |^| { r | ( r Er W /\ A. x e. W ran ( T ` x ) C_ [ x ] r ) } |