Metamath Proof Explorer

Theorem pthonpth

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

Ref Expression
Assertion pthonpth ⊢FPaths⁡GP→FP⁡0PathsOn⁡GP⁡FP

Proof

Step Hyp Ref Expression
1 pthistrl ⊢FPaths⁡GP→FTrails⁡GP
2 trlontrl ⊢FTrails⁡GP→FP⁡0TrailsOn⁡GP⁡FP
3 1 2 syl ⊢FPaths⁡GP→FP⁡0TrailsOn⁡GP⁡FP
4 id ⊢FPaths⁡GP→FPaths⁡GP
5 pthiswlk ⊢FPaths⁡GP→FWalks⁡GP
6 eqid ⊢Vtx⁡G=Vtx⁡G
7 6 wlkepvtx ⊢FWalks⁡GP→P⁡0∈Vtx⁡G∧P⁡F∈Vtx⁡G
8 wlkv ⊢FWalks⁡GP→G∈V∧F∈V∧P∈V
9 3simpc ⊢G∈V∧F∈V∧P∈V→F∈V∧P∈V
10 8 9 syl ⊢FWalks⁡GP→F∈V∧P∈V
11 7 10 jca ⊢FWalks⁡GP→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→FP⁡0PathsOn⁡GP⁡FP↔FP⁡0TrailsOn⁡GP⁡FP∧FPaths⁡GP
13 5 11 12 3syl ⊢FPaths⁡GP→FP⁡0PathsOn⁡GP⁡FP↔FP⁡0TrailsOn⁡GP⁡FP∧FPaths⁡GP
14 3 4 13 mpbir2and ⊢FPaths⁡GP→FP⁡0PathsOn⁡GP⁡FP