This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )