Metamath Proof Explorer


Theorem 0trl

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

Ref Expression
Hypothesis 0wlk.v V=VtxG
Assertion 0trl GUTrailsGPP:00V

Proof

Step Hyp Ref Expression
1 0wlk.v V=VtxG
2 1 0wlk GUWalksGPP:00V
3 2 anbi1d GUWalksGPFun-1P:00VFun-1
4 istrl TrailsGPWalksGPFun-1
5 funcnv0 Fun-1
6 5 biantru P:00VP:00VFun-1
7 3 4 6 3bitr4g GUTrailsGPP:00V