Proof of Theorem wlklniswwlkn1
Step | Hyp | Ref
| Expression |
1 | | wlkbprop 26051 |
. . . 4
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → ((#‘𝐹) ∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
2 | 1 | adantr 480 |
. . 3
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 𝑁) → ((#‘𝐹) ∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
3 | | wlkiswwlk1 26218 |
. . . . . . . . 9
⊢ (𝑉 USGrph 𝐸 → (𝐹(𝑉 Walks 𝐸)𝑃 → 𝑃 ∈ (𝑉 WWalks 𝐸))) |
4 | 3 | com12 32 |
. . . . . . . 8
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → (𝑉 USGrph 𝐸 → 𝑃 ∈ (𝑉 WWalks 𝐸))) |
5 | 4 | adantr 480 |
. . . . . . 7
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 𝑁) → (𝑉 USGrph 𝐸 → 𝑃 ∈ (𝑉 WWalks 𝐸))) |
6 | 5 | adantl 481 |
. . . . . 6
⊢
((((#‘𝐹)
∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 𝑁)) → (𝑉 USGrph 𝐸 → 𝑃 ∈ (𝑉 WWalks 𝐸))) |
7 | 6 | imp 444 |
. . . . 5
⊢
(((((#‘𝐹)
∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 𝑁)) ∧ 𝑉 USGrph 𝐸) → 𝑃 ∈ (𝑉 WWalks 𝐸)) |
8 | | 2mwlk 26049 |
. . . . . . . . . 10
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉)) |
9 | | ffn 5958 |
. . . . . . . . . . . 12
⊢ (𝑃:(0...(#‘𝐹))⟶𝑉 → 𝑃 Fn (0...(#‘𝐹))) |
10 | | hashfn 13025 |
. . . . . . . . . . . 12
⊢ (𝑃 Fn (0...(#‘𝐹)) → (#‘𝑃) = (#‘(0...(#‘𝐹)))) |
11 | | hashfz0 13079 |
. . . . . . . . . . . . . 14
⊢
((#‘𝐹) ∈
ℕ0 → (#‘(0...(#‘𝐹))) = ((#‘𝐹) + 1)) |
12 | 11 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) →
(#‘(0...(#‘𝐹)))
= ((#‘𝐹) +
1)) |
13 | | eqeq1 2614 |
. . . . . . . . . . . . . 14
⊢
((#‘(0...(#‘𝐹))) = (#‘𝑃) → ((#‘(0...(#‘𝐹))) = ((#‘𝐹) + 1) ↔ (#‘𝑃) = ((#‘𝐹) + 1))) |
14 | 13 | eqcoms 2618 |
. . . . . . . . . . . . 13
⊢
((#‘𝑃) =
(#‘(0...(#‘𝐹)))
→ ((#‘(0...(#‘𝐹))) = ((#‘𝐹) + 1) ↔ (#‘𝑃) = ((#‘𝐹) + 1))) |
15 | 12, 14 | syl5ib 233 |
. . . . . . . . . . . 12
⊢
((#‘𝑃) =
(#‘(0...(#‘𝐹)))
→ (((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (#‘𝑃) = ((#‘𝐹) + 1))) |
16 | 9, 10, 15 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝑃:(0...(#‘𝐹))⟶𝑉 → (((#‘𝐹) ∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) →
(#‘𝑃) =
((#‘𝐹) +
1))) |
17 | 16 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → (((#‘𝐹) ∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) →
(#‘𝑃) =
((#‘𝐹) +
1))) |
18 | 8, 17 | syl 17 |
. . . . . . . . 9
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → (((#‘𝐹) ∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) →
(#‘𝑃) =
((#‘𝐹) +
1))) |
19 | 18 | adantr 480 |
. . . . . . . 8
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 𝑁) → (((#‘𝐹) ∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) →
(#‘𝑃) =
((#‘𝐹) +
1))) |
20 | | oveq1 6556 |
. . . . . . . . . 10
⊢
((#‘𝐹) = 𝑁 → ((#‘𝐹) + 1) = (𝑁 + 1)) |
21 | 20 | eqeq2d 2620 |
. . . . . . . . 9
⊢
((#‘𝐹) = 𝑁 → ((#‘𝑃) = ((#‘𝐹) + 1) ↔ (#‘𝑃) = (𝑁 + 1))) |
22 | 21 | adantl 481 |
. . . . . . . 8
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 𝑁) → ((#‘𝑃) = ((#‘𝐹) + 1) ↔ (#‘𝑃) = (𝑁 + 1))) |
23 | 19, 22 | sylibd 228 |
. . . . . . 7
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 𝑁) → (((#‘𝐹) ∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) →
(#‘𝑃) = (𝑁 + 1))) |
24 | 23 | impcom 445 |
. . . . . 6
⊢
((((#‘𝐹)
∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 𝑁)) → (#‘𝑃) = (𝑁 + 1)) |
25 | 24 | adantr 480 |
. . . . 5
⊢
(((((#‘𝐹)
∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 𝑁)) ∧ 𝑉 USGrph 𝐸) → (#‘𝑃) = (𝑁 + 1)) |
26 | | simpl2l 1107 |
. . . . . . . 8
⊢
((((#‘𝐹)
∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 𝑁)) → 𝑉 ∈ V) |
27 | | simpl2r 1108 |
. . . . . . . 8
⊢
((((#‘𝐹)
∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 𝑁)) → 𝐸 ∈ V) |
28 | | eleq1 2676 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) = 𝑁 → ((#‘𝐹) ∈ ℕ0
↔ 𝑁 ∈
ℕ0)) |
29 | 28 | biimpcd 238 |
. . . . . . . . . . . 12
⊢
((#‘𝐹) ∈
ℕ0 → ((#‘𝐹) = 𝑁 → 𝑁 ∈
ℕ0)) |
30 | 29 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((#‘𝐹) = 𝑁 → 𝑁 ∈
ℕ0)) |
31 | 30 | com12 32 |
. . . . . . . . . 10
⊢
((#‘𝐹) = 𝑁 → (((#‘𝐹) ∈ ℕ0
∧ (𝑉 ∈ V ∧
𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → 𝑁 ∈
ℕ0)) |
32 | 31 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 𝑁) → (((#‘𝐹) ∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → 𝑁 ∈
ℕ0)) |
33 | 32 | impcom 445 |
. . . . . . . 8
⊢
((((#‘𝐹)
∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 𝑁)) → 𝑁 ∈
ℕ0) |
34 | 26, 27, 33 | 3jca 1235 |
. . . . . . 7
⊢
((((#‘𝐹)
∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 𝑁)) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈
ℕ0)) |
35 | 34 | adantr 480 |
. . . . . 6
⊢
(((((#‘𝐹)
∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 𝑁)) ∧ 𝑉 USGrph 𝐸) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈
ℕ0)) |
36 | | iswwlkn 26212 |
. . . . . 6
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ (𝑃 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ↔ (𝑃 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑃) = (𝑁 + 1)))) |
37 | 35, 36 | syl 17 |
. . . . 5
⊢
(((((#‘𝐹)
∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 𝑁)) ∧ 𝑉 USGrph 𝐸) → (𝑃 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ↔ (𝑃 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑃) = (𝑁 + 1)))) |
38 | 7, 25, 37 | mpbir2and 959 |
. . . 4
⊢
(((((#‘𝐹)
∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 𝑁)) ∧ 𝑉 USGrph 𝐸) → 𝑃 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) |
39 | 38 | ex 449 |
. . 3
⊢
((((#‘𝐹)
∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 𝑁)) → (𝑉 USGrph 𝐸 → 𝑃 ∈ ((𝑉 WWalksN 𝐸)‘𝑁))) |
40 | 2, 39 | mpancom 700 |
. 2
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 𝑁) → (𝑉 USGrph 𝐸 → 𝑃 ∈ ((𝑉 WWalksN 𝐸)‘𝑁))) |
41 | 40 | com12 32 |
1
⊢ (𝑉 USGrph 𝐸 → ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 𝑁) → 𝑃 ∈ ((𝑉 WWalksN 𝐸)‘𝑁))) |