MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cshwsexa Structured version   Visualization version   GIF version

Theorem cshwsexa 13364
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.
StepHypRef Expression
1 df-rab 2901 . . 3 {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤} = {𝑤 ∣ (𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤)}
2 r19.42v 3069 . . . . 5 (∃𝑛 ∈ (0..^(#‘𝑊))(𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) ↔ (𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤))
32bicomi 212 . . . 4 ((𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤) ↔ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤))
43abbii 2722 . . 3 {𝑤 ∣ (𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤)} = {𝑤 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤)}
5 df-rex 2898 . . . 4 (∃𝑛 ∈ (0..^(#‘𝑊))(𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) ↔ ∃𝑛(𝑛 ∈ (0..^(#‘𝑊)) ∧ (𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤)))
65abbii 2722 . . 3 {𝑤 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤)} = {𝑤 ∣ ∃𝑛(𝑛 ∈ (0..^(#‘𝑊)) ∧ (𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤))}
71, 4, 63eqtri 2632 . 2 {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤} = {𝑤 ∣ ∃𝑛(𝑛 ∈ (0..^(#‘𝑊)) ∧ (𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤))}
8 abid2 2728 . . . 4 {𝑛𝑛 ∈ (0..^(#‘𝑊))} = (0..^(#‘𝑊))
9 ovex 6552 . . . 4 (0..^(#‘𝑊)) ∈ V
108, 9eqeltri 2680 . . 3 {𝑛𝑛 ∈ (0..^(#‘𝑊))} ∈ V
11 tru 1478 . . . . 5
1211, 11pm3.2i 469 . . . 4 (⊤ ∧ ⊤)
13 ovex 6552 . . . . . . 7 (𝑊 cyclShift 𝑛) ∈ V
1413a1i 11 . . . . . 6 (⊤ → (𝑊 cyclShift 𝑛) ∈ V)
15 eqtr3 2627 . . . . . . . . . . . . 13 ((𝑤 = (𝑊 cyclShift 𝑛) ∧ 𝑦 = (𝑊 cyclShift 𝑛)) → 𝑤 = 𝑦)
1615ex 448 . . . . . . . . . . . 12 (𝑤 = (𝑊 cyclShift 𝑛) → (𝑦 = (𝑊 cyclShift 𝑛) → 𝑤 = 𝑦))
1716eqcoms 2614 . . . . . . . . . . 11 ((𝑊 cyclShift 𝑛) = 𝑤 → (𝑦 = (𝑊 cyclShift 𝑛) → 𝑤 = 𝑦))
1817adantl 480 . . . . . . . . . 10 ((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → (𝑦 = (𝑊 cyclShift 𝑛) → 𝑤 = 𝑦))
1918com12 32 . . . . . . . . 9 (𝑦 = (𝑊 cyclShift 𝑛) → ((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → 𝑤 = 𝑦))
2019ad2antlr 758 . . . . . . . 8 (((⊤ ∧ 𝑦 = (𝑊 cyclShift 𝑛)) ∧ ⊤) → ((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → 𝑤 = 𝑦))
2120alrimiv 1841 . . . . . . 7 (((⊤ ∧ 𝑦 = (𝑊 cyclShift 𝑛)) ∧ ⊤) → ∀𝑤((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → 𝑤 = 𝑦))
2221ex 448 . . . . . 6 ((⊤ ∧ 𝑦 = (𝑊 cyclShift 𝑛)) → (⊤ → ∀𝑤((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → 𝑤 = 𝑦)))
2314, 22spcimedv 3261 . . . . 5 (⊤ → (⊤ → ∃𝑦𝑤((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → 𝑤 = 𝑦)))
2423imp 443 . . . 4 ((⊤ ∧ ⊤) → ∃𝑦𝑤((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → 𝑤 = 𝑦))
2512, 24mp1i 13 . . 3 (𝑛 ∈ (0..^(#‘𝑊)) → ∃𝑦𝑤((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → 𝑤 = 𝑦))
2610, 25zfrep4 4698 . 2 {𝑤 ∣ ∃𝑛(𝑛 ∈ (0..^(#‘𝑊)) ∧ (𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤))} ∈ V
277, 26eqeltri 2680 1 {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤} ∈ V
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wal 1472   = wceq 1474  wtru 1475  wex 1694  wcel 1976  {cab 2592  wrex 2893  {crab 2896  Vcvv 3169  cfv 5787  (class class class)co 6524  0cc0 9789  ..^cfzo 12286  #chash 12931  Word cword 13089   cyclShift ccsh 13328
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-rep 4690  ax-nul 4709
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ral 2897  df-rex 2898  df-rab 2901  df-v 3171  df-sbc 3399  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-sn 4122  df-pr 4124  df-uni 4364  df-iota 5751  df-fv 5795  df-ov 6527
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator