Database
GRAPH THEORY
Vertices and edges
Vertices and indexed edges
The vertices and edges of a graph represented as extensible structure
funiedgval
Metamath Proof Explorer
Description: The set of indexed edges of a graph represented as an extensible structure
with vertices as base set and indexed edges. (Contributed by AV , 21-Sep-2020) (Revised by AV , 7-Jun-2021) (Revised by AV , 12-Nov-2021)
Ref
Expression
Assertion
funiedgval
⊢ ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ { ( Base ‘ ndx ) , ( .ef ‘ ndx ) } ⊆ dom 𝐺 ) → ( iEdg ‘ 𝐺 ) = ( .ef ‘ 𝐺 ) )
Proof
Step
Hyp
Ref
Expression
1
slotsbaseefdif
⊢ ( Base ‘ ndx ) ≠ ( .ef ‘ ndx )
2
fvex
⊢ ( Base ‘ ndx ) ∈ V
3
fvex
⊢ ( .ef ‘ ndx ) ∈ V
4
2 3
funiedgdm2val
⊢ ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ ( Base ‘ ndx ) ≠ ( .ef ‘ ndx ) ∧ { ( Base ‘ ndx ) , ( .ef ‘ ndx ) } ⊆ dom 𝐺 ) → ( iEdg ‘ 𝐺 ) = ( .ef ‘ 𝐺 ) )
5
1 4
mp3an2
⊢ ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ { ( Base ‘ ndx ) , ( .ef ‘ ndx ) } ⊆ dom 𝐺 ) → ( iEdg ‘ 𝐺 ) = ( .ef ‘ 𝐺 ) )