This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opstrgric

Description: A graph represented as an extensible structure with vertices as base set and indexed edges is isomorphic to a hypergraph represented as ordered pair with the same vertices and edges. (Contributed by AV, 11-Nov-2022) (Revised by AV, 4-May-2025)

Ref Expression
Hypotheses opstrgric.g 
|- G = <. V , E >.
opstrgric.h 
|- H = { <. ( Base ` ndx ) , V >. , <. ( .ef ` ndx ) , E >. }
Assertion opstrgric 
|- ( ( G e. UHGraph /\ V e. X /\ E e. Y ) -> G ~=gr H )

Proof

Step Hyp Ref Expression
1 opstrgric.g 
 |-  G = <. V , E >.
2 opstrgric.h 
 |-  H = { <. ( Base ` ndx ) , V >. , <. ( .ef ` ndx ) , E >. }
3 simp1 
 |-  ( ( G e. UHGraph /\ V e. X /\ E e. Y ) -> G e. UHGraph )
4 prex 
 |-  { <. ( Base ` ndx ) , V >. , <. ( .ef ` ndx ) , E >. } e. _V
5 2 4 eqeltri 
 |-  H e. _V
6 5 a1i 
 |-  ( ( G e. UHGraph /\ V e. X /\ E e. Y ) -> H e. _V )
7 opvtxfv 
 |-  ( ( V e. X /\ E e. Y ) -> ( Vtx ` <. V , E >. ) = V )
8 7 3adant1 
 |-  ( ( G e. UHGraph /\ V e. X /\ E e. Y ) -> ( Vtx ` <. V , E >. ) = V )
9 1 fveq2i 
 |-  ( Vtx ` G ) = ( Vtx ` <. V , E >. )
10 9 a1i 
 |-  ( ( G e. UHGraph /\ V e. X /\ E e. Y ) -> ( Vtx ` G ) = ( Vtx ` <. V , E >. ) )
11 2 struct2grvtx 
 |-  ( ( V e. X /\ E e. Y ) -> ( Vtx ` H ) = V )
12 11 3adant1 
 |-  ( ( G e. UHGraph /\ V e. X /\ E e. Y ) -> ( Vtx ` H ) = V )
13 8 10 12 3eqtr4d 
 |-  ( ( G e. UHGraph /\ V e. X /\ E e. Y ) -> ( Vtx ` G ) = ( Vtx ` H ) )
14 opiedgfv 
 |-  ( ( V e. X /\ E e. Y ) -> ( iEdg ` <. V , E >. ) = E )
15 14 3adant1 
 |-  ( ( G e. UHGraph /\ V e. X /\ E e. Y ) -> ( iEdg ` <. V , E >. ) = E )
16 1 fveq2i 
 |-  ( iEdg ` G ) = ( iEdg ` <. V , E >. )
17 16 a1i 
 |-  ( ( G e. UHGraph /\ V e. X /\ E e. Y ) -> ( iEdg ` G ) = ( iEdg ` <. V , E >. ) )
18 2 struct2griedg 
 |-  ( ( V e. X /\ E e. Y ) -> ( iEdg ` H ) = E )
19 18 3adant1 
 |-  ( ( G e. UHGraph /\ V e. X /\ E e. Y ) -> ( iEdg ` H ) = E )
20 15 17 19 3eqtr4d 
 |-  ( ( G e. UHGraph /\ V e. X /\ E e. Y ) -> ( iEdg ` G ) = ( iEdg ` H ) )
21 simpl 
 |-  ( ( G e. UHGraph /\ H e. _V ) -> G e. UHGraph )
22 21 adantr 
 |-  ( ( ( G e. UHGraph /\ H e. _V ) /\ ( ( Vtx ` G ) = ( Vtx ` H ) /\ ( iEdg ` G ) = ( iEdg ` H ) ) ) -> G e. UHGraph )
23 simpr 
 |-  ( ( G e. UHGraph /\ H e. _V ) -> H e. _V )
24 23 adantr 
 |-  ( ( ( G e. UHGraph /\ H e. _V ) /\ ( ( Vtx ` G ) = ( Vtx ` H ) /\ ( iEdg ` G ) = ( iEdg ` H ) ) ) -> H e. _V )
25 simpl 
 |-  ( ( ( Vtx ` G ) = ( Vtx ` H ) /\ ( iEdg ` G ) = ( iEdg ` H ) ) -> ( Vtx ` G ) = ( Vtx ` H ) )
26 25 adantl 
 |-  ( ( ( G e. UHGraph /\ H e. _V ) /\ ( ( Vtx ` G ) = ( Vtx ` H ) /\ ( iEdg ` G ) = ( iEdg ` H ) ) ) -> ( Vtx ` G ) = ( Vtx ` H ) )
27 simpr 
 |-  ( ( ( Vtx ` G ) = ( Vtx ` H ) /\ ( iEdg ` G ) = ( iEdg ` H ) ) -> ( iEdg ` G ) = ( iEdg ` H ) )
28 27 adantl 
 |-  ( ( ( G e. UHGraph /\ H e. _V ) /\ ( ( Vtx ` G ) = ( Vtx ` H ) /\ ( iEdg ` G ) = ( iEdg ` H ) ) ) -> ( iEdg ` G ) = ( iEdg ` H ) )
29 22 24 26 28 grimidvtxedg 
 |-  ( ( ( G e. UHGraph /\ H e. _V ) /\ ( ( Vtx ` G ) = ( Vtx ` H ) /\ ( iEdg ` G ) = ( iEdg ` H ) ) ) -> ( _I |` ( Vtx ` G ) ) e. ( G GraphIso H ) )
30 brgrici 
 |-  ( ( _I |` ( Vtx ` G ) ) e. ( G GraphIso H ) -> G ~=gr H )
31 29 30 syl 
 |-  ( ( ( G e. UHGraph /\ H e. _V ) /\ ( ( Vtx ` G ) = ( Vtx ` H ) /\ ( iEdg ` G ) = ( iEdg ` H ) ) ) -> G ~=gr H )
32 3 6 13 20 31 syl22anc 
 |-  ( ( G e. UHGraph /\ V e. X /\ E e. Y ) -> G ~=gr H )