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

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) (Proof shortened by SN, 15-Jan-2025)

Ref Expression
Assertion cshwsexa { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 } ∈ V

Proof

Step Hyp Ref Expression
1 eqcom ⊢ ( ( 𝑊 cyclShift 𝑛 ) = 𝑤 ↔ 𝑤 = ( 𝑊 cyclShift 𝑛 ) )
2 1 rexbii ⊢ ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 ↔ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) )
3 2 abbii ⊢ { 𝑤 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 } = { 𝑤 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) }
4 ovex ⊢ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∈ V
5 4 abrexex ⊢ { 𝑤 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) } ∈ V
6 3 5 eqeltri ⊢ { 𝑤 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 } ∈ V
7 rabssab ⊢ { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 } ⊆ { 𝑤 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 }
8 6 7 ssexi ⊢ { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 } ∈ V