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 { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 } ∈ V

Proof

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