Metamath Proof Explorer

Theorem trlontrl

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

Ref Expression
Assertion trlontrl ⊢ F Trails ⁡ G P → F P ⁡ 0 TrailsOn ⁡ G P ⁡ F P

Proof

Step Hyp Ref Expression
1 trliswlk ⊢ F Trails ⁡ G P → F Walks ⁡ G P
2 wlkonwlk ⊢ F Walks ⁡ G P → F P ⁡ 0 WalksOn ⁡ G P ⁡ F P
3 1 2 syl ⊢ F Trails ⁡ G P → F P ⁡ 0 WalksOn ⁡ G P ⁡ F P
4 id ⊢ F Trails ⁡ G P → F Trails ⁡ G P
5 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
6 5 wlkepvtx ⊢ F Walks ⁡ G P → P ⁡ 0 ∈ Vtx ⁡ G ∧ P ⁡ F ∈ Vtx ⁡ G
7 wlkv ⊢ F Walks ⁡ G P → G ∈ V ∧ F ∈ V ∧ P ∈ V
8 3simpc ⊢ G ∈ V ∧ F ∈ V ∧ P ∈ V → F ∈ V ∧ P ∈ V
9 8 anim2i ⊢ P ⁡ 0 ∈ Vtx ⁡ G ∧ P ⁡ F ∈ Vtx ⁡ G ∧ G ∈ V ∧ F ∈ V ∧ P ∈ V → P ⁡ 0 ∈ Vtx ⁡ G ∧ P ⁡ F ∈ Vtx ⁡ G ∧ F ∈ V ∧ P ∈ V
10 6 7 9 syl2anc ⊢ F Walks ⁡ G P → P ⁡ 0 ∈ Vtx ⁡ G ∧ P ⁡ F ∈ Vtx ⁡ G ∧ F ∈ V ∧ P ∈ V
11 1 10 syl ⊢ F Trails ⁡ G P → P ⁡ 0 ∈ Vtx ⁡ G ∧ P ⁡ F ∈ Vtx ⁡ G ∧ F ∈ V ∧ P ∈ V
12 5 istrlson ⊢ P ⁡ 0 ∈ Vtx ⁡ G ∧ P ⁡ F ∈ Vtx ⁡ G ∧ F ∈ V ∧ P ∈ V → F P ⁡ 0 TrailsOn ⁡ G P ⁡ F P ↔ F P ⁡ 0 WalksOn ⁡ G P ⁡ F P ∧ F Trails ⁡ G P
13 11 12 syl ⊢ F Trails ⁡ G P → F P ⁡ 0 TrailsOn ⁡ G P ⁡ F P ↔ F P ⁡ 0 WalksOn ⁡ G P ⁡ F P ∧ F Trails ⁡ G P
14 3 4 13 mpbir2and ⊢ F Trails ⁡ G P → F P ⁡ 0 TrailsOn ⁡ G P ⁡ F P