Metamath Proof Explorer


Theorem 0spth

Description: A pair of an empty set (of edges) and a second set (of vertices) is a simple path iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017) (Revised by AV, 18-Jan-2021) (Revised by AV, 30-Oct-2021)

Ref Expression
Hypothesis 0pth.v V = Vtx G
Assertion 0spth G W SPaths G P P : 0 0 V

Proof

Step Hyp Ref Expression
1 0pth.v V = Vtx G
2 1 0trl G W Trails G P P : 0 0 V
3 2 anbi1d G W Trails G P Fun P -1 P : 0 0 V Fun P -1
4 isspth SPaths G P Trails G P Fun P -1
5 fz0sn 0 0 = 0
6 5 feq2i P : 0 0 V P : 0 V
7 c0ex 0 V
8 7 fsn2 P : 0 V P 0 V P = 0 P 0
9 funcnvsn Fun 0 P 0 -1
10 cnveq P = 0 P 0 P -1 = 0 P 0 -1
11 10 funeqd P = 0 P 0 Fun P -1 Fun 0 P 0 -1
12 9 11 mpbiri P = 0 P 0 Fun P -1
13 8 12 simplbiim P : 0 V Fun P -1
14 6 13 sylbi P : 0 0 V Fun P -1
15 14 pm4.71i P : 0 0 V P : 0 0 V Fun P -1
16 3 4 15 3bitr4g G W SPaths G P P : 0 0 V