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 ‘ 𝐻 ) )