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 = V E
strisomgrop.h ⊢ H = Base ndx V ef ⁡ ndx E
Assertion strisomgrop ⊢ G ∈ UHGraph ∧ V ∈ X ∧ 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 ∈ 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 isomgreqve ⊢ G ∈ UHGraph ∧ H ∈ V ∧ Vtx ⁡ G = Vtx ⁡ H ∧ iEdg ⁡ G = iEdg ⁡ H → G IsomGr H
22 3 6 13 20 21 syl22anc ⊢ G ∈ UHGraph ∧ V ∈ X ∧ E ∈ Y → G IsomGr H