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)

Ref Expression
Assertion cshwsexa ⊢ w ∈ Word V | ∃ n ∈ 0 ..^ W W cyclShift n = w ∈ V

Proof

Step Hyp Ref Expression
1 df-rab ⊢ w ∈ Word V | ∃ n ∈ 0 ..^ W W cyclShift n = w = w | w ∈ Word V ∧ ∃ n ∈ 0 ..^ W W cyclShift n = w
2 r19.42v ⊢ ∃ n ∈ 0 ..^ W w ∈ Word V ∧ W cyclShift n = w ↔ w ∈ Word V ∧ ∃ n ∈ 0 ..^ W W cyclShift n = w
3 2 bicomi ⊢ w ∈ Word V ∧ ∃ n ∈ 0 ..^ W W cyclShift n = w ↔ ∃ n ∈ 0 ..^ W w ∈ Word V ∧ W cyclShift n = w
4 3 abbii ⊢ w | w ∈ Word V ∧ ∃ n ∈ 0 ..^ W W cyclShift n = w = w | ∃ n ∈ 0 ..^ W w ∈ Word V ∧ W cyclShift n = w
5 df-rex ⊢ ∃ n ∈ 0 ..^ W w ∈ Word V ∧ W cyclShift n = w ↔ ∃ n n ∈ 0 ..^ W ∧ w ∈ Word V ∧ W cyclShift n = w
6 5 abbii ⊢ w | ∃ n ∈ 0 ..^ W w ∈ Word V ∧ W cyclShift n = w = w | ∃ n n ∈ 0 ..^ W ∧ w ∈ Word V ∧ W cyclShift n = w
7 1 4 6 3eqtri ⊢ w ∈ Word V | ∃ n ∈ 0 ..^ W W cyclShift n = w = w | ∃ n n ∈ 0 ..^ W ∧ w ∈ Word V ∧ W cyclShift n = w
8 abid2 ⊢ n | n ∈ 0 ..^ W = 0 ..^ W
9 8 ovexi ⊢ n | n ∈ 0 ..^ W ∈ V
10 tru ⊢ ⊤
11 10 10 pm3.2i ⊢ ⊤ ∧ ⊤
12 ovexd ⊢ ⊤ → W cyclShift n ∈ V
13 eqtr3 ⊢ w = W cyclShift n ∧ y = W cyclShift n → w = y
14 13 ex ⊢ w = W cyclShift n → y = W cyclShift n → w = y
15 14 eqcoms ⊢ W cyclShift n = w → y = W cyclShift n → w = y
16 15 adantl ⊢ w ∈ Word V ∧ W cyclShift n = w → y = W cyclShift n → w = y
17 16 com12 ⊢ y = W cyclShift n → w ∈ Word V ∧ W cyclShift n = w → w = y
18 17 ad2antlr ⊢ ⊤ ∧ y = W cyclShift n ∧ ⊤ → w ∈ Word V ∧ W cyclShift n = w → w = y
19 18 alrimiv ⊢ ⊤ ∧ y = W cyclShift n ∧ ⊤ → ∀ w w ∈ Word V ∧ W cyclShift n = w → w = y
20 19 ex ⊢ ⊤ ∧ y = W cyclShift n → ⊤ → ∀ w w ∈ Word V ∧ W cyclShift n = w → w = y
21 12 20 spcimedv ⊢ ⊤ → ⊤ → ∃ y ∀ w w ∈ Word V ∧ W cyclShift n = w → w = y
22 21 imp ⊢ ⊤ ∧ ⊤ → ∃ y ∀ w w ∈ Word V ∧ W cyclShift n = w → w = y
23 11 22 mp1i ⊢ n ∈ 0 ..^ W → ∃ y ∀ w w ∈ Word V ∧ W cyclShift n = w → w = y
24 9 23 zfrep4 ⊢ w | ∃ n n ∈ 0 ..^ W ∧ w ∈ Word V ∧ W cyclShift n = w ∈ V
25 7 24 eqeltri ⊢ w ∈ Word V | ∃ n ∈ 0 ..^ W W cyclShift n = w ∈ V