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 ) |