Metamath Proof Explorer

Definition df-grim

Description: An isomorphism between two graphs is a bijection between the sets of vertices of the two graphs that preserves adjacency, see definition in Diestel p. 3. (Contributed by AV, 19-Apr-2025)

Ref Expression
Assertion df-grim ⊢ GraphIso = g ∈ V , h ∈ V ⟼ f | f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h ∧ ∃ j [˙ iEdg ⁡ g / e]˙ [˙ iEdg ⁡ h / d]˙ j : dom ⁡ e ⟶ 1-1 onto dom ⁡ d ∧ ∀ i ∈ dom ⁡ e d ⁡ j ⁡ i = f e ⁡ i

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgrim class GraphIso
1 vg setvar g
2 cvv class V
3 vh setvar h
4 vf setvar f
5 4 cv setvar f
6 cvtx class Vtx
7 1 cv setvar g
8 7 6 cfv class Vtx ⁡ g
9 3 cv setvar h
10 9 6 cfv class Vtx ⁡ h
11 8 10 5 wf1o wff f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h
12 vj setvar j
13 ciedg class iEdg
14 7 13 cfv class iEdg ⁡ g
15 ve setvar e
16 9 13 cfv class iEdg ⁡ h
17 vd setvar d
18 12 cv setvar j
19 15 cv setvar e
20 19 cdm class dom ⁡ e
21 17 cv setvar d
22 21 cdm class dom ⁡ d
23 20 22 18 wf1o wff j : dom ⁡ e ⟶ 1-1 onto dom ⁡ d
24 vi setvar i
25 24 cv setvar i
26 25 18 cfv class j ⁡ i
27 26 21 cfv class d ⁡ j ⁡ i
28 25 19 cfv class e ⁡ i
29 5 28 cima class f e ⁡ i
30 27 29 wceq wff d ⁡ j ⁡ i = f e ⁡ i
31 30 24 20 wral wff ∀ i ∈ dom ⁡ e d ⁡ j ⁡ i = f e ⁡ i
32 23 31 wa wff j : dom ⁡ e ⟶ 1-1 onto dom ⁡ d ∧ ∀ i ∈ dom ⁡ e d ⁡ j ⁡ i = f e ⁡ i
33 32 17 16 wsbc wff [˙ iEdg ⁡ h / d]˙ j : dom ⁡ e ⟶ 1-1 onto dom ⁡ d ∧ ∀ i ∈ dom ⁡ e d ⁡ j ⁡ i = f e ⁡ i
34 33 15 14 wsbc wff [˙ iEdg ⁡ g / e]˙ [˙ iEdg ⁡ h / d]˙ j : dom ⁡ e ⟶ 1-1 onto dom ⁡ d ∧ ∀ i ∈ dom ⁡ e d ⁡ j ⁡ i = f e ⁡ i
35 34 12 wex wff ∃ j [˙ iEdg ⁡ g / e]˙ [˙ iEdg ⁡ h / d]˙ j : dom ⁡ e ⟶ 1-1 onto dom ⁡ d ∧ ∀ i ∈ dom ⁡ e d ⁡ j ⁡ i = f e ⁡ i
36 11 35 wa wff f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h ∧ ∃ j [˙ iEdg ⁡ g / e]˙ [˙ iEdg ⁡ h / d]˙ j : dom ⁡ e ⟶ 1-1 onto dom ⁡ d ∧ ∀ i ∈ dom ⁡ e d ⁡ j ⁡ i = f e ⁡ i
37 36 4 cab class f | f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h ∧ ∃ j [˙ iEdg ⁡ g / e]˙ [˙ iEdg ⁡ h / d]˙ j : dom ⁡ e ⟶ 1-1 onto dom ⁡ d ∧ ∀ i ∈ dom ⁡ e d ⁡ j ⁡ i = f e ⁡ i
38 1 3 2 2 37 cmpo class g ∈ V , h ∈ V ⟼ f | f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h ∧ ∃ j [˙ iEdg ⁡ g / e]˙ [˙ iEdg ⁡ h / d]˙ j : dom ⁡ e ⟶ 1-1 onto dom ⁡ d ∧ ∀ i ∈ dom ⁡ e d ⁡ j ⁡ i = f e ⁡ i
39 0 38 wceq wff GraphIso = g ∈ V , h ∈ V ⟼ f | f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h ∧ ∃ j [˙ iEdg ⁡ g / e]˙ [˙ iEdg ⁡ h / d]˙ j : dom ⁡ e ⟶ 1-1 onto dom ⁡ d ∧ ∀ i ∈ dom ⁡ e d ⁡ j ⁡ i = f e ⁡ i