Metamath Proof Explorer

Theorem pfxid

Description: A word is a prefix of itself. (Contributed by Stefan O'Rear, 16-Aug-2015) (Revised by AV, 2-May-2020)

Ref Expression
Assertion pfxid 
|- ( S e. Word A -> ( S prefix ( # ` S ) ) = S )

Proof

Step Hyp Ref Expression
1 lencl 
 |-  ( S e. Word A -> ( # ` S ) e. NN0 )
2 nn0fz0 
 |-  ( ( # ` S ) e. NN0 <-> ( # ` S ) e. ( 0 ... ( # ` S ) ) )
3 1 2 sylib 
 |-  ( S e. Word A -> ( # ` S ) e. ( 0 ... ( # ` S ) ) )
4 pfxf 
 |-  ( ( S e. Word A /\ ( # ` S ) e. ( 0 ... ( # ` S ) ) ) -> ( S prefix ( # ` S ) ) : ( 0 ..^ ( # ` S ) ) --> A )
5 3 4 mpdan 
 |-  ( S e. Word A -> ( S prefix ( # ` S ) ) : ( 0 ..^ ( # ` S ) ) --> A )
6 5 ffnd 
 |-  ( S e. Word A -> ( S prefix ( # ` S ) ) Fn ( 0 ..^ ( # ` S ) ) )
7 wrdfn 
 |-  ( S e. Word A -> S Fn ( 0 ..^ ( # ` S ) ) )
8 simpl 
 |-  ( ( S e. Word A /\ x e. ( 0 ..^ ( # ` S ) ) ) -> S e. Word A )
9 3 adantr 
 |-  ( ( S e. Word A /\ x e. ( 0 ..^ ( # ` S ) ) ) -> ( # ` S ) e. ( 0 ... ( # ` S ) ) )
10 simpr 
 |-  ( ( S e. Word A /\ x e. ( 0 ..^ ( # ` S ) ) ) -> x e. ( 0 ..^ ( # ` S ) ) )
11 pfxfv 
 |-  ( ( S e. Word A /\ ( # ` S ) e. ( 0 ... ( # ` S ) ) /\ x e. ( 0 ..^ ( # ` S ) ) ) -> ( ( S prefix ( # ` S ) ) ` x ) = ( S ` x ) )
12 8 9 10 11 syl3anc 
 |-  ( ( S e. Word A /\ x e. ( 0 ..^ ( # ` S ) ) ) -> ( ( S prefix ( # ` S ) ) ` x ) = ( S ` x ) )
13 6 7 12 eqfnfvd 
 |-  ( S e. Word A -> ( S prefix ( # ` S ) ) = S )