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 ⊢ 𝐻 = { ⟨ ( Base ‘ ndx ) , ( Vtx ‘ 𝐺 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( iEdg ‘ 𝐺 ) ⟩ }
Assertion grastruct ( ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐻 ) ∧ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐻 ) )

Proof

Step Hyp Ref Expression
1 grastruct.h ⊢ 𝐻 = { ⟨ ( Base ‘ ndx ) , ( Vtx ‘ 𝐺 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( iEdg ‘ 𝐺 ) ⟩ }
2 fvex ⊢ ( Vtx ‘ 𝐺 ) ∈ V
3 fvex ⊢ ( iEdg ‘ 𝐺 ) ∈ V
4 1 struct2grvtx ⊢ ( ( ( Vtx ‘ 𝐺 ) ∈ V ∧ ( iEdg ‘ 𝐺 ) ∈ V ) → ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐺 ) )
5 2 3 4 mp2an ⊢ ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐺 )
6 5 eqcomi ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐻 )
7 1 struct2griedg ⊢ ( ( ( Vtx ‘ 𝐺 ) ∈ V ∧ ( iEdg ‘ 𝐺 ) ∈ V ) → ( iEdg ‘ 𝐻 ) = ( iEdg ‘ 𝐺 ) )
8 2 3 7 mp2an ⊢ ( iEdg ‘ 𝐻 ) = ( iEdg ‘ 𝐺 )
9 8 eqcomi ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐻 )
10 6 9 pm3.2i ⊢ ( ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐻 ) ∧ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐻 ) )