Metamath Proof Explorer


Theorem umgr2v2eiedg

Description: The edge function in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020)

Ref Expression
Hypothesis umgr2v2evtx.g 𝐺 = ⟨ 𝑉 , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } ⟩
Assertion umgr2v2eiedg ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) → ( iEdg ‘ 𝐺 ) = { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } )

Proof

Step Hyp Ref Expression
1 umgr2v2evtx.g 𝐺 = ⟨ 𝑉 , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } ⟩
2 1 fveq2i ( iEdg ‘ 𝐺 ) = ( iEdg ‘ ⟨ 𝑉 , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } ⟩ )
3 simp1 ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) → 𝑉𝑊 )
4 prex { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } ∈ V
5 opiedgfv ( ( 𝑉𝑊 ∧ { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } ∈ V ) → ( iEdg ‘ ⟨ 𝑉 , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } ⟩ ) = { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } )
6 3 4 5 sylancl ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) → ( iEdg ‘ ⟨ 𝑉 , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } ⟩ ) = { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } )
7 2 6 syl5eq ( ( 𝑉𝑊𝐴𝑉𝐵𝑉 ) → ( iEdg ‘ 𝐺 ) = { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } )