Metamath Proof Explorer


Theorem 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 ‘ 𝐺 ) )