Theorem wlkp

Description: The mapping enumerating the vertices of a walk is a function. (Contributed by AV, 5-Apr-2021)

	Ref	Expression
Hypothesis	wlkp.v	|- V = ( Vtx ` G )
Assertion	wlkp	|- ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> V )

Proof

Step	Hyp	Ref	Expression
1		wlkp.v	|- V = ( Vtx ` G )
2		eqid	|- ( iEdg ` G ) = ( iEdg ` G )
3	1 2	wlkprop	|- ( F ( Walks ` G ) P -> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) )
4	3	simp2d	|- ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> V )