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

Proof

Step Hyp Ref Expression
1 cshwrepswhash1.m ⊢ M = w ∈ Word V | ∃ n ∈ 0 ..^ W W cyclShift n = w
2 1 cshwsiun ⊢ W ∈ Word V → M = ⋃ n ∈ 0 ..^ W W cyclShift n
3 ovex ⊢ 0 ..^ W ∈ V
4 snex ⊢ W cyclShift n ∈ V
5 4 a1i ⊢ W ∈ Word V → W cyclShift n ∈ V
6 5 ralrimivw ⊢ W ∈ Word V → ∀ n ∈ 0 ..^ W W cyclShift n ∈ V
7 iunexg ⊢ 0 ..^ W ∈ V ∧ ∀ n ∈ 0 ..^ W W cyclShift n ∈ V → ⋃ n ∈ 0 ..^ W W cyclShift n ∈ V
8 3 6 7 sylancr ⊢ W ∈ Word V → ⋃ n ∈ 0 ..^ W W cyclShift n ∈ V
9 2 8 eqeltrd ⊢ W ∈ Word V → M ∈ V