This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-gric

Description: Two graphs are said to be isomorphic iff they are connected by at least one isomorphism, see definition in Diestel p. 3 and definition in Bollobas p. 3. Isomorphic graphs share all global graph properties like order and size. (Contributed by AV, 11-Nov-2022) (Revised by AV, 19-Apr-2025)

Ref Expression
Assertion df-gric 
|- ~=gr = ( `' GraphIso " ( _V \ 1o ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgric 
 |-  ~=gr
1 cgrim 
 |-  GraphIso
2 1 ccnv 
 |-  `' GraphIso
3 cvv 
 |-  _V
4 c1o 
 |-  1o
5 3 4 cdif 
 |-  ( _V \ 1o )
6 2 5 cima 
 |-  ( `' GraphIso " ( _V \ 1o ) )
7 0 6 wceq 
 |-  ~=gr = ( `' GraphIso " ( _V \ 1o ) )