Metamath Proof Explorer

Theorem gricrcl

Description: Reverse closure of the "is isomorphic to" relation for graphs. (Contributed by AV, 12-Jun-2025)

Ref Expression
Assertion gricrcl 
|- ( G ~=gr S -> ( G e. _V /\ S e. _V ) )

Proof

Step Hyp Ref Expression
1 brgric 
 |-  ( G ~=gr S <-> ( G GraphIso S ) =/= (/) )
2 grimdmrel 
 |-  Rel dom GraphIso
3 2 ovprc 
 |-  ( -. ( G e. _V /\ S e. _V ) -> ( G GraphIso S ) = (/) )
4 3 necon1ai 
 |-  ( ( G GraphIso S ) =/= (/) -> ( G e. _V /\ S e. _V ) )
5 1 4 sylbi 
 |-  ( G ~=gr S -> ( G e. _V /\ S e. _V ) )