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

Theorem cshwsexa 13421
 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 2905 . . 3 {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤} = {𝑤 ∣ (𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤)}
2 r19.42v 3073 . . . . 5 (∃𝑛 ∈ (0..^(#‘𝑊))(𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) ↔ (𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤))
32bicomi 213 . . . 4 ((𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤) ↔ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤))
43abbii 2726 . . 3 {𝑤 ∣ (𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤)} = {𝑤 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤)}
5 df-rex 2902 . . . 4 (∃𝑛 ∈ (0..^(#‘𝑊))(𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) ↔ ∃𝑛(𝑛 ∈ (0..^(#‘𝑊)) ∧ (𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤)))
65abbii 2726 . . 3 {𝑤 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤)} = {𝑤 ∣ ∃𝑛(𝑛 ∈ (0..^(#‘𝑊)) ∧ (𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤))}
71, 4, 63eqtri 2636 . 2 {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤} = {𝑤 ∣ ∃𝑛(𝑛 ∈ (0..^(#‘𝑊)) ∧ (𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤))}
8 abid2 2732 . . . 4 {𝑛𝑛 ∈ (0..^(#‘𝑊))} = (0..^(#‘𝑊))
9 ovex 6577 . . . 4 (0..^(#‘𝑊)) ∈ V
108, 9eqeltri 2684 . . 3 {𝑛𝑛 ∈ (0..^(#‘𝑊))} ∈ V
11 tru 1479 . . . . 5
1211, 11pm3.2i 470 . . . 4 (⊤ ∧ ⊤)
13 ovex 6577 . . . . . . 7 (𝑊 cyclShift 𝑛) ∈ V
1413a1i 11 . . . . . 6 (⊤ → (𝑊 cyclShift 𝑛) ∈ V)
15 eqtr3 2631 . . . . . . . . . . . . 13 ((𝑤 = (𝑊 cyclShift 𝑛) ∧ 𝑦 = (𝑊 cyclShift 𝑛)) → 𝑤 = 𝑦)
1615ex 449 . . . . . . . . . . . 12 (𝑤 = (𝑊 cyclShift 𝑛) → (𝑦 = (𝑊 cyclShift 𝑛) → 𝑤 = 𝑦))
1716eqcoms 2618 . . . . . . . . . . 11 ((𝑊 cyclShift 𝑛) = 𝑤 → (𝑦 = (𝑊 cyclShift 𝑛) → 𝑤 = 𝑦))
1817adantl 481 . . . . . . . . . 10 ((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → (𝑦 = (𝑊 cyclShift 𝑛) → 𝑤 = 𝑦))
1918com12 32 . . . . . . . . 9 (𝑦 = (𝑊 cyclShift 𝑛) → ((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → 𝑤 = 𝑦))
2019ad2antlr 759 . . . . . . . 8 (((⊤ ∧ 𝑦 = (𝑊 cyclShift 𝑛)) ∧ ⊤) → ((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → 𝑤 = 𝑦))
2120alrimiv 1842 . . . . . . 7 (((⊤ ∧ 𝑦 = (𝑊 cyclShift 𝑛)) ∧ ⊤) → ∀𝑤((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → 𝑤 = 𝑦))
2221ex 449 . . . . . 6 ((⊤ ∧ 𝑦 = (𝑊 cyclShift 𝑛)) → (⊤ → ∀𝑤((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → 𝑤 = 𝑦)))
2314, 22spcimedv 3265 . . . . 5 (⊤ → (⊤ → ∃𝑦𝑤((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → 𝑤 = 𝑦)))
2423imp 444 . . . 4 ((⊤ ∧ ⊤) → ∃𝑦𝑤((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → 𝑤 = 𝑦))
2512, 24mp1i 13 . . 3 (𝑛 ∈ (0..^(#‘𝑊)) → ∃𝑦𝑤((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → 𝑤 = 𝑦))
2610, 25zfrep4 4707 . 2 {𝑤 ∣ ∃𝑛(𝑛 ∈ (0..^(#‘𝑊)) ∧ (𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤))} ∈ V
277, 26eqeltri 2684 1 {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤} ∈ V
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383  ∀wal 1473   = wceq 1475  ⊤wtru 1476  ∃wex 1695   ∈ wcel 1977  {cab 2596  ∃wrex 2897  {crab 2900  Vcvv 3173  ‘cfv 5804  (class class class)co 6549  0cc0 9815  ..^cfzo 12334  #chash 12979  Word cword 13146   cyclShift ccsh 13385 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-nul 4717 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-sn 4126  df-pr 4128  df-uni 4373  df-iota 5768  df-fv 5812  df-ov 6552 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator