This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )