Metamath Proof Explorer


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 )