# 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 𝐺 = ⟨ 𝑉 , 𝐸
strisomgrop.h 𝐻 = { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ }
Assertion strisomgrop ( ( 𝐺 ∈ UHGraph ∧ 𝑉𝑋𝐸𝑌 ) → 𝐺 IsomGr 𝐻 )

### Proof

Step Hyp Ref Expression
1 strisomgrop.g 𝐺 = ⟨ 𝑉 , 𝐸
2 strisomgrop.h 𝐻 = { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ }
3 simp1 ( ( 𝐺 ∈ UHGraph ∧ 𝑉𝑋𝐸𝑌 ) → 𝐺 ∈ UHGraph )
4 prex { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ } ∈ V
5 2 4 eqeltri 𝐻 ∈ V
6 5 a1i ( ( 𝐺 ∈ UHGraph ∧ 𝑉𝑋𝐸𝑌 ) → 𝐻 ∈ V )
7 opvtxfv ( ( 𝑉𝑋𝐸𝑌 ) → ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 )
8 7 3adant1 ( ( 𝐺 ∈ UHGraph ∧ 𝑉𝑋𝐸𝑌 ) → ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 )
9 1 fveq2i ( Vtx ‘ 𝐺 ) = ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ )
10 9 a1i ( ( 𝐺 ∈ UHGraph ∧ 𝑉𝑋𝐸𝑌 ) → ( Vtx ‘ 𝐺 ) = ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) )
11 2 struct2grvtx ( ( 𝑉𝑋𝐸𝑌 ) → ( Vtx ‘ 𝐻 ) = 𝑉 )
12 11 3adant1 ( ( 𝐺 ∈ UHGraph ∧ 𝑉𝑋𝐸𝑌 ) → ( Vtx ‘ 𝐻 ) = 𝑉 )
13 8 10 12 3eqtr4d ( ( 𝐺 ∈ UHGraph ∧ 𝑉𝑋𝐸𝑌 ) → ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐻 ) )
14 opiedgfv ( ( 𝑉𝑋𝐸𝑌 ) → ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 )
15 14 3adant1 ( ( 𝐺 ∈ UHGraph ∧ 𝑉𝑋𝐸𝑌 ) → ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 )
16 1 fveq2i ( iEdg ‘ 𝐺 ) = ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ )
17 16 a1i ( ( 𝐺 ∈ UHGraph ∧ 𝑉𝑋𝐸𝑌 ) → ( iEdg ‘ 𝐺 ) = ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) )
18 2 struct2griedg ( ( 𝑉𝑋𝐸𝑌 ) → ( iEdg ‘ 𝐻 ) = 𝐸 )
19 18 3adant1 ( ( 𝐺 ∈ UHGraph ∧ 𝑉𝑋𝐸𝑌 ) → ( iEdg ‘ 𝐻 ) = 𝐸 )
20 15 17 19 3eqtr4d ( ( 𝐺 ∈ UHGraph ∧ 𝑉𝑋𝐸𝑌 ) → ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐻 ) )
21 isomgreqve ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ∧ ( ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐻 ) ∧ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐻 ) ) ) → 𝐺 IsomGr 𝐻 )
22 3 6 13 20 21 syl22anc ( ( 𝐺 ∈ UHGraph ∧ 𝑉𝑋𝐸𝑌 ) → 𝐺 IsomGr 𝐻 )