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