Metamath Proof Explorer


Theorem spthispth

Description: A simple path is a path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017) (Revised by AV, 9-Jan-2021) (Proof shortened by AV, 30-Oct-2021)

Ref Expression
Assertion spthispth F SPaths G P F Paths G P

Proof

Step Hyp Ref Expression
1 simpl F Trails G P Fun P -1 F Trails G P
2 funres11 Fun P -1 Fun P 1 ..^ F -1
3 2 adantl F Trails G P Fun P -1 Fun P 1 ..^ F -1
4 imain Fun P -1 P 0 F 1 ..^ F = P 0 F P 1 ..^ F
5 1e0p1 1 = 0 + 1
6 5 oveq1i 1 ..^ F = 0 + 1 ..^ F
7 6 ineq2i 0 F 1 ..^ F = 0 F 0 + 1 ..^ F
8 0z 0
9 prinfzo0 0 0 F 0 + 1 ..^ F =
10 8 9 ax-mp 0 F 0 + 1 ..^ F =
11 7 10 eqtri 0 F 1 ..^ F =
12 11 imaeq2i P 0 F 1 ..^ F = P
13 ima0 P =
14 12 13 eqtri P 0 F 1 ..^ F =
15 4 14 eqtr3di Fun P -1 P 0 F P 1 ..^ F =
16 15 adantl F Trails G P Fun P -1 P 0 F P 1 ..^ F =
17 1 3 16 3jca F Trails G P Fun P -1 F Trails G P Fun P 1 ..^ F -1 P 0 F P 1 ..^ F =
18 isspth F SPaths G P F Trails G P Fun P -1
19 ispth F Paths G P F Trails G P Fun P 1 ..^ F -1 P 0 F P 1 ..^ F =
20 17 18 19 3imtr4i F SPaths G P F Paths G P