Metamath Proof Explorer


Theorem pthdepisspth

Description: A path with different start and end points is a simple path (in an undirected graph). (Contributed by Alexander van der Vekens, 31-Oct-2017) (Revised by AV, 12-Jan-2021) (Proof shortened by AV, 30-Oct-2021)

Ref Expression
Assertion pthdepisspth F Paths G P P 0 P F F SPaths G P

Proof

Step Hyp Ref Expression
1 ispth F Paths G P F Trails G P Fun P 1 ..^ F -1 P 0 F P 1 ..^ F =
2 simplll F Trails G P Fun P 1 ..^ F -1 P 0 F P 1 ..^ F = P 0 P F F Trails G P
3 trliswlk F Trails G P F Walks G P
4 wlkcl F Walks G P F 0
5 3 4 syl F Trails G P F 0
6 5 ad3antrrr F Trails G P Fun P 1 ..^ F -1 P 0 F P 1 ..^ F = P 0 P F F 0
7 eqid Vtx G = Vtx G
8 7 wlkp F Walks G P P : 0 F Vtx G
9 3 8 syl F Trails G P P : 0 F Vtx G
10 9 ad3antrrr F Trails G P Fun P 1 ..^ F -1 P 0 F P 1 ..^ F = P 0 P F P : 0 F Vtx G
11 simpllr F Trails G P Fun P 1 ..^ F -1 P 0 F P 1 ..^ F = P 0 P F Fun P 1 ..^ F -1
12 simpr F Trails G P Fun P 1 ..^ F -1 P 0 F P 1 ..^ F = P 0 P F P 0 P F
13 10 11 12 3jca F Trails G P Fun P 1 ..^ F -1 P 0 F P 1 ..^ F = P 0 P F P : 0 F Vtx G Fun P 1 ..^ F -1 P 0 P F
14 simplr F Trails G P Fun P 1 ..^ F -1 P 0 F P 1 ..^ F = P 0 P F P 0 F P 1 ..^ F =
15 injresinj F 0 P : 0 F Vtx G Fun P 1 ..^ F -1 P 0 P F P 0 F P 1 ..^ F = Fun P -1
16 6 13 14 15 syl3c F Trails G P Fun P 1 ..^ F -1 P 0 F P 1 ..^ F = P 0 P F Fun P -1
17 2 16 jca F Trails G P Fun P 1 ..^ F -1 P 0 F P 1 ..^ F = P 0 P F F Trails G P Fun P -1
18 17 ex3 F Trails G P Fun P 1 ..^ F -1 P 0 F P 1 ..^ F = P 0 P F F Trails G P Fun P -1
19 1 18 sylbi F Paths G P P 0 P F F Trails G P Fun P -1
20 19 imp F Paths G P P 0 P F F Trails G P Fun P -1
21 isspth F SPaths G P F Trails G P Fun P -1
22 20 21 sylibr F Paths G P P 0 P F F SPaths G P