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 “ ( 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 ) )