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 ∈ UHGraph ∧ V ∈ X ∧ E ∈ Y → G ≃ 𝑔𝑟 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 ∈ UHGraph ∧ V ∈ X ∧ E ∈ Y → G ∈ UHGraph
4 prex ⊢ Base ndx V ef ⁡ ndx E ∈ 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 ⁡ V E = V
8 7 3adant1 ⊢ G ∈ UHGraph ∧ V ∈ X ∧ E ∈ Y → Vtx ⁡ V E = V
9 1 fveq2i ⊢ Vtx ⁡ G = Vtx ⁡ V E
10 9 a1i ⊢ G ∈ UHGraph ∧ V ∈ X ∧ E ∈ Y → Vtx ⁡ G = Vtx ⁡ V E
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 ⁡ V E = E
15 14 3adant1 ⊢ G ∈ UHGraph ∧ V ∈ X ∧ E ∈ Y → iEdg ⁡ V E = E
16 1 fveq2i ⊢ iEdg ⁡ G = iEdg ⁡ V E
17 16 a1i ⊢ G ∈ UHGraph ∧ V ∈ X ∧ E ∈ Y → iEdg ⁡ G = iEdg ⁡ V E
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 simpl ⊢ G ∈ UHGraph ∧ H ∈ V → G ∈ UHGraph
22 21 adantr ⊢ G ∈ UHGraph ∧ H ∈ V ∧ Vtx ⁡ G = Vtx ⁡ H ∧ iEdg ⁡ G = iEdg ⁡ H → G ∈ UHGraph
23 simpr ⊢ G ∈ UHGraph ∧ H ∈ V → H ∈ V
24 23 adantr ⊢ G ∈ UHGraph ∧ H ∈ V ∧ Vtx ⁡ G = Vtx ⁡ H ∧ iEdg ⁡ G = iEdg ⁡ H → H ∈ V
25 simpl ⊢ Vtx ⁡ G = Vtx ⁡ H ∧ iEdg ⁡ G = iEdg ⁡ H → Vtx ⁡ G = Vtx ⁡ H
26 25 adantl ⊢ G ∈ UHGraph ∧ H ∈ 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 ∈ UHGraph ∧ H ∈ V ∧ Vtx ⁡ G = Vtx ⁡ H ∧ iEdg ⁡ G = iEdg ⁡ H → iEdg ⁡ G = iEdg ⁡ H
29 22 24 26 28 grimidvtxedg ⊢ G ∈ UHGraph ∧ H ∈ V ∧ Vtx ⁡ G = Vtx ⁡ H ∧ iEdg ⁡ G = iEdg ⁡ H → I ↾ Vtx ⁡ G ∈ G GraphIso H
30 brgrici ⊢ I ↾ Vtx ⁡ G ∈ G GraphIso H → G ≃ 𝑔𝑟 H
31 29 30 syl ⊢ G ∈ UHGraph ∧ H ∈ V ∧ Vtx ⁡ G = Vtx ⁡ H ∧ iEdg ⁡ G = iEdg ⁡ H → G ≃ 𝑔𝑟 H
32 3 6 13 20 31 syl22anc ⊢ G ∈ UHGraph ∧ V ∈ X ∧ E ∈ Y → G ≃ 𝑔𝑟 H