Theorem 1wlkd

Description: In a graph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a walk. The two vertices need not be distinct (in the case of a loop). (Contributed by AV, 22-Jan-2021) (Revised by AV, 23-Mar-2021)

	Ref	Expression
Hypotheses	1wlkd.p	|- P = <" X Y ">
	1wlkd.f	|- F = <" J ">
	1wlkd.x	|- ( ph -> X e. V )
	1wlkd.y	|- ( ph -> Y e. V )
	1wlkd.l	|- ( ( ph /\ X = Y ) -> ( I ` J ) = { X } )
	1wlkd.j	|- ( ( ph /\ X =/= Y ) -> { X , Y } C_ ( I ` J ) )
	1wlkd.v	|- V = ( Vtx ` G )
	1wlkd.i	|- I = ( iEdg ` G )
Assertion	1wlkd	|- ( ph -> F ( Walks ` G ) P )

Proof

Step	Hyp	Ref	Expression
1		1wlkd.p	|- P = <" X Y ">
2		1wlkd.f	|- F = <" J ">
3		1wlkd.x	|- ( ph -> X e. V )
4		1wlkd.y	|- ( ph -> Y e. V )
5		1wlkd.l	|- ( ( ph /\ X = Y ) -> ( I ` J ) = { X } )
6		1wlkd.j	|- ( ( ph /\ X =/= Y ) -> { X , Y } C_ ( I ` J ) )
7		1wlkd.v	|- V = ( Vtx ` G )
8		1wlkd.i	|- I = ( iEdg ` G )
9	1 2 3 4 5 6	1wlkdlem3	|- ( ph -> F e. Word dom I )
10	1 2 3 4	1wlkdlem1	|- ( ph -> P : ( 0 ... ( # ` F ) ) --> V )
11	1 2 3 4 5 6	1wlkdlem4	|- ( ph -> A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) )
12	7	1vgrex	|- ( X e. V -> G e. _V )
13	7 8	iswlkg	|- ( G e. _V -> ( F ( Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) )
14	3 12 13	3syl	|- ( ph -> ( F ( Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) )
15	9 10 11 14	mpbir3and	|- ( ph -> F ( Walks ` G ) P )