Metamath Proof Explorer

Theorem graop

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

Ref Expression
Hypothesis graop.h 
|- H = <. ( Vtx ` G ) , ( iEdg ` G ) >.
Assertion graop 
|- ( ( Vtx ` G ) = ( Vtx ` H ) /\ ( iEdg ` G ) = ( iEdg ` H ) )

Proof

Step Hyp Ref Expression
1 graop.h 
 |-  H = <. ( Vtx ` G ) , ( iEdg ` G ) >.
2 1 fveq2i 
 |-  ( Vtx ` H ) = ( Vtx ` <. ( Vtx ` G ) , ( iEdg ` G ) >. )
3 fvex 
 |-  ( Vtx ` G ) e. _V
4 fvex 
 |-  ( iEdg ` G ) e. _V
5 3 4 opvtxfvi 
 |-  ( Vtx ` <. ( Vtx ` G ) , ( iEdg ` G ) >. ) = ( Vtx ` G )
6 2 5 eqtr2i 
 |-  ( Vtx ` G ) = ( Vtx ` H )
7 1 fveq2i 
 |-  ( iEdg ` H ) = ( iEdg ` <. ( Vtx ` G ) , ( iEdg ` G ) >. )
8 3 4 opiedgfvi 
 |-  ( iEdg ` <. ( Vtx ` G ) , ( iEdg ` G ) >. ) = ( iEdg ` G )
9 7 8 eqtr2i 
 |-  ( iEdg ` G ) = ( iEdg ` H )
10 6 9 pm3.2i 
 |-  ( ( Vtx ` G ) = ( Vtx ` H ) /\ ( iEdg ` G ) = ( iEdg ` H ) )