Proof of Theorem usgrwlknloop
Step | Hyp | Ref
| Expression |
1 | | wlkbprop 26051 |
. . 3
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → ((#‘𝐹) ∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
2 | | iswlk 26048 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Walks 𝐸)𝑃 ↔ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
3 | 2 | 3adant1 1072 |
. . . 4
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Walks 𝐸)𝑃 ↔ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
4 | | wrdf 13165 |
. . . . . . . . 9
⊢ (𝐹 ∈ Word dom 𝐸 → 𝐹:(0..^(#‘𝐹))⟶dom 𝐸) |
5 | | ffvelrn 6265 |
. . . . . . . . . . . 12
⊢ ((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ 𝑘 ∈ (0..^(#‘𝐹))) → (𝐹‘𝑘) ∈ dom 𝐸) |
6 | | usgrafun 25878 |
. . . . . . . . . . . . 13
⊢ (𝑉 USGrph 𝐸 → Fun 𝐸) |
7 | | fvelrn 6260 |
. . . . . . . . . . . . . . . 16
⊢ ((Fun
𝐸 ∧ (𝐹‘𝑘) ∈ dom 𝐸) → (𝐸‘(𝐹‘𝑘)) ∈ ran 𝐸) |
8 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → ((𝐸‘(𝐹‘𝑘)) ∈ ran 𝐸 ↔ {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ ran 𝐸)) |
9 | 8 | anbi2d 736 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → ((𝑉 USGrph 𝐸 ∧ (𝐸‘(𝐹‘𝑘)) ∈ ran 𝐸) ↔ (𝑉 USGrph 𝐸 ∧ {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ ran 𝐸))) |
10 | 9 | biimpd 218 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → ((𝑉 USGrph 𝐸 ∧ (𝐸‘(𝐹‘𝑘)) ∈ ran 𝐸) → (𝑉 USGrph 𝐸 ∧ {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ ran 𝐸))) |
11 | | usgraedgrn 25910 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑉 USGrph 𝐸 ∧ {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ ran 𝐸) → (𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1))) |
12 | 10, 11 | syl6com 36 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐸‘(𝐹‘𝑘)) ∈ ran 𝐸) → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)))) |
13 | 12 | expcom 450 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐸‘(𝐹‘𝑘)) ∈ ran 𝐸 → (𝑉 USGrph 𝐸 → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1))))) |
14 | 7, 13 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((Fun
𝐸 ∧ (𝐹‘𝑘) ∈ dom 𝐸) → (𝑉 USGrph 𝐸 → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1))))) |
15 | 14 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (Fun
𝐸 → ((𝐹‘𝑘) ∈ dom 𝐸 → (𝑉 USGrph 𝐸 → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)))))) |
16 | 15 | com23 84 |
. . . . . . . . . . . . 13
⊢ (Fun
𝐸 → (𝑉 USGrph 𝐸 → ((𝐹‘𝑘) ∈ dom 𝐸 → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)))))) |
17 | 6, 16 | mpcom 37 |
. . . . . . . . . . . 12
⊢ (𝑉 USGrph 𝐸 → ((𝐹‘𝑘) ∈ dom 𝐸 → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1))))) |
18 | 5, 17 | syl5com 31 |
. . . . . . . . . . 11
⊢ ((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ 𝑘 ∈ (0..^(#‘𝐹))) → (𝑉 USGrph 𝐸 → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1))))) |
19 | 18 | ex 449 |
. . . . . . . . . 10
⊢ (𝐹:(0..^(#‘𝐹))⟶dom 𝐸 → (𝑘 ∈ (0..^(#‘𝐹)) → (𝑉 USGrph 𝐸 → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)))))) |
20 | 19 | com23 84 |
. . . . . . . . 9
⊢ (𝐹:(0..^(#‘𝐹))⟶dom 𝐸 → (𝑉 USGrph 𝐸 → (𝑘 ∈ (0..^(#‘𝐹)) → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)))))) |
21 | 4, 20 | syl 17 |
. . . . . . . 8
⊢ (𝐹 ∈ Word dom 𝐸 → (𝑉 USGrph 𝐸 → (𝑘 ∈ (0..^(#‘𝐹)) → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)))))) |
22 | 21 | imp31 447 |
. . . . . . 7
⊢ (((𝐹 ∈ Word dom 𝐸 ∧ 𝑉 USGrph 𝐸) ∧ 𝑘 ∈ (0..^(#‘𝐹))) → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)))) |
23 | 22 | ralimdva 2945 |
. . . . . 6
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑉 USGrph 𝐸) → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → ∀𝑘 ∈ (0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)))) |
24 | 23 | impancom 455 |
. . . . 5
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → (𝑉 USGrph 𝐸 → ∀𝑘 ∈ (0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)))) |
25 | 24 | 3adant2 1073 |
. . . 4
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → (𝑉 USGrph 𝐸 → ∀𝑘 ∈ (0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)))) |
26 | 3, 25 | syl6bi 242 |
. . 3
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Walks 𝐸)𝑃 → (𝑉 USGrph 𝐸 → ∀𝑘 ∈ (0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1))))) |
27 | 1, 26 | mpcom 37 |
. 2
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → (𝑉 USGrph 𝐸 → ∀𝑘 ∈ (0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)))) |
28 | 27 | impcom 445 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝐹(𝑉 Walks 𝐸)𝑃) → ∀𝑘 ∈ (0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1))) |