Metamath Proof Explorer


Theorem swrdrn

Description: The range of a subword of a word is a subset of the set of symbols for the word. (Contributed by AV, 13-Nov-2018)

Ref Expression
Assertion swrdrn
|- ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ran ( W substr <. M , N >. ) C_ V )

Proof

Step Hyp Ref Expression
1 swrdf
 |-  ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ( W substr <. M , N >. ) : ( 0 ..^ ( N - M ) ) --> V )
2 1 frnd
 |-  ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ran ( W substr <. M , N >. ) C_ V )