Step | Hyp | Ref
| Expression |
1 | | eqeq1 2614 |
. . . 4
⊢ (𝑦 = 𝑥 → (𝑦 = (𝑊 cyclShift 𝑛) ↔ 𝑥 = (𝑊 cyclShift 𝑛))) |
2 | 1 | rexbidv 3034 |
. . 3
⊢ (𝑦 = 𝑥 → (∃𝑛 ∈ (0...𝑁)𝑦 = (𝑊 cyclShift 𝑛) ↔ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑊 cyclShift 𝑛))) |
3 | 2 | cbvrabv 3172 |
. 2
⊢ {𝑦 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑊 cyclShift 𝑛)} = {𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑊 cyclShift 𝑛)} |
4 | | clwwlknprop 26300 |
. . . . . . . 8
⊢ (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) |
5 | 4 | simp2d 1067 |
. . . . . . 7
⊢ (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → 𝑤 ∈ Word 𝑉) |
6 | 5 | ad2antrl 760 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∧ ∃𝑛 ∈ (0...𝑁)𝑤 = (𝑊 cyclShift 𝑛))) → 𝑤 ∈ Word 𝑉) |
7 | | simprr 792 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∧ ∃𝑛 ∈ (0...𝑁)𝑤 = (𝑊 cyclShift 𝑛))) → ∃𝑛 ∈ (0...𝑁)𝑤 = (𝑊 cyclShift 𝑛)) |
8 | 6, 7 | jca 553 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∧ ∃𝑛 ∈ (0...𝑁)𝑤 = (𝑊 cyclShift 𝑛))) → (𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0...𝑁)𝑤 = (𝑊 cyclShift 𝑛))) |
9 | | simplr 788 |
. . . . . . . . . . . . 13
⊢ ((((𝑤 ∈ Word 𝑉 ∧ 𝑛 ∈ (0...𝑁)) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁))) ∧ 𝑤 = (𝑊 cyclShift 𝑛)) → (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁))) |
10 | | simpllr 795 |
. . . . . . . . . . . . 13
⊢ ((((𝑤 ∈ Word 𝑉 ∧ 𝑛 ∈ (0...𝑁)) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁))) ∧ 𝑤 = (𝑊 cyclShift 𝑛)) → 𝑛 ∈ (0...𝑁)) |
11 | | clwwnisshclwwn 26337 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → (𝑛 ∈ (0...𝑁) → (𝑊 cyclShift 𝑛) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁))) |
12 | 9, 10, 11 | sylc 63 |
. . . . . . . . . . . 12
⊢ ((((𝑤 ∈ Word 𝑉 ∧ 𝑛 ∈ (0...𝑁)) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁))) ∧ 𝑤 = (𝑊 cyclShift 𝑛)) → (𝑊 cyclShift 𝑛) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) |
13 | | eleq1 2676 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝑊 cyclShift 𝑛) → (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ (𝑊 cyclShift 𝑛) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁))) |
14 | 13 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝑤 ∈ Word 𝑉 ∧ 𝑛 ∈ (0...𝑁)) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁))) ∧ 𝑤 = (𝑊 cyclShift 𝑛)) → (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ (𝑊 cyclShift 𝑛) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁))) |
15 | 12, 14 | mpbird 246 |
. . . . . . . . . . 11
⊢ ((((𝑤 ∈ Word 𝑉 ∧ 𝑛 ∈ (0...𝑁)) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁))) ∧ 𝑤 = (𝑊 cyclShift 𝑛)) → 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) |
16 | 15 | exp31 628 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ Word 𝑉 ∧ 𝑛 ∈ (0...𝑁)) → ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → (𝑤 = (𝑊 cyclShift 𝑛) → 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)))) |
17 | 16 | com23 84 |
. . . . . . . . 9
⊢ ((𝑤 ∈ Word 𝑉 ∧ 𝑛 ∈ (0...𝑁)) → (𝑤 = (𝑊 cyclShift 𝑛) → ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)))) |
18 | 17 | rexlimdva 3013 |
. . . . . . . 8
⊢ (𝑤 ∈ Word 𝑉 → (∃𝑛 ∈ (0...𝑁)𝑤 = (𝑊 cyclShift 𝑛) → ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)))) |
19 | 18 | imp 444 |
. . . . . . 7
⊢ ((𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0...𝑁)𝑤 = (𝑊 cyclShift 𝑛)) → ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁))) |
20 | 19 | impcom 445 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ (𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0...𝑁)𝑤 = (𝑊 cyclShift 𝑛))) → 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) |
21 | | simprr 792 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ (𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0...𝑁)𝑤 = (𝑊 cyclShift 𝑛))) → ∃𝑛 ∈ (0...𝑁)𝑤 = (𝑊 cyclShift 𝑛)) |
22 | 20, 21 | jca 553 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ (𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0...𝑁)𝑤 = (𝑊 cyclShift 𝑛))) → (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∧ ∃𝑛 ∈ (0...𝑁)𝑤 = (𝑊 cyclShift 𝑛))) |
23 | 8, 22 | impbida 873 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → ((𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∧ ∃𝑛 ∈ (0...𝑁)𝑤 = (𝑊 cyclShift 𝑛)) ↔ (𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0...𝑁)𝑤 = (𝑊 cyclShift 𝑛)))) |
24 | | eqeq1 2614 |
. . . . . 6
⊢ (𝑥 = 𝑤 → (𝑥 = (𝑊 cyclShift 𝑛) ↔ 𝑤 = (𝑊 cyclShift 𝑛))) |
25 | 24 | rexbidv 3034 |
. . . . 5
⊢ (𝑥 = 𝑤 → (∃𝑛 ∈ (0...𝑁)𝑥 = (𝑊 cyclShift 𝑛) ↔ ∃𝑛 ∈ (0...𝑁)𝑤 = (𝑊 cyclShift 𝑛))) |
26 | 25 | elrab 3331 |
. . . 4
⊢ (𝑤 ∈ {𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑊 cyclShift 𝑛)} ↔ (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∧ ∃𝑛 ∈ (0...𝑁)𝑤 = (𝑊 cyclShift 𝑛))) |
27 | | eqeq1 2614 |
. . . . . 6
⊢ (𝑦 = 𝑤 → (𝑦 = (𝑊 cyclShift 𝑛) ↔ 𝑤 = (𝑊 cyclShift 𝑛))) |
28 | 27 | rexbidv 3034 |
. . . . 5
⊢ (𝑦 = 𝑤 → (∃𝑛 ∈ (0...𝑁)𝑦 = (𝑊 cyclShift 𝑛) ↔ ∃𝑛 ∈ (0...𝑁)𝑤 = (𝑊 cyclShift 𝑛))) |
29 | 28 | elrab 3331 |
. . . 4
⊢ (𝑤 ∈ {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑊 cyclShift 𝑛)} ↔ (𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0...𝑁)𝑤 = (𝑊 cyclShift 𝑛))) |
30 | 23, 26, 29 | 3bitr4g 302 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → (𝑤 ∈ {𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑊 cyclShift 𝑛)} ↔ 𝑤 ∈ {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑊 cyclShift 𝑛)})) |
31 | 30 | eqrdv 2608 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → {𝑥 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ ∃𝑛 ∈ (0...𝑁)𝑥 = (𝑊 cyclShift 𝑛)} = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑊 cyclShift 𝑛)}) |
32 | 3, 31 | syl5eq 2656 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → {𝑦 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑊 cyclShift 𝑛)} = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑊 cyclShift 𝑛)}) |