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

Metamath Proof Explorer

Theorem wwlksn0

Description: A walk of length 0 is represented by a singleton word. (Contributed by Alexander van der Vekens, 20-Jul-2018) (Revised by AV, 9-Apr-2021) (Proof shortened by AV, 21-May-2021)

Ref Expression
Hypothesis wwlkssswrd.v 
|- V = ( Vtx ` G )
Assertion wwlksn0 
|- ( W e. ( 0 WWalksN G ) -> E. v e. V W = <" v "> )

Proof

Step Hyp Ref Expression
1 wwlkssswrd.v 
 |-  V = ( Vtx ` G )
2 wrdl1exs1 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = 1 ) -> E. v e. ( Vtx ` G ) W = <" v "> )
3 fveqeq2 
 |-  ( w = W -> ( ( # ` w ) = 1 <-> ( # ` W ) = 1 ) )
4 wwlksn0s 
 |-  ( 0 WWalksN G ) = { w e. Word ( Vtx ` G ) | ( # ` w ) = 1 }
5 3 4 elrab2 
 |-  ( W e. ( 0 WWalksN G ) <-> ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = 1 ) )
6 1 rexeqi 
 |-  ( E. v e. V W = <" v "> <-> E. v e. ( Vtx ` G ) W = <" v "> )
7 2 5 6 3imtr4i 
 |-  ( W e. ( 0 WWalksN G ) -> E. v e. V W = <" v "> )