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

Proof

Step Hyp Ref Expression
1 opstrgric.g ⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
2 opstrgric.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 simpl ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) → 𝐺 ∈ UHGraph )
22 21 adantr ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ∧ ( ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐻 ) ∧ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐻 ) ) ) → 𝐺 ∈ UHGraph )
23 simpr ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) → 𝐻 ∈ V )
24 23 adantr ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ∧ ( ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐻 ) ∧ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐻 ) ) ) → 𝐻 ∈ V )
25 simpl ⊢ ( ( ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐻 ) ∧ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐻 ) ) → ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐻 ) )
26 25 adantl ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ∧ ( ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐻 ) ∧ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐻 ) ) ) → ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐻 ) )
27 simpr ⊢ ( ( ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐻 ) ∧ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐻 ) ) → ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐻 ) )
28 27 adantl ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ∧ ( ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐻 ) ∧ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐻 ) ) ) → ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐻 ) )
29 22 24 26 28 grimidvtxedg ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ∧ ( ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐻 ) ∧ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐻 ) ) ) → ( I ↾ ( Vtx ‘ 𝐺 ) ) ∈ ( 𝐺 GraphIso 𝐻 ) )
30 brgrici ⊢ ( ( I ↾ ( Vtx ‘ 𝐺 ) ) ∈ ( 𝐺 GraphIso 𝐻 ) → 𝐺 ≃𝑔𝑟 𝐻 )
31 29 30 syl ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ∧ ( ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐻 ) ∧ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐻 ) ) ) → 𝐺 ≃𝑔𝑟 𝐻 )
32 3 6 13 20 31 syl22anc ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → 𝐺 ≃𝑔𝑟 𝐻 )