Step |
Hyp |
Ref |
Expression |
1 |
|
wrdfn |
|- ( W e. Word V -> W Fn ( 0 ..^ ( # ` W ) ) ) |
2 |
1
|
adantr |
|- ( ( W e. Word V /\ ( # ` W ) = 3 ) -> W Fn ( 0 ..^ ( # ` W ) ) ) |
3 |
|
oveq2 |
|- ( ( # ` W ) = 3 -> ( 0 ..^ ( # ` W ) ) = ( 0 ..^ 3 ) ) |
4 |
|
fzo0to3tp |
|- ( 0 ..^ 3 ) = { 0 , 1 , 2 } |
5 |
3 4
|
eqtr2di |
|- ( ( # ` W ) = 3 -> { 0 , 1 , 2 } = ( 0 ..^ ( # ` W ) ) ) |
6 |
5
|
adantl |
|- ( ( W e. Word V /\ ( # ` W ) = 3 ) -> { 0 , 1 , 2 } = ( 0 ..^ ( # ` W ) ) ) |
7 |
6
|
fneq2d |
|- ( ( W e. Word V /\ ( # ` W ) = 3 ) -> ( W Fn { 0 , 1 , 2 } <-> W Fn ( 0 ..^ ( # ` W ) ) ) ) |
8 |
2 7
|
mpbird |
|- ( ( W e. Word V /\ ( # ` W ) = 3 ) -> W Fn { 0 , 1 , 2 } ) |
9 |
|
c0ex |
|- 0 e. _V |
10 |
|
1ex |
|- 1 e. _V |
11 |
|
2ex |
|- 2 e. _V |
12 |
9 10 11
|
fntpb |
|- ( W Fn { 0 , 1 , 2 } <-> W = { <. 0 , ( W ` 0 ) >. , <. 1 , ( W ` 1 ) >. , <. 2 , ( W ` 2 ) >. } ) |
13 |
8 12
|
sylib |
|- ( ( W e. Word V /\ ( # ` W ) = 3 ) -> W = { <. 0 , ( W ` 0 ) >. , <. 1 , ( W ` 1 ) >. , <. 2 , ( W ` 2 ) >. } ) |