Metamath Proof Explorer

Theorem gricrel

Description: The "is isomorphic to" relation for graphs is a relation. (Contributed by AV, 11-Nov-2022) (Revised by AV, 5-May-2025)

Ref Expression
Assertion gricrel 
|- Rel ~=gr

Proof

Step Hyp Ref Expression
1 df-gric 
 |-  ~=gr = ( `' GraphIso " ( _V \ 1o ) )
2 cnvimass 
 |-  ( `' GraphIso " ( _V \ 1o ) ) C_ dom GraphIso
3 grimfn 
 |-  GraphIso Fn ( _V X. _V )
4 3 fndmi 
 |-  dom GraphIso = ( _V X. _V )
5 2 4 sseqtri 
 |-  ( `' GraphIso " ( _V \ 1o ) ) C_ ( _V X. _V )
6 1 5 eqsstri 
 |-  ~=gr C_ ( _V X. _V )
7 relxp 
 |-  Rel ( _V X. _V )
8 relss 
 |-  ( ~=gr C_ ( _V X. _V ) -> ( Rel ( _V X. _V ) -> Rel ~=gr ) )
9 6 7 8 mp2 
 |-  Rel ~=gr