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	$$⊢{\simeq }_{𝑔𝑟}={\mathrm{GraphIso}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]$$

Detailed syntax breakdown

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