Metamath Proof Explorer

Theorem cshwrn

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

Ref Expression
Assertion cshwrn 
|- ( ( W e. Word V /\ N e. ZZ ) -> ran ( W cyclShift N ) C_ V )

Proof

Step Hyp Ref Expression
1 cshwf 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ( W cyclShift N ) : ( 0 ..^ ( # ` W ) ) --> V )
2 1 frnd 
 |-  ( ( W e. Word V /\ N e. ZZ ) -> ran ( W cyclShift N ) C_ V )