| Step |
Hyp |
Ref |
Expression |
| 1 |
|
pthistrl |
⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) |
| 2 |
|
trlontrl |
⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → 𝐹 ( ( 𝑃 ‘ 0 ) ( TrailsOn ‘ 𝐺 ) ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) 𝑃 ) |
| 3 |
1 2
|
syl |
⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → 𝐹 ( ( 𝑃 ‘ 0 ) ( TrailsOn ‘ 𝐺 ) ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) 𝑃 ) |
| 4 |
|
id |
⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) |
| 5 |
|
pthiswlk |
⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) |
| 6 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
| 7 |
6
|
wlkepvtx |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( Vtx ‘ 𝐺 ) ) ) |
| 8 |
|
wlkv |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) |
| 9 |
|
3simpc |
⊢ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) |
| 10 |
8 9
|
syl |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) |
| 11 |
7 10
|
jca |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) |
| 12 |
6
|
ispthson |
⊢ ( ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( 𝐹 ( ( 𝑃 ‘ 0 ) ( PathsOn ‘ 𝐺 ) ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) 𝑃 ↔ ( 𝐹 ( ( 𝑃 ‘ 0 ) ( TrailsOn ‘ 𝐺 ) ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) 𝑃 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ) ) |
| 13 |
5 11 12
|
3syl |
⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( 𝐹 ( ( 𝑃 ‘ 0 ) ( PathsOn ‘ 𝐺 ) ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) 𝑃 ↔ ( 𝐹 ( ( 𝑃 ‘ 0 ) ( TrailsOn ‘ 𝐺 ) ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) 𝑃 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ) ) |
| 14 |
3 4 13
|
mpbir2and |
⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → 𝐹 ( ( 𝑃 ‘ 0 ) ( PathsOn ‘ 𝐺 ) ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) 𝑃 ) |