Step | Hyp | Ref
| Expression |
1 | | pthsfval 40927 |
. . . . 5
⊢ (𝐺 ∈ V →
(PathS‘𝐺) =
{〈𝑥, 𝑦〉 ∣ (𝑥(TrailS‘𝐺)𝑦 ∧ Fun ◡(𝑦 ↾ (1..^(#‘𝑥))) ∧ ((𝑦 “ {0, (#‘𝑥)}) ∩ (𝑦 “ (1..^(#‘𝑥)))) = ∅)}) |
2 | 1 | brfvopab 6598 |
. . . 4
⊢ (𝐹(PathS‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) |
3 | | isPth 40929 |
. . . . 5
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(PathS‘𝐺)𝑃 ↔ (𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅))) |
4 | | simplll 794 |
. . . . . . 7
⊢ ((((𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → 𝐹(TrailS‘𝐺)𝑃) |
5 | | trlis1wlk 40905 |
. . . . . . . . . 10
⊢ (𝐹(TrailS‘𝐺)𝑃 → 𝐹(1Walks‘𝐺)𝑃) |
6 | | 1wlkcl 40820 |
. . . . . . . . . 10
⊢ (𝐹(1Walks‘𝐺)𝑃 → (#‘𝐹) ∈
ℕ0) |
7 | 5, 6 | syl 17 |
. . . . . . . . 9
⊢ (𝐹(TrailS‘𝐺)𝑃 → (#‘𝐹) ∈
ℕ0) |
8 | 7 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (#‘𝐹) ∈
ℕ0) |
9 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
10 | 9 | 1wlkp 40821 |
. . . . . . . . . . 11
⊢ (𝐹(1Walks‘𝐺)𝑃 → 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) |
11 | 5, 10 | syl 17 |
. . . . . . . . . 10
⊢ (𝐹(TrailS‘𝐺)𝑃 → 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) |
12 | 11 | ad3antrrr 762 |
. . . . . . . . 9
⊢ ((((𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) |
13 | | simpllr 795 |
. . . . . . . . 9
⊢ ((((𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) |
14 | | simpr 476 |
. . . . . . . . 9
⊢ ((((𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) |
15 | 12, 13, 14 | 3jca 1235 |
. . . . . . . 8
⊢ ((((𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹)))) |
16 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) → ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) |
17 | 16 | adantr 480 |
. . . . . . . 8
⊢ ((((𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) |
18 | | injresinj 12451 |
. . . . . . . 8
⊢
((#‘𝐹) ∈
ℕ0 → ((𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ → Fun ◡𝑃))) |
19 | 8, 15, 17, 18 | syl3c 64 |
. . . . . . 7
⊢ ((((𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → Fun ◡𝑃) |
20 | 4, 19 | jca 553 |
. . . . . 6
⊢ ((((𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡𝑃)) |
21 | 20 | ex3 1255 |
. . . . 5
⊢ ((𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) → ((𝑃‘0) ≠ (𝑃‘(#‘𝐹)) → (𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡𝑃))) |
22 | 3, 21 | syl6bi 242 |
. . . 4
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(PathS‘𝐺)𝑃 → ((𝑃‘0) ≠ (𝑃‘(#‘𝐹)) → (𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡𝑃)))) |
23 | 2, 22 | mpcom 37 |
. . 3
⊢ (𝐹(PathS‘𝐺)𝑃 → ((𝑃‘0) ≠ (𝑃‘(#‘𝐹)) → (𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡𝑃))) |
24 | 23 | imp 444 |
. 2
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡𝑃)) |
25 | 2 | adantr 480 |
. . 3
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) |
26 | | issPth 40930 |
. . 3
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(SPathS‘𝐺)𝑃 ↔ (𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡𝑃))) |
27 | 25, 26 | syl 17 |
. 2
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → (𝐹(SPathS‘𝐺)𝑃 ↔ (𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡𝑃))) |
28 | 24, 27 | mpbird 246 |
1
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → 𝐹(SPathS‘𝐺)𝑃) |