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 “ ( V ∖ 1o ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgric	⊢ ≃𝑔𝑟
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	⊢ ≃𝑔𝑟 = ( ◡ GraphIso “ ( V ∖ 1o ) )