Theorem grastruct

Description: Any representation of a graph G (especially as ordered pair G = <. V , E >. ) is convertible in a representation of the graph as extensible structure. (Contributed by AV, 8-Oct-2020)

	Ref	Expression
Hypothesis	grastruct.h	|- H = { <. ( Base ` ndx ) , ( Vtx ` G ) >. , <. ( .ef ` ndx ) , ( iEdg ` G ) >. }
Assertion	grastruct	|- ( ( Vtx ` G ) = ( Vtx ` H ) /\ ( iEdg ` G ) = ( iEdg ` H ) )

Proof

Step	Hyp	Ref	Expression
1		grastruct.h	|- H = { <. ( Base ` ndx ) , ( Vtx ` G ) >. , <. ( .ef ` ndx ) , ( iEdg ` G ) >. }
2		fvex	|- ( Vtx ` G ) e. _V
3		fvex	|- ( iEdg ` G ) e. _V
4	1	struct2grvtx	|- ( ( ( Vtx ` G ) e. _V /\ ( iEdg ` G ) e. _V ) -> ( Vtx ` H ) = ( Vtx ` G ) )
5	2 3 4	mp2an	|- ( Vtx ` H ) = ( Vtx ` G )
6	5	eqcomi	|- ( Vtx ` G ) = ( Vtx ` H )
7	1	struct2griedg	|- ( ( ( Vtx ` G ) e. _V /\ ( iEdg ` G ) e. _V ) -> ( iEdg ` H ) = ( iEdg ` G ) )
8	2 3 7	mp2an	|- ( iEdg ` H ) = ( iEdg ` G )
9	8	eqcomi	|- ( iEdg ` G ) = ( iEdg ` H )
10	6 9	pm3.2i	|- ( ( Vtx ` G ) = ( Vtx ` H ) /\ ( iEdg ` G ) = ( iEdg ` H ) )