This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )