Metamath Proof Explorer

Theorem pfxcl

Description: Closure of the prefix extractor. (Contributed by AV, 2-May-2020)

Ref Expression
Assertion pfxcl 
|- ( S e. Word A -> ( S prefix L ) e. Word A )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( ( S prefix L ) = (/) -> ( ( S prefix L ) e. Word A <-> (/) e. Word A ) )
2 n0 
 |-  ( ( S prefix L ) =/= (/) <-> E. x x e. ( S prefix L ) )
3 df-pfx 
 |-  prefix = ( s e. _V , l e. NN0 |-> ( s substr <. 0 , l >. ) )
4 3 elmpocl2 
 |-  ( x e. ( S prefix L ) -> L e. NN0 )
5 4 exlimiv 
 |-  ( E. x x e. ( S prefix L ) -> L e. NN0 )
6 2 5 sylbi 
 |-  ( ( S prefix L ) =/= (/) -> L e. NN0 )
7 pfxval 
 |-  ( ( S e. Word A /\ L e. NN0 ) -> ( S prefix L ) = ( S substr <. 0 , L >. ) )
8 swrdcl 
 |-  ( S e. Word A -> ( S substr <. 0 , L >. ) e. Word A )
9 8 adantr 
 |-  ( ( S e. Word A /\ L e. NN0 ) -> ( S substr <. 0 , L >. ) e. Word A )
10 7 9 eqeltrd 
 |-  ( ( S e. Word A /\ L e. NN0 ) -> ( S prefix L ) e. Word A )
11 6 10 sylan2 
 |-  ( ( S e. Word A /\ ( S prefix L ) =/= (/) ) -> ( S prefix L ) e. Word A )
12 wrd0 
 |-  (/) e. Word A
13 12 a1i 
 |-  ( S e. Word A -> (/) e. Word A )
14 1 11 13 pm2.61ne 
 |-  ( S e. Word A -> ( S prefix L ) e. Word A )