Metamath Proof Explorer


Theorem isspthonpth

Description: A pair of functions is a simple path between two given vertices iff it is a simple path starting and ending at the two vertices. (Contributed by Alexander van der Vekens, 9-Mar-2018) (Revised by AV, 17-Jan-2021)

Ref Expression
Hypothesis isspthonpth.v V = Vtx G
Assertion isspthonpth A V B V F W P Z F A SPathsOn G B P F SPaths G P P 0 = A P F = B

Proof

Step Hyp Ref Expression
1 isspthonpth.v V = Vtx G
2 1 isspthson A V B V F W P Z F A SPathsOn G B P F A TrailsOn G B P F SPaths G P
3 1 istrlson A V B V F W P Z F A TrailsOn G B P F A WalksOn G B P F Trails G P
4 3 adantr A V B V F W P Z F SPaths G P F A TrailsOn G B P F A WalksOn G B P F Trails G P
5 spthispth F SPaths G P F Paths G P
6 pthistrl F Paths G P F Trails G P
7 5 6 syl F SPaths G P F Trails G P
8 7 adantl A V B V F W P Z F SPaths G P F Trails G P
9 8 biantrud A V B V F W P Z F SPaths G P F A WalksOn G B P F A WalksOn G B P F Trails G P
10 spthiswlk F SPaths G P F Walks G P
11 10 adantl A V B V F W P Z F SPaths G P F Walks G P
12 1 iswlkon A V B V F W P Z F A WalksOn G B P F Walks G P P 0 = A P F = B
13 3anass F Walks G P P 0 = A P F = B F Walks G P P 0 = A P F = B
14 12 13 bitrdi A V B V F W P Z F A WalksOn G B P F Walks G P P 0 = A P F = B
15 14 adantr A V B V F W P Z F SPaths G P F A WalksOn G B P F Walks G P P 0 = A P F = B
16 11 15 mpbirand A V B V F W P Z F SPaths G P F A WalksOn G B P P 0 = A P F = B
17 4 9 16 3bitr2d A V B V F W P Z F SPaths G P F A TrailsOn G B P P 0 = A P F = B
18 17 ex A V B V F W P Z F SPaths G P F A TrailsOn G B P P 0 = A P F = B
19 18 pm5.32rd A V B V F W P Z F A TrailsOn G B P F SPaths G P P 0 = A P F = B F SPaths G P
20 3anass F SPaths G P P 0 = A P F = B F SPaths G P P 0 = A P F = B
21 ancom F SPaths G P P 0 = A P F = B P 0 = A P F = B F SPaths G P
22 20 21 bitr2i P 0 = A P F = B F SPaths G P F SPaths G P P 0 = A P F = B
23 19 22 bitrdi A V B V F W P Z F A TrailsOn G B P F SPaths G P F SPaths G P P 0 = A P F = B
24 2 23 bitrd A V B V F W P Z F A SPathsOn G B P F SPaths G P P 0 = A P F = B