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 𝑃 = ⟨“ 𝑋 𝑌 ”⟩
upgr1wlkd.f 𝐹 = ⟨“ 𝐽 ”⟩
upgr1wlkd.x ( 𝜑𝑋 ∈ ( Vtx ‘ 𝐺 ) )
upgr1wlkd.y ( 𝜑𝑌 ∈ ( Vtx ‘ 𝐺 ) )
upgr1wlkd.j ( 𝜑 → ( ( iEdg ‘ 𝐺 ) ‘ 𝐽 ) = { 𝑋 , 𝑌 } )
upgr1wlkd.g ( 𝜑𝐺 ∈ UPGraph )
Assertion upgr1wlkd ( 𝜑𝐹 ( Walks ‘ 𝐺 ) 𝑃 )

Proof

Step Hyp Ref Expression
1 upgr1wlkd.p 𝑃 = ⟨“ 𝑋 𝑌 ”⟩
2 upgr1wlkd.f 𝐹 = ⟨“ 𝐽 ”⟩
3 upgr1wlkd.x ( 𝜑𝑋 ∈ ( Vtx ‘ 𝐺 ) )
4 upgr1wlkd.y ( 𝜑𝑌 ∈ ( Vtx ‘ 𝐺 ) )
5 upgr1wlkd.j ( 𝜑 → ( ( iEdg ‘ 𝐺 ) ‘ 𝐽 ) = { 𝑋 , 𝑌 } )
6 upgr1wlkd.g ( 𝜑𝐺 ∈ UPGraph )
7 1 2 3 4 5 upgr1wlkdlem1 ( ( 𝜑𝑋 = 𝑌 ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝐽 ) = { 𝑋 } )
8 1 2 3 4 5 upgr1wlkdlem2 ( ( 𝜑𝑋𝑌 ) → { 𝑋 , 𝑌 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝐽 ) )
9 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
10 eqid ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
11 1 2 3 4 7 8 9 10 1wlkd ( 𝜑𝐹 ( Walks ‘ 𝐺 ) 𝑃 )