Metamath Proof Explorer

Theorem cshwsexa

Description: The class of (different!) words resulting by cyclically shifting something (not necessarily a word) is a set. (Contributed by AV, 8-Jun-2018) (Revised by Mario Carneiro/AV, 25-Oct-2018) (Proof shortened by SN, 15-Jan-2025)

Ref Expression
Assertion cshwsexa 
|- { w e. Word V | E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w } e. _V

Proof

Step Hyp Ref Expression
1 eqcom 
 |-  ( ( W cyclShift n ) = w <-> w = ( W cyclShift n ) )
2 1 rexbii 
 |-  ( E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w <-> E. n e. ( 0 ..^ ( # ` W ) ) w = ( W cyclShift n ) )
3 2 abbii 
 |-  { w | E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w } = { w | E. n e. ( 0 ..^ ( # ` W ) ) w = ( W cyclShift n ) }
4 ovex 
 |-  ( 0 ..^ ( # ` W ) ) e. _V
5 4 abrexex 
 |-  { w | E. n e. ( 0 ..^ ( # ` W ) ) w = ( W cyclShift n ) } e. _V
6 3 5 eqeltri 
 |-  { w | E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w } e. _V
7 rabssab 
 |-  { w e. Word V | E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w } C_ { w | E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w }
8 6 7 ssexi 
 |-  { w e. Word V | E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w } e. _V