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