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	⊢ 𝑀 = { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 }
Assertion	cshwsex	⊢ ( 𝑊 ∈ Word 𝑉 → 𝑀 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		cshwrepswhash1.m	⊢ 𝑀 = { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 }
2	1	cshwsiun	⊢ ( 𝑊 ∈ Word 𝑉 → 𝑀 = ∪ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) { ( 𝑊 cyclShift 𝑛 ) } )
3		ovex	⊢ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∈ V
4		snex	⊢ { ( 𝑊 cyclShift 𝑛 ) } ∈ V
5	4	a1i	⊢ ( 𝑊 ∈ Word 𝑉 → { ( 𝑊 cyclShift 𝑛 ) } ∈ V )
6	5	ralrimivw	⊢ ( 𝑊 ∈ Word 𝑉 → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) { ( 𝑊 cyclShift 𝑛 ) } ∈ V )
7		iunexg	⊢ ( ( ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∈ V ∧ ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) { ( 𝑊 cyclShift 𝑛 ) } ∈ V ) → ∪ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) { ( 𝑊 cyclShift 𝑛 ) } ∈ V )
8	3 6 7	sylancr	⊢ ( 𝑊 ∈ Word 𝑉 → ∪ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) { ( 𝑊 cyclShift 𝑛 ) } ∈ V )
9	2 8	eqeltrd	⊢ ( 𝑊 ∈ Word 𝑉 → 𝑀 ∈ V )