| Step |
Hyp |
Ref |
Expression |
| 1 |
|
opelxp |
|- ( <. (/) , L >. e. ( _V X. NN0 ) <-> ( (/) e. _V /\ L e. NN0 ) ) |
| 2 |
|
pfxval |
|- ( ( (/) e. _V /\ L e. NN0 ) -> ( (/) prefix L ) = ( (/) substr <. 0 , L >. ) ) |
| 3 |
|
swrd0 |
|- ( (/) substr <. 0 , L >. ) = (/) |
| 4 |
2 3
|
eqtrdi |
|- ( ( (/) e. _V /\ L e. NN0 ) -> ( (/) prefix L ) = (/) ) |
| 5 |
1 4
|
sylbi |
|- ( <. (/) , L >. e. ( _V X. NN0 ) -> ( (/) prefix L ) = (/) ) |
| 6 |
|
df-pfx |
|- prefix = ( s e. _V , l e. NN0 |-> ( s substr <. 0 , l >. ) ) |
| 7 |
|
ovex |
|- ( s substr <. 0 , l >. ) e. _V |
| 8 |
6 7
|
dmmpo |
|- dom prefix = ( _V X. NN0 ) |
| 9 |
5 8
|
eleq2s |
|- ( <. (/) , L >. e. dom prefix -> ( (/) prefix L ) = (/) ) |
| 10 |
|
df-ov |
|- ( (/) prefix L ) = ( prefix ` <. (/) , L >. ) |
| 11 |
|
ndmfv |
|- ( -. <. (/) , L >. e. dom prefix -> ( prefix ` <. (/) , L >. ) = (/) ) |
| 12 |
10 11
|
eqtrid |
|- ( -. <. (/) , L >. e. dom prefix -> ( (/) prefix L ) = (/) ) |
| 13 |
9 12
|
pm2.61i |
|- ( (/) prefix L ) = (/) |