Theorem upgr1pthond

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 path from one of these vertices to the other vertex. The two vertices need not be distinct (in the case of a loop) - in this case, however, the path is not a simple path. (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	upgr1pthond	|- ( ph -> F ( X ( PathsOn ` G ) Y ) 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	1pthond	|- ( ph -> F ( X ( PathsOn ` G ) Y ) P )