Theorem strisomgrop

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)

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

Proof

Step	Hyp	Ref	Expression
1		strisomgrop.g	|- G = <. V , E >.
2		strisomgrop.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		isomgreqve	|- ( ( ( G e. UHGraph /\ H e. _V ) /\ ( ( Vtx ` G ) = ( Vtx ` H ) /\ ( iEdg ` G ) = ( iEdg ` H ) ) ) -> G IsomGr H )
22	3 6 13 20 21	syl22anc	|- ( ( G e. UHGraph /\ V e. X /\ E e. Y ) -> G IsomGr H )