Metamath Proof Explorer

Theorem gricer

Description: Isomorphism is an equivalence relation on hypergraphs. (Contributed by AV, 3-May-2025) (Proof shortened by AV, 11-Jul-2025)

Ref Expression
Assertion gricer 
|- ( ~=gr i^i ( UHGraph X. UHGraph ) ) Er UHGraph

Proof

Step Hyp Ref Expression
1 gricref 
 |-  ( g e. UHGraph -> g ~=gr g )
2 gricsym 
 |-  ( g e. UHGraph -> ( g ~=gr h -> h ~=gr g ) )
3 grictr 
 |-  ( ( g ~=gr h /\ h ~=gr k ) -> g ~=gr k )
4 3 a1i 
 |-  ( g e. UHGraph -> ( ( g ~=gr h /\ h ~=gr k ) -> g ~=gr k ) )
5 1 2 4 brinxper 
 |-  ( ~=gr i^i ( UHGraph X. UHGraph ) ) Er UHGraph