Step |
Hyp |
Ref |
Expression |
1 |
|
oveq2 |
|- ( l = L -> ( 0 ..^ l ) = ( 0 ..^ L ) ) |
2 |
1
|
feq2d |
|- ( l = L -> ( W : ( 0 ..^ l ) --> S <-> W : ( 0 ..^ L ) --> S ) ) |
3 |
2
|
rspcev |
|- ( ( L e. NN0 /\ W : ( 0 ..^ L ) --> S ) -> E. l e. NN0 W : ( 0 ..^ l ) --> S ) |
4 |
|
0nn0 |
|- 0 e. NN0 |
5 |
|
fzo0n0 |
|- ( ( 0 ..^ L ) =/= (/) <-> L e. NN ) |
6 |
|
nnnn0 |
|- ( L e. NN -> L e. NN0 ) |
7 |
5 6
|
sylbi |
|- ( ( 0 ..^ L ) =/= (/) -> L e. NN0 ) |
8 |
7
|
necon1bi |
|- ( -. L e. NN0 -> ( 0 ..^ L ) = (/) ) |
9 |
|
fzo0 |
|- ( 0 ..^ 0 ) = (/) |
10 |
8 9
|
eqtr4di |
|- ( -. L e. NN0 -> ( 0 ..^ L ) = ( 0 ..^ 0 ) ) |
11 |
10
|
feq2d |
|- ( -. L e. NN0 -> ( W : ( 0 ..^ L ) --> S <-> W : ( 0 ..^ 0 ) --> S ) ) |
12 |
11
|
biimpa |
|- ( ( -. L e. NN0 /\ W : ( 0 ..^ L ) --> S ) -> W : ( 0 ..^ 0 ) --> S ) |
13 |
|
oveq2 |
|- ( l = 0 -> ( 0 ..^ l ) = ( 0 ..^ 0 ) ) |
14 |
13
|
feq2d |
|- ( l = 0 -> ( W : ( 0 ..^ l ) --> S <-> W : ( 0 ..^ 0 ) --> S ) ) |
15 |
14
|
rspcev |
|- ( ( 0 e. NN0 /\ W : ( 0 ..^ 0 ) --> S ) -> E. l e. NN0 W : ( 0 ..^ l ) --> S ) |
16 |
4 12 15
|
sylancr |
|- ( ( -. L e. NN0 /\ W : ( 0 ..^ L ) --> S ) -> E. l e. NN0 W : ( 0 ..^ l ) --> S ) |
17 |
3 16
|
pm2.61ian |
|- ( W : ( 0 ..^ L ) --> S -> E. l e. NN0 W : ( 0 ..^ l ) --> S ) |
18 |
|
iswrd |
|- ( W e. Word S <-> E. l e. NN0 W : ( 0 ..^ l ) --> S ) |
19 |
17 18
|
sylibr |
|- ( W : ( 0 ..^ L ) --> S -> W e. Word S ) |