Metamath Proof Explorer


Theorem is0trl

Description: A pair of an empty set (of edges) and a sequence of one vertex is a trail (of length 0). (Contributed by AV, 7-Jan-2021) (Revised by AV, 23-Mar-2021) (Proof shortened by AV, 30-Oct-2021)

Ref Expression
Hypothesis 0wlk.v V = Vtx G
Assertion is0trl P = 0 N N V Trails G P

Proof

Step Hyp Ref Expression
1 0wlk.v V = Vtx G
2 1fv N V P = 0 N P : 0 0 V P 0 = N
3 2 ancoms P = 0 N N V P : 0 0 V P 0 = N
4 3 simpld P = 0 N N V P : 0 0 V
5 1 1vgrex N V G V
6 5 adantl P = 0 N N V G V
7 1 0trl G V Trails G P P : 0 0 V
8 6 7 syl P = 0 N N V Trails G P P : 0 0 V
9 4 8 mpbird P = 0 N N V Trails G P