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

Metamath Proof Explorer

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