Metamath Proof Explorer


Theorem uspgrloopvtxel

Description: A vertex in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop ). (Contributed by AV, 17-Dec-2020)

Ref Expression
Hypothesis uspgrloopvtx.g 𝐺 = ⟨ 𝑉 , { ⟨ 𝐴 , { 𝑁 } ⟩ } ⟩
Assertion uspgrloopvtxel ( ( 𝑉𝑊𝑁𝑉 ) → 𝑁 ∈ ( Vtx ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 uspgrloopvtx.g 𝐺 = ⟨ 𝑉 , { ⟨ 𝐴 , { 𝑁 } ⟩ } ⟩
2 1 uspgrloopvtx ( 𝑉𝑊 → ( Vtx ‘ 𝐺 ) = 𝑉 )
3 eleq2 ( 𝑉 = ( Vtx ‘ 𝐺 ) → ( 𝑁𝑉𝑁 ∈ ( Vtx ‘ 𝐺 ) ) )
4 3 biimpd ( 𝑉 = ( Vtx ‘ 𝐺 ) → ( 𝑁𝑉𝑁 ∈ ( Vtx ‘ 𝐺 ) ) )
5 4 eqcoms ( ( Vtx ‘ 𝐺 ) = 𝑉 → ( 𝑁𝑉𝑁 ∈ ( Vtx ‘ 𝐺 ) ) )
6 5 com12 ( 𝑁𝑉 → ( ( Vtx ‘ 𝐺 ) = 𝑉𝑁 ∈ ( Vtx ‘ 𝐺 ) ) )
7 2 6 mpan9 ( ( 𝑉𝑊𝑁𝑉 ) → 𝑁 ∈ ( Vtx ‘ 𝐺 ) )