Step | Hyp | Ref
| Expression |
1 | | wlkbprop 26051 |
. . 3
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → ((#‘𝐹) ∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
2 | | wlkn0 26055 |
. . . . 5
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → 𝑃 ≠ ∅) |
3 | | iswlk 26048 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Walks 𝐸)𝑃 ↔ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
4 | | simprl 790 |
. . . . . . . . . 10
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ (𝑃 ≠ ∅ ∧ 𝑉 USGrph 𝐸)) → 𝑃 ≠ ∅) |
5 | | ffz0iswrd 13187 |
. . . . . . . . . . . . 13
⊢ (𝑃:(0...(#‘𝐹))⟶𝑉 → 𝑃 ∈ Word 𝑉) |
6 | 5 | 3ad2ant2 1076 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → 𝑃 ∈ Word 𝑉) |
7 | 6 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → 𝑃 ∈ Word 𝑉) |
8 | 7 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ (𝑃 ≠ ∅ ∧ 𝑉 USGrph 𝐸)) → 𝑃 ∈ Word 𝑉) |
9 | | lencl 13179 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹 ∈ Word dom 𝐸 → (#‘𝐹) ∈
ℕ0) |
10 | | ffz0hash 13088 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → (#‘𝑃) = ((#‘𝐹) + 1)) |
11 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝐹) ∈
ℕ0 → (#‘𝐹) ∈ ℂ) |
12 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 ∈
ℂ |
13 | | pncan 10166 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((#‘𝐹) ∈
ℂ ∧ 1 ∈ ℂ) → (((#‘𝐹) + 1) − 1) = (#‘𝐹)) |
14 | 13 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((#‘𝐹) ∈
ℂ ∧ 1 ∈ ℂ) → (#‘𝐹) = (((#‘𝐹) + 1) − 1)) |
15 | 11, 12, 14 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝐹) ∈
ℕ0 → (#‘𝐹) = (((#‘𝐹) + 1) − 1)) |
16 | 15 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → (#‘𝐹) = (((#‘𝐹) + 1) − 1)) |
17 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((#‘𝐹) + 1) =
(#‘𝑃) →
(((#‘𝐹) + 1) −
1) = ((#‘𝑃) −
1)) |
18 | 17 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝑃) =
((#‘𝐹) + 1) →
(((#‘𝐹) + 1) −
1) = ((#‘𝑃) −
1)) |
19 | 18 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑃) =
((#‘𝐹) + 1) →
((#‘𝐹) =
(((#‘𝐹) + 1) −
1) ↔ (#‘𝐹) =
((#‘𝑃) −
1))) |
20 | 16, 19 | syl5ib 233 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑃) =
((#‘𝐹) + 1) →
(((#‘𝐹) ∈
ℕ0 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → (#‘𝐹) = ((#‘𝑃) − 1))) |
21 | 10, 20 | mpcom 37 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → (#‘𝐹) = ((#‘𝑃) − 1)) |
22 | 9, 21 | sylan 487 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → (#‘𝐹) = ((#‘𝑃) − 1)) |
23 | 22 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (𝑃 ≠ ∅ ∧ 𝑉 USGrph 𝐸)) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) → (#‘𝐹) = ((#‘𝑃) − 1)) |
24 | 23 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (𝑃 ≠ ∅ ∧ 𝑉 USGrph 𝐸)) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) → (0..^(#‘𝐹)) = (0..^((#‘𝑃) − 1))) |
25 | 24 | raleqdv 3121 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (𝑃 ≠ ∅ ∧ 𝑉 USGrph 𝐸)) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) → (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ∀𝑖 ∈ (0..^((#‘𝑃) − 1))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
26 | | usgrafun 25878 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑉 USGrph 𝐸 → Fun 𝐸) |
27 | 26 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃 ≠ ∅ ∧ 𝑉 USGrph 𝐸) → Fun 𝐸) |
28 | 27 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐹 ∈ Word
dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (𝑃 ≠ ∅ ∧ 𝑉 USGrph 𝐸)) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → Fun 𝐸) |
29 | | wrdf 13165 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐹 ∈ Word dom 𝐸 → 𝐹:(0..^(#‘𝐹))⟶dom 𝐸) |
30 | | simplll 794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ (#‘𝐹) ∈ ℕ0) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → 𝐹:(0..^(#‘𝐹))⟶dom 𝐸) |
31 | 21 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → ((#‘𝑃) − 1) = (#‘𝐹)) |
32 | 31 | adantll 746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ (#‘𝐹) ∈ ℕ0) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → ((#‘𝑃) − 1) = (#‘𝐹)) |
33 | 32 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ (#‘𝐹) ∈ ℕ0) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → (0..^((#‘𝑃) − 1)) = (0..^(#‘𝐹))) |
34 | 33 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ (#‘𝐹) ∈ ℕ0) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → (𝑖 ∈ (0..^((#‘𝑃) − 1)) ↔ 𝑖 ∈ (0..^(#‘𝐹)))) |
35 | 34 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ (#‘𝐹) ∈ ℕ0) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → 𝑖 ∈ (0..^(#‘𝐹))) |
36 | 30, 35 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ (#‘𝐹) ∈ ℕ0) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝐹‘𝑖) ∈ dom 𝐸) |
37 | 36 | exp31 628 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ (#‘𝐹) ∈ ℕ0) → (𝑃:(0...(#‘𝐹))⟶𝑉 → (𝑖 ∈ (0..^((#‘𝑃) − 1)) → (𝐹‘𝑖) ∈ dom 𝐸))) |
38 | 29, 9, 37 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐹 ∈ Word dom 𝐸 → (𝑃:(0...(#‘𝐹))⟶𝑉 → (𝑖 ∈ (0..^((#‘𝑃) − 1)) → (𝐹‘𝑖) ∈ dom 𝐸))) |
39 | 38 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → (𝑖 ∈ (0..^((#‘𝑃) − 1)) → (𝐹‘𝑖) ∈ dom 𝐸)) |
40 | 39 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (𝑃 ≠ ∅ ∧ 𝑉 USGrph 𝐸)) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) → (𝑖 ∈ (0..^((#‘𝑃) − 1)) → (𝐹‘𝑖) ∈ dom 𝐸)) |
41 | 40 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐹 ∈ Word
dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (𝑃 ≠ ∅ ∧ 𝑉 USGrph 𝐸)) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝐹‘𝑖) ∈ dom 𝐸) |
42 | 28, 41 | jca 553 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐹 ∈ Word
dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (𝑃 ≠ ∅ ∧ 𝑉 USGrph 𝐸)) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → (Fun 𝐸 ∧ (𝐹‘𝑖) ∈ dom 𝐸)) |
43 | 42 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐹 ∈ Word
dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (𝑃 ≠ ∅ ∧ 𝑉 USGrph 𝐸)) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) ∧ (𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (Fun 𝐸 ∧ (𝐹‘𝑖) ∈ dom 𝐸)) |
44 | | fvelrn 6260 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((Fun
𝐸 ∧ (𝐹‘𝑖) ∈ dom 𝐸) → (𝐸‘(𝐹‘𝑖)) ∈ ran 𝐸) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐹 ∈ Word
dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (𝑃 ≠ ∅ ∧ 𝑉 USGrph 𝐸)) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) ∧ (𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (𝐸‘(𝐹‘𝑖)) ∈ ran 𝐸) |
46 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = (𝐸‘(𝐹‘𝑖)) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ↔ (𝐸‘(𝐹‘𝑖)) ∈ ran 𝐸)) |
47 | 46 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ↔ (𝐸‘(𝐹‘𝑖)) ∈ ran 𝐸)) |
48 | 47 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐹 ∈ Word
dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (𝑃 ≠ ∅ ∧ 𝑉 USGrph 𝐸)) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) ∧ (𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ↔ (𝐸‘(𝐹‘𝑖)) ∈ ran 𝐸)) |
49 | 45, 48 | mpbird 246 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐹 ∈ Word
dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (𝑃 ≠ ∅ ∧ 𝑉 USGrph 𝐸)) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) ∧ (𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) |
50 | 49 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐹 ∈ Word
dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (𝑃 ≠ ∅ ∧ 𝑉 USGrph 𝐸)) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → ((𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
51 | 50 | ralimdva 2945 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (𝑃 ≠ ∅ ∧ 𝑉 USGrph 𝐸)) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
52 | 25, 51 | sylbid 229 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (𝑃 ≠ ∅ ∧ 𝑉 USGrph 𝐸)) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) → (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
53 | 52 | exp31 628 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → ((𝑃 ≠ ∅ ∧ 𝑉 USGrph 𝐸) → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)))) |
54 | 53 | com24 93 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((𝑃 ≠ ∅ ∧ 𝑉 USGrph 𝐸) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)))) |
55 | 54 | 3impia 1253 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((𝑃 ≠ ∅ ∧ 𝑉 USGrph 𝐸) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸))) |
56 | 55 | impcom 445 |
. . . . . . . . . . 11
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → ((𝑃 ≠ ∅ ∧ 𝑉 USGrph 𝐸) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
57 | 56 | imp 444 |
. . . . . . . . . 10
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ (𝑃 ≠ ∅ ∧ 𝑉 USGrph 𝐸)) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) |
58 | 4, 8, 57 | 3jca 1235 |
. . . . . . . . 9
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ (𝑃 ≠ ∅ ∧ 𝑉 USGrph 𝐸)) → (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
59 | 58 | ex 449 |
. . . . . . . 8
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → ((𝑃 ≠ ∅ ∧ 𝑉 USGrph 𝐸) → (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸))) |
60 | | iswwlk 26211 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑃 ∈ (𝑉 WWalks 𝐸) ↔ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸))) |
61 | 60 | bicomd 212 |
. . . . . . . . 9
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) ↔ 𝑃 ∈ (𝑉 WWalks 𝐸))) |
62 | 61 | ad2antrr 758 |
. . . . . . . 8
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → ((𝑃 ≠ ∅ ∧ 𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) ↔ 𝑃 ∈ (𝑉 WWalks 𝐸))) |
63 | 59, 62 | sylibd 228 |
. . . . . . 7
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → ((𝑃 ≠ ∅ ∧ 𝑉 USGrph 𝐸) → 𝑃 ∈ (𝑉 WWalks 𝐸))) |
64 | 63 | exp4b 630 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (𝑃 ≠ ∅ → (𝑉 USGrph 𝐸 → 𝑃 ∈ (𝑉 WWalks 𝐸))))) |
65 | 3, 64 | sylbid 229 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Walks 𝐸)𝑃 → (𝑃 ≠ ∅ → (𝑉 USGrph 𝐸 → 𝑃 ∈ (𝑉 WWalks 𝐸))))) |
66 | 2, 65 | mpdi 44 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Walks 𝐸)𝑃 → (𝑉 USGrph 𝐸 → 𝑃 ∈ (𝑉 WWalks 𝐸)))) |
67 | 66 | 3adant1 1072 |
. . 3
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Walks 𝐸)𝑃 → (𝑉 USGrph 𝐸 → 𝑃 ∈ (𝑉 WWalks 𝐸)))) |
68 | 1, 67 | mpcom 37 |
. 2
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → (𝑉 USGrph 𝐸 → 𝑃 ∈ (𝑉 WWalks 𝐸))) |
69 | 68 | com12 32 |
1
⊢ (𝑉 USGrph 𝐸 → (𝐹(𝑉 Walks 𝐸)𝑃 → 𝑃 ∈ (𝑉 WWalks 𝐸))) |