Metamath Proof Explorer


Theorem opiedgfv

Description: The set of indexed edges of a graph represented as an ordered pair of vertices and indexed edges as function value. (Contributed by AV, 21-Sep-2020)

Ref Expression
Assertion opiedgfv ( ( 𝑉𝑋𝐸𝑌 ) → ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 )

Proof

Step Hyp Ref Expression
1 opelvvg ( ( 𝑉𝑋𝐸𝑌 ) → ⟨ 𝑉 , 𝐸 ⟩ ∈ ( V × V ) )
2 opiedgval ( ⟨ 𝑉 , 𝐸 ⟩ ∈ ( V × V ) → ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = ( 2nd ‘ ⟨ 𝑉 , 𝐸 ⟩ ) )
3 1 2 syl ( ( 𝑉𝑋𝐸𝑌 ) → ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = ( 2nd ‘ ⟨ 𝑉 , 𝐸 ⟩ ) )
4 op2ndg ( ( 𝑉𝑋𝐸𝑌 ) → ( 2nd ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 )
5 3 4 eqtrd ( ( 𝑉𝑋𝐸𝑌 ) → ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 )