Metamath Proof Explorer

Theorem pfx00

Description: The zero length prefix is the empty set. (Contributed by AV, 2-May-2020)

Ref Expression
Assertion pfx00 
|- ( S prefix 0 ) = (/)

Proof

Step Hyp Ref Expression
1 opelxp 
 |-  ( <. S , 0 >. e. ( _V X. NN0 ) <-> ( S e. _V /\ 0 e. NN0 ) )
2 pfxval 
 |-  ( ( S e. _V /\ 0 e. NN0 ) -> ( S prefix 0 ) = ( S substr <. 0 , 0 >. ) )
3 swrd00 
 |-  ( S substr <. 0 , 0 >. ) = (/)
4 2 3 eqtrdi 
 |-  ( ( S e. _V /\ 0 e. NN0 ) -> ( S prefix 0 ) = (/) )
5 1 4 sylbi 
 |-  ( <. S , 0 >. e. ( _V X. NN0 ) -> ( S prefix 0 ) = (/) )
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 
 |-  ( <. S , 0 >. e. dom prefix -> ( S prefix 0 ) = (/) )
10 df-ov 
 |-  ( S prefix 0 ) = ( prefix ` <. S , 0 >. )
11 ndmfv 
 |-  ( -. <. S , 0 >. e. dom prefix -> ( prefix ` <. S , 0 >. ) = (/) )
12 10 11 syl5eq 
 |-  ( -. <. S , 0 >. e. dom prefix -> ( S prefix 0 ) = (/) )
13 9 12 pm2.61i 
 |-  ( S prefix 0 ) = (/)