Metamath Proof Explorer

Theorem pthonpth

Description: A path is a path between its endpoints. (Contributed by AV, 31-Jan-2021)

Ref Expression
Assertion pthonpth ⊢ F Paths ⁡ G P → F P ⁡ 0 PathsOn ⁡ G P ⁡ F P

Proof

Step Hyp Ref Expression
1 pthistrl ⊢ F Paths ⁡ G P → F Trails ⁡ G P
2 trlontrl ⊢ F Trails ⁡ G P → F P ⁡ 0 TrailsOn ⁡ G P ⁡ F P
3 1 2 syl ⊢ F Paths ⁡ G P → F P ⁡ 0 TrailsOn ⁡ G P ⁡ F P
4 id ⊢ F Paths ⁡ G P → F Paths ⁡ G P
5 pthiswlk ⊢ F Paths ⁡ G P → F Walks ⁡ G P
6 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
7 6 wlkepvtx ⊢ F Walks ⁡ G P → P ⁡ 0 ∈ Vtx ⁡ G ∧ P ⁡ F ∈ Vtx ⁡ G
8 wlkv ⊢ F Walks ⁡ G P → G ∈ V ∧ F ∈ V ∧ P ∈ V
9 3simpc ⊢ G ∈ V ∧ F ∈ V ∧ P ∈ V → F ∈ V ∧ P ∈ V
10 8 9 syl ⊢ F Walks ⁡ G P → F ∈ V ∧ P ∈ V
11 7 10 jca ⊢ F Walks ⁡ G P → P ⁡ 0 ∈ Vtx ⁡ G ∧ P ⁡ F ∈ Vtx ⁡ G ∧ F ∈ V ∧ P ∈ V
12 6 ispthson ⊢ P ⁡ 0 ∈ Vtx ⁡ G ∧ P ⁡ F ∈ Vtx ⁡ G ∧ F ∈ V ∧ P ∈ V → F P ⁡ 0 PathsOn ⁡ G P ⁡ F P ↔ F P ⁡ 0 TrailsOn ⁡ G P ⁡ F P ∧ F Paths ⁡ G P
13 5 11 12 3syl ⊢ F Paths ⁡ G P → F P ⁡ 0 PathsOn ⁡ G P ⁡ F P ↔ F P ⁡ 0 TrailsOn ⁡ G P ⁡ F P ∧ F Paths ⁡ G P
14 3 4 13 mpbir2and ⊢ F Paths ⁡ G P → F P ⁡ 0 PathsOn ⁡ G P ⁡ F P