Metamath Proof Explorer

Theorem isomgrref

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

Ref Expression
Assertion isomgrref 
|- ( G e. UHGraph -> G IsomGr G )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( G e. UHGraph -> G e. 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 e. UHGraph -> ( ( Vtx ` G ) = ( Vtx ` G ) /\ ( iEdg ` G ) = ( iEdg ` G ) ) )
6 isomgreqve 
 |-  ( ( ( G e. UHGraph /\ G e. UHGraph ) /\ ( ( Vtx ` G ) = ( Vtx ` G ) /\ ( iEdg ` G ) = ( iEdg ` G ) ) ) -> G IsomGr G )
7 1 1 5 6 syl21anc 
 |-  ( G e. UHGraph -> G IsomGr G )