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 ∈ V
3 fvex ⊢ iEdg ⁡ G ∈ V
4 1 struct2grvtx ⊢ Vtx ⁡ G ∈ V ∧ iEdg ⁡ G ∈ 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 ∈ V ∧ iEdg ⁡ G ∈ 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