Proof of Theorem clwwlknimp
Step | Hyp | Ref
| Expression |
1 | | clwwlknprop 26300 |
. 2
⊢ (𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑊 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑊) = 𝑁))) |
2 | | simp1l 1078 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑊 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑊) = 𝑁)) → 𝑉 ∈ V) |
3 | | simp1r 1079 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑊 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑊) = 𝑁)) → 𝐸 ∈ V) |
4 | | simp3l 1082 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑊 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑊) = 𝑁)) → 𝑁 ∈
ℕ0) |
5 | | isclwwlkn 26297 |
. . . . 5
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ (𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ (𝑊 ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘𝑊) = 𝑁))) |
6 | 2, 3, 4, 5 | syl3anc 1318 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑊 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑊) = 𝑁)) → (𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ (𝑊 ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘𝑊) = 𝑁))) |
7 | | isclwwlk 26296 |
. . . . . 6
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑊 ∈ (𝑉 ClWWalks 𝐸) ↔ (𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸))) |
8 | 7 | 3ad2ant1 1075 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑊 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑊) = 𝑁)) → (𝑊 ∈ (𝑉 ClWWalks 𝐸) ↔ (𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸))) |
9 | 8 | anbi1d 737 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑊 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑊) = 𝑁)) → ((𝑊 ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘𝑊) = 𝑁) ↔ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸) ∧ (#‘𝑊) = 𝑁))) |
10 | 6, 9 | bitrd 267 |
. . 3
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑊 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑊) = 𝑁)) → (𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸) ∧ (#‘𝑊) = 𝑁))) |
11 | | simp1 1054 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸) → 𝑊 ∈ Word 𝑉) |
12 | 11 | anim1i 590 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸) ∧ (#‘𝑊) = 𝑁) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁)) |
13 | | oveq1 6556 |
. . . . . . . . 9
⊢
((#‘𝑊) = 𝑁 → ((#‘𝑊) − 1) = (𝑁 − 1)) |
14 | 13 | oveq2d 6565 |
. . . . . . . 8
⊢
((#‘𝑊) = 𝑁 → (0..^((#‘𝑊) − 1)) = (0..^(𝑁 − 1))) |
15 | 14 | raleqdv 3121 |
. . . . . . 7
⊢
((#‘𝑊) = 𝑁 → (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸)) |
16 | 15 | biimpcd 238 |
. . . . . 6
⊢
(∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 → ((#‘𝑊) = 𝑁 → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸)) |
17 | 16 | 3ad2ant2 1076 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸) → ((#‘𝑊) = 𝑁 → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸)) |
18 | 17 | imp 444 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸) ∧ (#‘𝑊) = 𝑁) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸) |
19 | | simpl3 1059 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸) ∧ (#‘𝑊) = 𝑁) → {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸) |
20 | 12, 18, 19 | 3jca 1235 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸) ∧ (#‘𝑊) = 𝑁) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸)) |
21 | 10, 20 | syl6bi 242 |
. 2
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑊 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑊) = 𝑁)) → (𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸))) |
22 | 1, 21 | mpcom 37 |
1
⊢ (𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸)) |