This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database GRAPH THEORY Vertices and edges Vertices and indexed edges The vertices and edges of a graph represented as extensible structure funiedgval
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
basendxnedgfndx ⊢ ( 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 ‘ 𝐺 ) )