Metamath Proof Explorer

Theorem gricref

Description: Graph isomorphism is reflexive for hypergraphs. (Contributed by AV, 11-Nov-2022) (Revised by AV, 29-Apr-2025)

Ref Expression
Assertion gricref 
|- ( G e. UHGraph -> G ~=gr G )

Proof

Step Hyp Ref Expression
1 grimid 
 |-  ( G e. UHGraph -> ( _I |` ( Vtx ` G ) ) e. ( G GraphIso G ) )
2 brgrici 
 |-  ( ( _I |` ( Vtx ` G ) ) e. ( G GraphIso G ) -> G ~=gr G )
3 1 2 syl 
 |-  ( G e. UHGraph -> G ~=gr G )