| Step | Hyp | Ref
| Expression |
|---|
| 1 | | df-wlk 26036 |
. . . 4
⊢ Walks =
(𝑣 ∈ V, 𝑒 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom 𝑒 ∧ 𝑝:(0...(#‘𝑓))⟶𝑣 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝑒‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) |
| 2 | 1 | brovmpt2ex 7236 |
. . 3
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
| 3 | | simpr1 1060 |
. . . . . . . . . . 11
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ Fun ◡𝑃) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) → 𝐹 ∈ Word dom 𝐸) |
| 4 | | df-f1 5809 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃:(0...(#‘𝐹))–1-1→𝑉 ↔ (𝑃:(0...(#‘𝐹))⟶𝑉 ∧ Fun ◡𝑃)) |
| 5 | | wlkdvspthlem 26137 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → Fun ◡𝐹) |
| 6 | 5 | 3exp 1256 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 ∈ Word dom 𝐸 → (𝑃:(0...(#‘𝐹))–1-1→𝑉 → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → Fun ◡𝐹))) |
| 7 | 6 | com3l 87 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃:(0...(#‘𝐹))–1-1→𝑉 → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝐹 ∈ Word dom 𝐸 → Fun ◡𝐹))) |
| 8 | 4, 7 | sylbir 224 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃:(0...(#‘𝐹))⟶𝑉 ∧ Fun ◡𝑃) → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝐹 ∈ Word dom 𝐸 → Fun ◡𝐹))) |
| 9 | 8 | expcom 450 |
. . . . . . . . . . . . . . . 16
⊢ (Fun
◡𝑃 → (𝑃:(0...(#‘𝐹))⟶𝑉 → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝐹 ∈ Word dom 𝐸 → Fun ◡𝐹)))) |
| 10 | 9 | com14 94 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Word dom 𝐸 → (𝑃:(0...(#‘𝐹))⟶𝑉 → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (Fun ◡𝑃 → Fun ◡𝐹)))) |
| 11 | 10 | 3imp 1249 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → (Fun ◡𝑃 → Fun ◡𝐹)) |
| 12 | 11 | com12 32 |
. . . . . . . . . . . . 13
⊢ (Fun
◡𝑃 → ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → Fun ◡𝐹)) |
| 13 | 12 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ Fun ◡𝑃) → ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → Fun ◡𝐹)) |
| 14 | 13 | imp 444 |
. . . . . . . . . . 11
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ Fun ◡𝑃) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) → Fun ◡𝐹) |
| 15 | 3, 14 | jca 553 |
. . . . . . . . . 10
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ Fun ◡𝑃) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) → (𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹)) |
| 16 | | simpr2 1061 |
. . . . . . . . . 10
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ Fun ◡𝑃) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) → 𝑃:(0...(#‘𝐹))⟶𝑉) |
| 17 | | simpr3 1062 |
. . . . . . . . . 10
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ Fun ◡𝑃) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) → ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) |
| 18 | 15, 16, 17 | 3jca 1235 |
. . . . . . . . 9
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ Fun ◡𝑃) ∧ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) → ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |
| 19 | 18 | ex 449 |
. . . . . . . 8
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ Fun ◡𝑃) → ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
| 20 | | iswlk 26048 |
. . . . . . . . 9
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Walks 𝐸)𝑃 ↔ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
| 21 | 20 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ Fun ◡𝑃) → (𝐹(𝑉 Walks 𝐸)𝑃 ↔ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
| 22 | | istrl 26067 |
. . . . . . . . 9
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Trails 𝐸)𝑃 ↔ ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
| 23 | 22 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ Fun ◡𝑃) → (𝐹(𝑉 Trails 𝐸)𝑃 ↔ ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
| 24 | 19, 21, 23 | 3imtr4d 282 |
. . . . . . 7
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ Fun ◡𝑃) → (𝐹(𝑉 Walks 𝐸)𝑃 → 𝐹(𝑉 Trails 𝐸)𝑃)) |
| 25 | | simpr 476 |
. . . . . . 7
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ Fun ◡𝑃) → Fun ◡𝑃) |
| 26 | 24, 25 | jctird 565 |
. . . . . 6
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ Fun ◡𝑃) → (𝐹(𝑉 Walks 𝐸)𝑃 → (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃))) |
| 27 | | isspth 26099 |
. . . . . . . 8
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 SPaths 𝐸)𝑃 ↔ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃))) |
| 28 | 27 | bicomd 212 |
. . . . . . 7
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃) ↔ 𝐹(𝑉 SPaths 𝐸)𝑃)) |
| 29 | 28 | adantr 480 |
. . . . . 6
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ Fun ◡𝑃) → ((𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃) ↔ 𝐹(𝑉 SPaths 𝐸)𝑃)) |
| 30 | 26, 29 | sylibd 228 |
. . . . 5
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ Fun ◡𝑃) → (𝐹(𝑉 Walks 𝐸)𝑃 → 𝐹(𝑉 SPaths 𝐸)𝑃)) |
| 31 | 30 | ex 449 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (Fun ◡𝑃 → (𝐹(𝑉 Walks 𝐸)𝑃 → 𝐹(𝑉 SPaths 𝐸)𝑃))) |
| 32 | 31 | com23 84 |
. . 3
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Walks 𝐸)𝑃 → (Fun ◡𝑃 → 𝐹(𝑉 SPaths 𝐸)𝑃))) |
| 33 | 2, 32 | mpcom 37 |
. 2
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → (Fun ◡𝑃 → 𝐹(𝑉 SPaths 𝐸)𝑃)) |
| 34 | 33 | imp 444 |
1
⊢ ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ Fun ◡𝑃) → 𝐹(𝑉 SPaths 𝐸)𝑃) |
