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

Metamath Proof Explorer

Theorem cshwsex

Description: The class of (different!) words resulting by cyclically shifting a given word is a set. (Contributed by AV, 8-Jun-2018) (Revised by AV, 8-Nov-2018)

Ref Expression
Hypothesis cshwrepswhash1.m 
|- M = { w e. Word V | E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w }
Assertion cshwsex 
|- ( W e. Word V -> M e. _V )

Proof

Step Hyp Ref Expression
1 cshwrepswhash1.m 
 |-  M = { w e. Word V | E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w }
2 1 cshwsiun 
 |-  ( W e. Word V -> M = U_ n e. ( 0 ..^ ( # ` W ) ) { ( W cyclShift n ) } )
3 ovex 
 |-  ( 0 ..^ ( # ` W ) ) e. _V
4 snex 
 |-  { ( W cyclShift n ) } e. _V
5 4 a1i 
 |-  ( W e. Word V -> { ( W cyclShift n ) } e. _V )
6 5 ralrimivw 
 |-  ( W e. Word V -> A. n e. ( 0 ..^ ( # ` W ) ) { ( W cyclShift n ) } e. _V )
7 iunexg 
 |-  ( ( ( 0 ..^ ( # ` W ) ) e. _V /\ A. n e. ( 0 ..^ ( # ` W ) ) { ( W cyclShift n ) } e. _V ) -> U_ n e. ( 0 ..^ ( # ` W ) ) { ( W cyclShift n ) } e. _V )
8 3 6 7 sylancr 
 |-  ( W e. Word V -> U_ n e. ( 0 ..^ ( # ` W ) ) { ( W cyclShift n ) } e. _V )
9 2 8 eqeltrd 
 |-  ( W e. Word V -> M e. _V )