Theorem upgr1wlkd

Description: In a pseudograph 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)

	Ref	Expression
Hypotheses	upgr1wlkd.p	|- P = <" X Y ">
	upgr1wlkd.f	|- F = <" J ">
	upgr1wlkd.x	|- ( ph -> X e. ( Vtx ` G ) )
	upgr1wlkd.y	|- ( ph -> Y e. ( Vtx ` G ) )
	upgr1wlkd.j	|- ( ph -> ( ( iEdg ` G ) ` J ) = { X , Y } )
	upgr1wlkd.g	|- ( ph -> G e. UPGraph )
Assertion	upgr1wlkd	|- ( ph -> F ( Walks ` G ) P )

Proof

Step	Hyp	Ref	Expression
1		upgr1wlkd.p	|- P = <" X Y ">
2		upgr1wlkd.f	|- F = <" J ">
3		upgr1wlkd.x	|- ( ph -> X e. ( Vtx ` G ) )
4		upgr1wlkd.y	|- ( ph -> Y e. ( Vtx ` G ) )
5		upgr1wlkd.j	|- ( ph -> ( ( iEdg ` G ) ` J ) = { X , Y } )
6		upgr1wlkd.g	|- ( ph -> G e. UPGraph )
7	1 2 3 4 5	upgr1wlkdlem1	|- ( ( ph /\ X = Y ) -> ( ( iEdg ` G ) ` J ) = { X } )
8	1 2 3 4 5	upgr1wlkdlem2	|- ( ( ph /\ X =/= Y ) -> { X , Y } C_ ( ( iEdg ` G ) ` J ) )
9		eqid	|- ( Vtx ` G ) = ( Vtx ` G )
10		eqid	|- ( iEdg ` G ) = ( iEdg ` G )
11	1 2 3 4 7 8 9 10	1wlkd	|- ( ph -> F ( Walks ` G ) P )