Metamath Proof Explorer

Theorem isomgrref

Description: The isomorphy relation is reflexive for hypergraphs. (Contributed by AV, 11-Nov-2022)

Ref Expression
Assertion isomgrref ⊢ G ∈ UHGraph → G IsomGr G

Proof

Step Hyp Ref Expression
1 id ⊢ G ∈ UHGraph → G ∈ UHGraph
2 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
3 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
4 2 3 pm3.2i ⊢ Vtx ⁡ G = Vtx ⁡ G ∧ iEdg ⁡ G = iEdg ⁡ G
5 4 a1i ⊢ G ∈ UHGraph → Vtx ⁡ G = Vtx ⁡ G ∧ iEdg ⁡ G = iEdg ⁡ G
6 isomgreqve ⊢ G ∈ UHGraph ∧ G ∈ UHGraph ∧ Vtx ⁡ G = Vtx ⁡ G ∧ iEdg ⁡ G = iEdg ⁡ G → G IsomGr G
7 1 1 5 6 syl21anc ⊢ G ∈ UHGraph → G IsomGr G