Metamath Proof Explorer

Theorem wrdsymb

Description: A word is a word over the symbols it consists of. (Contributed by AV, 1-Dec-2022)

Ref Expression
Assertion wrdsymb 
|- ( S e. Word A -> S e. Word ( S " ( 0 ..^ ( # ` S ) ) ) )

Proof

Step Hyp Ref Expression
1 wrdf 
 |-  ( S e. Word A -> S : ( 0 ..^ ( # ` S ) ) --> A )
2 fimadmfo 
 |-  ( S : ( 0 ..^ ( # ` S ) ) --> A -> S : ( 0 ..^ ( # ` S ) ) -onto-> ( S " ( 0 ..^ ( # ` S ) ) ) )
3 fof 
 |-  ( S : ( 0 ..^ ( # ` S ) ) -onto-> ( S " ( 0 ..^ ( # ` S ) ) ) -> S : ( 0 ..^ ( # ` S ) ) --> ( S " ( 0 ..^ ( # ` S ) ) ) )
4 1 2 3 3syl 
 |-  ( S e. Word A -> S : ( 0 ..^ ( # ` S ) ) --> ( S " ( 0 ..^ ( # ` S ) ) ) )
5 iswrdb 
 |-  ( S e. Word ( S " ( 0 ..^ ( # ` S ) ) ) <-> S : ( 0 ..^ ( # ` S ) ) --> ( S " ( 0 ..^ ( # ` S ) ) ) )
6 4 5 sylibr 
 |-  ( S e. Word A -> S e. Word ( S " ( 0 ..^ ( # ` S ) ) ) )