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