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 ‘ 〈 𝑉 , 𝐸 〉 ) = 𝐸 ) |
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 ‘ 〈 𝑉 , 𝐸 〉 ) = 𝐸 ) |