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	$⊢ ≃_{𝑔𝑟} = {GraphIso}^{-1} [V ∖ 1_{𝑜}]$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgric	$class ≃_{𝑔𝑟}$
1		cgrim	$class GraphIso$
2	1	ccnv	$class {GraphIso}^{-1}$
3		cvv	$class V$
4		c1o	$class 1_{𝑜}$
5	3 4	cdif	$class (V ∖ 1_{𝑜})$
6	2 5	cima	$class {GraphIso}^{-1} [V ∖ 1_{𝑜}]$
7	0 6	wceq	$wff ≃_{𝑔𝑟} = {GraphIso}^{-1} [V ∖ 1_{𝑜}]$