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 V
4 fvex iEdg G 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