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)

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 df-rab 
 |-  { w e. Word V | E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w } = { w | ( w e. Word V /\ E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w ) }
2 r19.42v 
 |-  ( E. n e. ( 0 ..^ ( # ` W ) ) ( w e. Word V /\ ( W cyclShift n ) = w ) <-> ( w e. Word V /\ E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w ) )
3 2 bicomi 
 |-  ( ( w e. Word V /\ E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w ) <-> E. n e. ( 0 ..^ ( # ` W ) ) ( w e. Word V /\ ( W cyclShift n ) = w ) )
4 3 abbii 
 |-  { w | ( w e. Word V /\ E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w ) } = { w | E. n e. ( 0 ..^ ( # ` W ) ) ( w e. Word V /\ ( W cyclShift n ) = w ) }
5 df-rex 
 |-  ( E. n e. ( 0 ..^ ( # ` W ) ) ( w e. Word V /\ ( W cyclShift n ) = w ) <-> E. n ( n e. ( 0 ..^ ( # ` W ) ) /\ ( w e. Word V /\ ( W cyclShift n ) = w ) ) )
6 5 abbii 
 |-  { w | E. n e. ( 0 ..^ ( # ` W ) ) ( w e. Word V /\ ( W cyclShift n ) = w ) } = { w | E. n ( n e. ( 0 ..^ ( # ` W ) ) /\ ( w e. Word V /\ ( W cyclShift n ) = w ) ) }
7 1 4 6 3eqtri 
 |-  { w e. Word V | E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w } = { w | E. n ( n e. ( 0 ..^ ( # ` W ) ) /\ ( w e. Word V /\ ( W cyclShift n ) = w ) ) }
8 abid2 
 |-  { n | n e. ( 0 ..^ ( # ` W ) ) } = ( 0 ..^ ( # ` W ) )
9 8 ovexi 
 |-  { n | n e. ( 0 ..^ ( # ` W ) ) } e. _V
10 tru 
 |-  T.
11 10 10 pm3.2i 
 |-  ( T. /\ T. )
12 ovexd 
 |-  ( T. -> ( W cyclShift n ) e. _V )
13 eqtr3 
 |-  ( ( w = ( W cyclShift n ) /\ y = ( W cyclShift n ) ) -> w = y )
14 13 ex 
 |-  ( w = ( W cyclShift n ) -> ( y = ( W cyclShift n ) -> w = y ) )
15 14 eqcoms 
 |-  ( ( W cyclShift n ) = w -> ( y = ( W cyclShift n ) -> w = y ) )
16 15 adantl 
 |-  ( ( w e. Word V /\ ( W cyclShift n ) = w ) -> ( y = ( W cyclShift n ) -> w = y ) )
17 16 com12 
 |-  ( y = ( W cyclShift n ) -> ( ( w e. Word V /\ ( W cyclShift n ) = w ) -> w = y ) )
18 17 ad2antlr 
 |-  ( ( ( T. /\ y = ( W cyclShift n ) ) /\ T. ) -> ( ( w e. Word V /\ ( W cyclShift n ) = w ) -> w = y ) )
19 18 alrimiv 
 |-  ( ( ( T. /\ y = ( W cyclShift n ) ) /\ T. ) -> A. w ( ( w e. Word V /\ ( W cyclShift n ) = w ) -> w = y ) )
20 19 ex 
 |-  ( ( T. /\ y = ( W cyclShift n ) ) -> ( T. -> A. w ( ( w e. Word V /\ ( W cyclShift n ) = w ) -> w = y ) ) )
21 12 20 spcimedv 
 |-  ( T. -> ( T. -> E. y A. w ( ( w e. Word V /\ ( W cyclShift n ) = w ) -> w = y ) ) )
22 21 imp 
 |-  ( ( T. /\ T. ) -> E. y A. w ( ( w e. Word V /\ ( W cyclShift n ) = w ) -> w = y ) )
23 11 22 mp1i 
 |-  ( n e. ( 0 ..^ ( # ` W ) ) -> E. y A. w ( ( w e. Word V /\ ( W cyclShift n ) = w ) -> w = y ) )
24 9 23 zfrep4 
 |-  { w | E. n ( n e. ( 0 ..^ ( # ` W ) ) /\ ( w e. Word V /\ ( W cyclShift n ) = w ) ) } e. _V
25 7 24 eqeltri 
 |-  { w e. Word V | E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w } e. _V