This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iswrdsymb

Description: An arbitrary word is a word over an alphabet if all of its symbols belong to the alphabet. (Contributed by AV, 23-Jan-2021)

Ref Expression
Assertion iswrdsymb 
|- ( ( W e. Word _V /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) e. V ) -> W e. Word V )

Proof

Step Hyp Ref Expression
1 wrdfn 
 |-  ( W e. Word _V -> W Fn ( 0 ..^ ( # ` W ) ) )
2 1 anim1i 
 |-  ( ( W e. Word _V /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) e. V ) -> ( W Fn ( 0 ..^ ( # ` W ) ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) e. V ) )
3 ffnfv 
 |-  ( W : ( 0 ..^ ( # ` W ) ) --> V <-> ( W Fn ( 0 ..^ ( # ` W ) ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) e. V ) )
4 2 3 sylibr 
 |-  ( ( W e. Word _V /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) e. V ) -> W : ( 0 ..^ ( # ` W ) ) --> V )
5 iswrdi 
 |-  ( W : ( 0 ..^ ( # ` W ) ) --> V -> W e. Word V )
6 4 5 syl 
 |-  ( ( W e. Word _V /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) e. V ) -> W e. Word V )