Step | Hyp | Ref
| Expression |
1 | | df-pth 26038 |
. . . . 5
⊢ Paths =
(𝑣 ∈ V, 𝑒 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑣 Trails 𝑒)𝑝 ∧ Fun ◡(𝑝 ↾ (1..^(#‘𝑓))) ∧ ((𝑝 “ {0, (#‘𝑓)}) ∩ (𝑝 “ (1..^(#‘𝑓)))) = ∅)}) |
2 | 1 | brovmpt2ex 7236 |
. . . 4
⊢ (𝐹(𝑉 Paths 𝐸)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
3 | | ispth 26098 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Paths 𝐸)𝑃 ↔ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅))) |
4 | | simp-4l 802 |
. . . . . . . . 9
⊢
(((((𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → 𝐹(𝑉 Trails 𝐸)𝑃) |
5 | | trliswlk 26069 |
. . . . . . . . . . . 12
⊢ (𝐹(𝑉 Trails 𝐸)𝑃 → 𝐹(𝑉 Walks 𝐸)𝑃) |
6 | | 2mwlk 26049 |
. . . . . . . . . . . 12
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉)) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐹(𝑉 Trails 𝐸)𝑃 → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉)) |
8 | | lencl 13179 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Word dom 𝐸 → (#‘𝐹) ∈
ℕ0) |
9 | 8 | ad5antr 766 |
. . . . . . . . . . . . 13
⊢
((((((𝐹 ∈ Word
dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (#‘𝐹) ∈
ℕ0) |
10 | | simp-5r 805 |
. . . . . . . . . . . . . 14
⊢
((((((𝐹 ∈ Word
dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → 𝑃:(0...(#‘𝐹))⟶𝑉) |
11 | | simp-4r 803 |
. . . . . . . . . . . . . 14
⊢
((((((𝐹 ∈ Word
dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) |
12 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢
((((((𝐹 ∈ Word
dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) |
13 | 10, 11, 12 | 3jca 1235 |
. . . . . . . . . . . . 13
⊢
((((((𝐹 ∈ Word
dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (𝑃:(0...(#‘𝐹))⟶𝑉 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹)))) |
14 | | simpllr 795 |
. . . . . . . . . . . . 13
⊢
((((((𝐹 ∈ Word
dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) |
15 | | injresinj 12451 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) ∈
ℕ0 → ((𝑃:(0...(#‘𝐹))⟶𝑉 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ → Fun ◡𝑃))) |
16 | 9, 13, 14, 15 | syl3c 64 |
. . . . . . . . . . . 12
⊢
((((((𝐹 ∈ Word
dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → Fun ◡𝑃) |
17 | 16 | exp31 628 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((𝑃‘0) ≠ (𝑃‘(#‘𝐹)) → Fun ◡𝑃))) |
18 | 7, 17 | sylanl1 680 |
. . . . . . . . . 10
⊢ (((𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((𝑃‘0) ≠ (𝑃‘(#‘𝐹)) → Fun ◡𝑃))) |
19 | 18 | imp31 447 |
. . . . . . . . 9
⊢
(((((𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → Fun ◡𝑃) |
20 | 4, 19 | jca 553 |
. . . . . . . 8
⊢
(((((𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃)) |
21 | 20 | exp31 628 |
. . . . . . 7
⊢ (((𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((𝑃‘0) ≠ (𝑃‘(#‘𝐹)) → (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃)))) |
22 | 21 | 3impa 1251 |
. . . . . 6
⊢ ((𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((𝑃‘0) ≠ (𝑃‘(#‘𝐹)) → (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃)))) |
23 | 22 | com12 32 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) → ((𝑃‘0) ≠ (𝑃‘(#‘𝐹)) → (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃)))) |
24 | 3, 23 | sylbid 229 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Paths 𝐸)𝑃 → ((𝑃‘0) ≠ (𝑃‘(#‘𝐹)) → (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃)))) |
25 | 2, 24 | mpcom 37 |
. . 3
⊢ (𝐹(𝑉 Paths 𝐸)𝑃 → ((𝑃‘0) ≠ (𝑃‘(#‘𝐹)) → (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃))) |
26 | 25 | imp 444 |
. 2
⊢ ((𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃)) |
27 | 2 | adantr 480 |
. . 3
⊢ ((𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
28 | | isspth 26099 |
. . 3
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 SPaths 𝐸)𝑃 ↔ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃))) |
29 | 27, 28 | syl 17 |
. 2
⊢ ((𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (𝐹(𝑉 SPaths 𝐸)𝑃 ↔ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃))) |
30 | 26, 29 | mpbird 246 |
1
⊢ ((𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → 𝐹(𝑉 SPaths 𝐸)𝑃) |