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 )