# 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 𝑀 = { 𝑤 ∈ 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 )