Step | Hyp | Ref
| Expression |
1 | | wlkonprop 26063 |
. . . 4
⊢ (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵))) |
2 | | simplr 788 |
. . . . . 6
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) |
3 | | iswlk 26048 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Walks 𝐸)𝑃 ↔ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
4 | 3 | 3adant3 1074 |
. . . . . . . . . . . . . . 15
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐹(𝑉 Walks 𝐸)𝑃 ↔ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
5 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹 ∈ Word dom 𝐸 → 𝐹 ∈ Word dom 𝐸) |
6 | 5 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → 𝐹 ∈ Word dom 𝐸) |
7 | 6 | ad4antlr 765 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ ((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → 𝐹 ∈ Word dom 𝐸) |
8 | | usgraf1 25889 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑉 USGrph 𝐸 → 𝐸:dom 𝐸–1-1→ran 𝐸) |
9 | 8 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵) → 𝐸:dom 𝐸–1-1→ran 𝐸) |
10 | 9 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ ((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → 𝐸:dom 𝐸–1-1→ran 𝐸) |
11 | | simp2 1055 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵) → (#‘𝐹) = 2) |
12 | 11 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ ((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → (#‘𝐹) = 2) |
13 | 7, 10, 12 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ ((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → (𝐹 ∈ Word dom 𝐸 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸 ∧ (#‘𝐹) = 2)) |
14 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → (𝑃‘0) = 𝐴) |
15 | 14 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ ((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → (𝑃‘0) = 𝐴) |
16 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → (𝑃‘(#‘𝐹)) = 𝐵) |
17 | 16 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ ((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → (𝑃‘(#‘𝐹)) = 𝐵) |
18 | | simp3 1056 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵) → 𝐴 ≠ 𝐵) |
19 | 18 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ ((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → 𝐴 ≠ 𝐵) |
20 | 15, 17, 19 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ ((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → ((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵)) |
21 | | simp3 1056 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) |
22 | 21 | ad4antlr 765 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ ((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) |
23 | 20, 22 | jca 553 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ ((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → (((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
24 | | usgra2wlkspthlem1 26147 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸 ∧ (#‘𝐹) = 2) → ((((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → Fun ◡𝐹)) |
25 | 13, 23, 24 | sylc 63 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ ((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → Fun ◡𝐹) |
26 | 7, 25 | jca 553 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ ((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → (𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹)) |
27 | | simp2 1055 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → 𝑃:(0...(#‘𝐹))⟶𝑉) |
28 | 27 | ad4antlr 765 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ ((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → 𝑃:(0...(#‘𝐹))⟶𝑉) |
29 | 26, 28, 22 | 3jca 1235 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ ((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
30 | 29 | exp31 628 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ ((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) → (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 → ((𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵) → ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})))) |
31 | 30 | exp31 628 |
. . . . . . . . . . . . . . 15
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 → ((𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵) → ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})))))) |
32 | 4, 31 | sylbid 229 |
. . . . . . . . . . . . . 14
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐹(𝑉 Walks 𝐸)𝑃 → (((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 → ((𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵) → ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})))))) |
33 | 32 | com13 86 |
. . . . . . . . . . . . 13
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → (𝐹(𝑉 Walks 𝐸)𝑃 → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 → ((𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵) → ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})))))) |
34 | 33 | ex 449 |
. . . . . . . . . . . 12
⊢ ((𝑃‘0) = 𝐴 → ((𝑃‘(#‘𝐹)) = 𝐵 → (𝐹(𝑉 Walks 𝐸)𝑃 → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 → ((𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵) → ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))))))) |
35 | 34 | com3r 85 |
. . . . . . . . . . 11
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → ((𝑃‘0) = 𝐴 → ((𝑃‘(#‘𝐹)) = 𝐵 → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 → ((𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵) → ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))))))) |
36 | 35 | 3imp 1249 |
. . . . . . . . . 10
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 → ((𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵) → ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))))) |
37 | 36 | impcom 445 |
. . . . . . . . 9
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) → (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 → ((𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵) → ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})))) |
38 | 37 | imp31 447 |
. . . . . . . 8
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
39 | | id 22 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
40 | 39 | 3adant3 1074 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
41 | 40 | ad3antrrr 762 |
. . . . . . . . 9
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
42 | | istrl 26067 |
. . . . . . . . 9
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Trails 𝐸)𝑃 ↔ ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
43 | 41, 42 | syl 17 |
. . . . . . . 8
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → (𝐹(𝑉 Trails 𝐸)𝑃 ↔ ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
44 | 38, 43 | mpbird 246 |
. . . . . . 7
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → 𝐹(𝑉 Trails 𝐸)𝑃) |
45 | | 2mwlk 26049 |
. . . . . . . . . . . . 13
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉)) |
46 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → 𝐹 ∈ Word dom 𝐸) |
47 | 45, 46 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → 𝐹 ∈ Word dom 𝐸) |
48 | 47 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → 𝐹 ∈ Word dom 𝐸) |
49 | 48 | ad3antlr 763 |
. . . . . . . . . 10
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → 𝐹 ∈ Word dom 𝐸) |
50 | 11 | adantl 481 |
. . . . . . . . . 10
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → (#‘𝐹) = 2) |
51 | 49, 50 | jca 553 |
. . . . . . . . 9
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → (𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2)) |
52 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑉 USGrph 𝐸 → 𝑉 USGrph 𝐸) |
53 | 52 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵) → 𝑉 USGrph 𝐸) |
54 | 53 | adantl 481 |
. . . . . . . . . 10
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → 𝑉 USGrph 𝐸) |
55 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → 𝑃:(0...(#‘𝐹))⟶𝑉) |
56 | 45, 55 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → 𝑃:(0...(#‘𝐹))⟶𝑉) |
57 | 56 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → 𝑃:(0...(#‘𝐹))⟶𝑉) |
58 | 57 | ad3antlr 763 |
. . . . . . . . . 10
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → 𝑃:(0...(#‘𝐹))⟶𝑉) |
59 | 54, 58 | jca 553 |
. . . . . . . . 9
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → (𝑉 USGrph 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉)) |
60 | 51, 59 | jca 553 |
. . . . . . . 8
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → ((𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2) ∧ (𝑉 USGrph 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉))) |
61 | | simp2 1055 |
. . . . . . . . . . 11
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → (𝑃‘0) = 𝐴) |
62 | 61 | ad3antlr 763 |
. . . . . . . . . 10
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → (𝑃‘0) = 𝐴) |
63 | | simp3 1056 |
. . . . . . . . . . 11
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → (𝑃‘(#‘𝐹)) = 𝐵) |
64 | 63 | ad3antlr 763 |
. . . . . . . . . 10
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → (𝑃‘(#‘𝐹)) = 𝐵) |
65 | 18 | adantl 481 |
. . . . . . . . . 10
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → 𝐴 ≠ 𝐵) |
66 | 62, 64, 65 | 3jca 1235 |
. . . . . . . . 9
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → ((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵)) |
67 | 4, 21 | syl6bi 242 |
. . . . . . . . . . . . 13
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐹(𝑉 Walks 𝐸)𝑃 → ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
68 | 67 | com12 32 |
. . . . . . . . . . . 12
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
69 | 68 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
70 | 69 | impcom 445 |
. . . . . . . . . 10
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) → ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) |
71 | 70 | ad2antrr 758 |
. . . . . . . . 9
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) |
72 | 66, 71 | jca 553 |
. . . . . . . 8
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → (((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
73 | | usgra2wlkspthlem2 26148 |
. . . . . . . 8
⊢ (((𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2) ∧ (𝑉 USGrph 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉)) → ((((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → Fun ◡𝑃)) |
74 | 60, 72, 73 | sylc 63 |
. . . . . . 7
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → Fun ◡𝑃) |
75 | | isspth 26099 |
. . . . . . . 8
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 SPaths 𝐸)𝑃 ↔ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃))) |
76 | 41, 75 | syl 17 |
. . . . . . 7
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → (𝐹(𝑉 SPaths 𝐸)𝑃 ↔ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃))) |
77 | 44, 74, 76 | mpbir2and 959 |
. . . . . 6
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → 𝐹(𝑉 SPaths 𝐸)𝑃) |
78 | | isspthon 26113 |
. . . . . . 7
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐹(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑃 ↔ (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 ∧ 𝐹(𝑉 SPaths 𝐸)𝑃))) |
79 | 78 | ad3antrrr 762 |
. . . . . 6
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → (𝐹(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑃 ↔ (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 ∧ 𝐹(𝑉 SPaths 𝐸)𝑃))) |
80 | 2, 77, 79 | mpbir2and 959 |
. . . . 5
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) ∧ (𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵)) → 𝐹(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑃) |
81 | 80 | exp31 628 |
. . . 4
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) → (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 → ((𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵) → 𝐹(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑃))) |
82 | 1, 81 | mpcom 37 |
. . 3
⊢ (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 → ((𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵) → 𝐹(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑃)) |
83 | 82 | com12 32 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵) → (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 → 𝐹(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑃)) |
84 | | spthonprp 26115 |
. . 3
⊢ (𝐹(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑃 → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 ∧ 𝐹(𝑉 SPaths 𝐸)𝑃))) |
85 | | simpl 472 |
. . . 4
⊢ ((𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 ∧ 𝐹(𝑉 SPaths 𝐸)𝑃) → 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) |
86 | 85 | adantl 481 |
. . 3
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 ∧ 𝐹(𝑉 SPaths 𝐸)𝑃)) → 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) |
87 | 84, 86 | syl 17 |
. 2
⊢ (𝐹(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑃 → 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) |
88 | 83, 87 | impbid1 214 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵) → (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 ↔ 𝐹(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑃)) |