Step | Hyp | Ref
| Expression |
1 | | df-rab 2905 |
. . 3
⊢ {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤} = {𝑤 ∣ (𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤)} |
2 | | r19.42v 3073 |
. . . . 5
⊢
(∃𝑛 ∈
(0..^(#‘𝑊))(𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) ↔ (𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤)) |
3 | 2 | bicomi 213 |
. . . 4
⊢ ((𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤) ↔ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤)) |
4 | 3 | abbii 2726 |
. . 3
⊢ {𝑤 ∣ (𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤)} = {𝑤 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤)} |
5 | | df-rex 2902 |
. . . 4
⊢
(∃𝑛 ∈
(0..^(#‘𝑊))(𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) ↔ ∃𝑛(𝑛 ∈ (0..^(#‘𝑊)) ∧ (𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤))) |
6 | 5 | abbii 2726 |
. . 3
⊢ {𝑤 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤)} = {𝑤 ∣ ∃𝑛(𝑛 ∈ (0..^(#‘𝑊)) ∧ (𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤))} |
7 | 1, 4, 6 | 3eqtri 2636 |
. 2
⊢ {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤} = {𝑤 ∣ ∃𝑛(𝑛 ∈ (0..^(#‘𝑊)) ∧ (𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤))} |
8 | | abid2 2732 |
. . . 4
⊢ {𝑛 ∣ 𝑛 ∈ (0..^(#‘𝑊))} = (0..^(#‘𝑊)) |
9 | | ovex 6577 |
. . . 4
⊢
(0..^(#‘𝑊))
∈ V |
10 | 8, 9 | eqeltri 2684 |
. . 3
⊢ {𝑛 ∣ 𝑛 ∈ (0..^(#‘𝑊))} ∈ V |
11 | | tru 1479 |
. . . . 5
⊢
⊤ |
12 | 11, 11 | pm3.2i 470 |
. . . 4
⊢ (⊤
∧ ⊤) |
13 | | ovex 6577 |
. . . . . . 7
⊢ (𝑊 cyclShift 𝑛) ∈ V |
14 | 13 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (𝑊 cyclShift 𝑛) ∈ V) |
15 | | eqtr3 2631 |
. . . . . . . . . . . . 13
⊢ ((𝑤 = (𝑊 cyclShift 𝑛) ∧ 𝑦 = (𝑊 cyclShift 𝑛)) → 𝑤 = 𝑦) |
16 | 15 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝑤 = (𝑊 cyclShift 𝑛) → (𝑦 = (𝑊 cyclShift 𝑛) → 𝑤 = 𝑦)) |
17 | 16 | eqcoms 2618 |
. . . . . . . . . . 11
⊢ ((𝑊 cyclShift 𝑛) = 𝑤 → (𝑦 = (𝑊 cyclShift 𝑛) → 𝑤 = 𝑦)) |
18 | 17 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → (𝑦 = (𝑊 cyclShift 𝑛) → 𝑤 = 𝑦)) |
19 | 18 | com12 32 |
. . . . . . . . 9
⊢ (𝑦 = (𝑊 cyclShift 𝑛) → ((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → 𝑤 = 𝑦)) |
20 | 19 | ad2antlr 759 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑦
= (𝑊 cyclShift 𝑛)) ∧ ⊤) →
((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → 𝑤 = 𝑦)) |
21 | 20 | alrimiv 1842 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑦
= (𝑊 cyclShift 𝑛)) ∧ ⊤) →
∀𝑤((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → 𝑤 = 𝑦)) |
22 | 21 | ex 449 |
. . . . . 6
⊢
((⊤ ∧ 𝑦 =
(𝑊 cyclShift 𝑛)) → (⊤ →
∀𝑤((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → 𝑤 = 𝑦))) |
23 | 14, 22 | spcimedv 3265 |
. . . . 5
⊢ (⊤
→ (⊤ → ∃𝑦∀𝑤((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → 𝑤 = 𝑦))) |
24 | 23 | imp 444 |
. . . 4
⊢
((⊤ ∧ ⊤) → ∃𝑦∀𝑤((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → 𝑤 = 𝑦)) |
25 | 12, 24 | mp1i 13 |
. . 3
⊢ (𝑛 ∈ (0..^(#‘𝑊)) → ∃𝑦∀𝑤((𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤) → 𝑤 = 𝑦)) |
26 | 10, 25 | zfrep4 4707 |
. 2
⊢ {𝑤 ∣ ∃𝑛(𝑛 ∈ (0..^(#‘𝑊)) ∧ (𝑤 ∈ Word 𝑉 ∧ (𝑊 cyclShift 𝑛) = 𝑤))} ∈ V |
27 | 7, 26 | eqeltri 2684 |
1
⊢ {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤} ∈ V |