Metamath Proof Explorer


Theorem struct2griedg

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, 23-Sep-2020) (Proof shortened by AV, 12-Nov-2021)

Ref Expression
Hypothesis struct2grvtx.g
|- G = { <. ( Base ` ndx ) , V >. , <. ( .ef ` ndx ) , E >. }
Assertion struct2griedg
|- ( ( V e. X /\ E e. Y ) -> ( iEdg ` G ) = E )

Proof

Step Hyp Ref Expression
1 struct2grvtx.g
 |-  G = { <. ( Base ` ndx ) , V >. , <. ( .ef ` ndx ) , E >. }
2 1 struct2grstr
 |-  G Struct <. ( Base ` ndx ) , ( .ef ` ndx ) >.
3 2 a1i
 |-  ( ( V e. X /\ E e. Y ) -> G Struct <. ( Base ` ndx ) , ( .ef ` ndx ) >. )
4 simpl
 |-  ( ( V e. X /\ E e. Y ) -> V e. X )
5 simpr
 |-  ( ( V e. X /\ E e. Y ) -> E e. Y )
6 1 eqimss2i
 |-  { <. ( Base ` ndx ) , V >. , <. ( .ef ` ndx ) , E >. } C_ G
7 6 a1i
 |-  ( ( V e. X /\ E e. Y ) -> { <. ( Base ` ndx ) , V >. , <. ( .ef ` ndx ) , E >. } C_ G )
8 3 4 5 7 structgrssiedg
 |-  ( ( V e. X /\ E e. Y ) -> ( iEdg ` G ) = E )