Metamath Proof Explorer

Theorem pfx0

Description: A prefix of an empty set is always the empty set. (Contributed by AV, 3-May-2020)

Ref Expression
Assertion pfx0 
|- ( (/) prefix L ) = (/)

Proof

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 ) = (/)