| Step | Hyp | Ref
| Expression |
|---|
| 1 | | clwwlknimp 26304 |
. . . 4
⊢ (𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) |
| 2 | | clwwlknprop 26300 |
. . . 4
⊢ (𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁))) |
| 3 | | df-3an 1033 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ) ↔ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈
ℕ)) |
| 4 | 3 | simplbi2 653 |
. . . . . . . . 9
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑁 ∈ ℕ → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈
ℕ))) |
| 5 | 4 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁)) → (𝑁 ∈ ℕ → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ))) |
| 6 | 5 | adantl 481 |
. . . . . . 7
⊢ ((((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁))) → (𝑁 ∈ ℕ → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ))) |
| 7 | 6 | imp 444 |
. . . . . 6
⊢
(((((𝑃 ∈ Word
𝑉 ∧ (#‘𝑃) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁))) ∧ 𝑁 ∈ ℕ) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ)) |
| 8 | | simpll1 1093 |
. . . . . 6
⊢
(((((𝑃 ∈ Word
𝑉 ∧ (#‘𝑃) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁))) ∧ 𝑁 ∈ ℕ) → (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) |
| 9 | | 3simpc 1053 |
. . . . . . 7
⊢ (((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) |
| 10 | 9 | ad2antrr 758 |
. . . . . 6
⊢
(((((𝑃 ∈ Word
𝑉 ∧ (#‘𝑃) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁))) ∧ 𝑁 ∈ ℕ) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) |
| 11 | 7, 8, 10 | 3jca 1235 |
. . . . 5
⊢
(((((𝑃 ∈ Word
𝑉 ∧ (#‘𝑃) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁))) ∧ 𝑁 ∈ ℕ) → ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸))) |
| 12 | 11 | ex 449 |
. . . 4
⊢ ((((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁))) → (𝑁 ∈ ℕ → ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)))) |
| 13 | 1, 2, 12 | syl2anc 691 |
. . 3
⊢ (𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → (𝑁 ∈ ℕ → ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)))) |
| 14 | 13 | impcom 445 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸))) |
| 15 | | eqid 2610 |
. . 3
⊢ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑤) = (𝑤‘0)} = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑤) = (𝑤‘0)} |
| 16 | 15 | clwwlkel 26321 |
. 2
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) → (𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑤) = (𝑤‘0)}) |
| 17 | 14, 16 | syl 17 |
1
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → (𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑤) = (𝑤‘0)}) |
