Theorem cshwsexa 13570

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.)

Assertion

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

Distinct variable groups:   𝑛,𝑉   𝑛,𝑊,𝑤

Allowed substitution hint:   𝑉(𝑤)

Proof of Theorem cshwsexa

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-rab 2921	. . 3 ⊢ {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤} = {𝑤 ∣ (𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤)}
2		r19.42v 3092	. . . . 5 ⊢ (∃𝑛 ∈ (0..^(#‘𝑊))(𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) ↔ (𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤))
3	2	bicomi 214	. . . 4 ⊢ ((𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤) ↔ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤))
4	3	abbii 2739	. . 3 ⊢ {𝑤 ∣ (𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤)} = {𝑤 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤)}
5		df-rex 2918	. . . 4 ⊢ (∃𝑛 ∈ (0..^(#‘𝑊))(𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) ↔ ∃𝑛(𝑛 ∈ (0..^(#‘𝑊)) ∧ (𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤)))
6	5	abbii 2739	. . 3 ⊢ {𝑤 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤)} = {𝑤 ∣ ∃𝑛(𝑛 ∈ (0..^(#‘𝑊)) ∧ (𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤))}
7	1, 4, 6	3eqtri 2648	. 2 ⊢ {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤} = {𝑤 ∣ ∃𝑛(𝑛 ∈ (0..^(#‘𝑊)) ∧ (𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤))}
8		abid2 2745	. . . 4 ⊢ {𝑛 ∣ 𝑛 ∈ (0..^(#‘𝑊))} = (0..^(#‘𝑊))
9		ovex 6678	. . . 4 ⊢ (0..^(#‘𝑊)) ∈ V
10	8, 9	eqeltri 2697	. . 3 ⊢ {𝑛 ∣ 𝑛 ∈ (0..^(#‘𝑊))} ∈ V
11		tru 1487	. . . . 5 ⊢ ⊤
12	11, 11	pm3.2i 471	. . . 4 ⊢ (⊤ ∧ ⊤)
13		ovexd 6680	. . . . . 6 ⊢ (⊤ → (𝑊 cyclShift 𝑛) ∈ V)
14		eqtr3 2643	. . . . . . . . . . . . 13 ⊢ ((𝑤 = (𝑊 cyclShift 𝑛) ∧ 𝑦 = (𝑊 cyclShift 𝑛)) → 𝑤 = 𝑦)
15	14	ex 450	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝑊 cyclShift 𝑛) → (𝑦 = (𝑊 cyclShift 𝑛) → 𝑤 = 𝑦))
16	15	eqcoms 2630	. . . . . . . . . . 11 ⊢ ((𝑊 cyclShift 𝑛) = 𝑤 → (𝑦 = (𝑊 cyclShift 𝑛) → 𝑤 = 𝑦))
17	16	adantl 482	. . . . . . . . . 10 ⊢ ((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → (𝑦 = (𝑊 cyclShift 𝑛) → 𝑤 = 𝑦))
18	17	com12 32	. . . . . . . . 9 ⊢ (𝑦 = (𝑊 cyclShift 𝑛) → ((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → 𝑤 = 𝑦))
19	18	ad2antlr 763	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑦 = (𝑊 cyclShift 𝑛)) ∧ ⊤) → ((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → 𝑤 = 𝑦))
20	19	alrimiv 1855	. . . . . . 7 ⊢ (((⊤ ∧ 𝑦 = (𝑊 cyclShift 𝑛)) ∧ ⊤) → ∀𝑤((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → 𝑤 = 𝑦))
21	20	ex 450	. . . . . 6 ⊢ ((⊤ ∧ 𝑦 = (𝑊 cyclShift 𝑛)) → (⊤ → ∀𝑤((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → 𝑤 = 𝑦)))
22	13, 21	spcimedv 3292	. . . . 5 ⊢ (⊤ → (⊤ → ∃𝑦∀𝑤((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → 𝑤 = 𝑦)))
23	22	imp 445	. . . 4 ⊢ ((⊤ ∧ ⊤) → ∃𝑦∀𝑤((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → 𝑤 = 𝑦))
24	12, 23	mp1i 13	. . 3 ⊢ (𝑛 ∈ (0..^(#‘𝑊)) → ∃𝑦∀𝑤((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → 𝑤 = 𝑦))
25	10, 24	zfrep4 4779	. 2 ⊢ {𝑤 ∣ ∃𝑛(𝑛 ∈ (0..^(#‘𝑊)) ∧ (𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤))} ∈ V
26	7, 25	eqeltri 2697	1 ⊢ {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤} ∈ V

Syntax hints:   → wi 4   ∧ wa 384  ∀wal 1481   = wceq 1483  ⊤wtru 1484  ∃wex 1704   ∈ wcel 1990  {cab 2608  ∃wrex 2913  {crab 2916  Vcvv 3200  ‘cfv 5888  (class class class)co 6650  0cc0 9936  ..^cfzo 12465  #chash 13117  Word cword 13291   cyclShift ccsh 13534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-sn 4178  df-pr 4180  df-uni 4437  df-iota 5851  df-fv 5896  df-ov 6653

This theorem is referenced by: (None)