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 ⊢ w ∈ Word V | ∃ n ∈ 0 ..^ W W cyclShift n = w ∈ V

Proof

Step Hyp Ref Expression
1 eqcom ⊢ W cyclShift n = w ↔ w = W cyclShift n
2 1 rexbii ⊢ ∃ n ∈ 0 ..^ W W cyclShift n = w ↔ ∃ n ∈ 0 ..^ W w = W cyclShift n
3 2 abbii ⊢ w | ∃ n ∈ 0 ..^ W W cyclShift n = w = w | ∃ n ∈ 0 ..^ W w = W cyclShift n
4 ovex ⊢ 0 ..^ W ∈ V
5 4 abrexex ⊢ w | ∃ n ∈ 0 ..^ W w = W cyclShift n ∈ V
6 3 5 eqeltri ⊢ w | ∃ n ∈ 0 ..^ W W cyclShift n = w ∈ V
7 rabssab ⊢ w ∈ Word V | ∃ n ∈ 0 ..^ W W cyclShift n = w ⊆ w | ∃ n ∈ 0 ..^ W W cyclShift n = w
8 6 7 ssexi ⊢ w ∈ Word V | ∃ n ∈ 0 ..^ W W cyclShift n = w ∈ V