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 = ( Vtx ` G )
Assertion 0trl
|- ( G e. U -> ( (/) ( Trails ` G ) P <-> P : ( 0 ... 0 ) --> V ) )

Proof

Step Hyp Ref Expression
1 0wlk.v
 |-  V = ( Vtx ` G )
2 1 0wlk
 |-  ( G e. U -> ( (/) ( Walks ` G ) P <-> P : ( 0 ... 0 ) --> V ) )
3 2 anbi1d
 |-  ( G e. U -> ( ( (/) ( Walks ` G ) P /\ Fun `' (/) ) <-> ( P : ( 0 ... 0 ) --> V /\ Fun `' (/) ) ) )
4 istrl
 |-  ( (/) ( Trails ` G ) P <-> ( (/) ( Walks ` G ) P /\ Fun `' (/) ) )
5 funcnv0
 |-  Fun `' (/)
6 5 biantru
 |-  ( P : ( 0 ... 0 ) --> V <-> ( P : ( 0 ... 0 ) --> V /\ Fun `' (/) ) )
7 3 4 6 3bitr4g
 |-  ( G e. U -> ( (/) ( Trails ` G ) P <-> P : ( 0 ... 0 ) --> V ) )