Metamath Proof Explorer

Theorem gricsym

Description: Graph isomorphism is symmetric for hypergraphs. (Contributed by AV, 11-Nov-2022) (Revised by AV, 3-May-2025)

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

Proof

Step Hyp Ref Expression
1 brgric 
 |-  ( G ~=gr S <-> ( G GraphIso S ) =/= (/) )
2 n0 
 |-  ( ( G GraphIso S ) =/= (/) <-> E. f f e. ( G GraphIso S ) )
3 1 2 bitri 
 |-  ( G ~=gr S <-> E. f f e. ( G GraphIso S ) )
4 grimcnv 
 |-  ( G e. UHGraph -> ( f e. ( G GraphIso S ) -> `' f e. ( S GraphIso G ) ) )
5 brgrici 
 |-  ( `' f e. ( S GraphIso G ) -> S ~=gr G )
6 4 5 syl6 
 |-  ( G e. UHGraph -> ( f e. ( G GraphIso S ) -> S ~=gr G ) )
7 6 exlimdv 
 |-  ( G e. UHGraph -> ( E. f f e. ( G GraphIso S ) -> S ~=gr G ) )
8 3 7 biimtrid 
 |-  ( G e. UHGraph -> ( G ~=gr S -> S ~=gr G ) )