Metamath Proof Explorer

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=VE
strisomgrop.h ⊢H=BasendxVef⁡ndxE
Assertion strisomgrop ⊢G∈UHGraph∧V∈X∧E∈Y→GIsomGrH

Proof

Step Hyp Ref Expression
1 strisomgrop.g ⊢G=VE
2 strisomgrop.h ⊢H=BasendxVef⁡ndxE
3 simp1 ⊢G∈UHGraph∧V∈X∧E∈Y→G∈UHGraph
4 prex ⊢BasendxVef⁡ndxE∈V
5 2 4 eqeltri ⊢H∈V
6 5 a1i ⊢G∈UHGraph∧V∈X∧E∈Y→H∈V
7 opvtxfv ⊢V∈X∧E∈Y→Vtx⁡VE=V
8 7 3adant1 ⊢G∈UHGraph∧V∈X∧E∈Y→Vtx⁡VE=V
9 1 fveq2i ⊢Vtx⁡G=Vtx⁡VE
10 9 a1i ⊢G∈UHGraph∧V∈X∧E∈Y→Vtx⁡G=Vtx⁡VE
11 2 struct2grvtx ⊢V∈X∧E∈Y→Vtx⁡H=V
12 11 3adant1 ⊢G∈UHGraph∧V∈X∧E∈Y→Vtx⁡H=V
13 8 10 12 3eqtr4d ⊢G∈UHGraph∧V∈X∧E∈Y→Vtx⁡G=Vtx⁡H
14 opiedgfv ⊢V∈X∧E∈Y→iEdg⁡VE=E
15 14 3adant1 ⊢G∈UHGraph∧V∈X∧E∈Y→iEdg⁡VE=E
16 1 fveq2i ⊢iEdg⁡G=iEdg⁡VE
17 16 a1i ⊢G∈UHGraph∧V∈X∧E∈Y→iEdg⁡G=iEdg⁡VE
18 2 struct2griedg ⊢V∈X∧E∈Y→iEdg⁡H=E
19 18 3adant1 ⊢G∈UHGraph∧V∈X∧E∈Y→iEdg⁡H=E
20 15 17 19 3eqtr4d ⊢G∈UHGraph∧V∈X∧E∈Y→iEdg⁡G=iEdg⁡H
21 isomgreqve ⊢G∈UHGraph∧H∈V∧Vtx⁡G=Vtx⁡H∧iEdg⁡G=iEdg⁡H→GIsomGrH
22 3 6 13 20 21 syl22anc ⊢G∈UHGraph∧V∈X∧E∈Y→GIsomGrH