Metamath Proof Explorer

Definition df-grisom

Description: Define the class of all isomorphisms between two graphs. In contrast to ( F GraphIso H ) , which is a set of functions between the vertices, ( F GraphIsom H ) is a set of pairs of functions: a function between the vertices, and a function between the (indices of the) edges.

It is not clear if such a definition is useful. In the definition by Diestel p. 3, for example, the bijection between the vertices is called an isomorphism, as formalized in df-grim . (Contributed by AV, 11-Dec-2022) (New usage is discouraged.)

Ref Expression
Assertion df-grisom ⊢ GraphIsom = x ∈ V , y ∈ V ⟼ f g | f : Vtx ⁡ x ⟶ 1-1 onto Vtx ⁡ y ∧ g : dom ⁡ iEdg ⁡ x ⟶ 1-1 onto dom ⁡ iEdg ⁡ y ∧ ∀ i ∈ dom ⁡ iEdg ⁡ x f iEdg ⁡ x ⁡ i = iEdg ⁡ y ⁡ g ⁡ i

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgrisom class GraphIsom
1 vx setvar x
2 cvv class V
3 vy setvar y
4 vf setvar f
5 vg setvar g
6 4 cv setvar f
7 cvtx class Vtx
8 1 cv setvar x
9 8 7 cfv class Vtx ⁡ x
10 3 cv setvar y
11 10 7 cfv class Vtx ⁡ y
12 9 11 6 wf1o wff f : Vtx ⁡ x ⟶ 1-1 onto Vtx ⁡ y
13 5 cv setvar g
14 ciedg class iEdg
15 8 14 cfv class iEdg ⁡ x
16 15 cdm class dom ⁡ iEdg ⁡ x
17 10 14 cfv class iEdg ⁡ y
18 17 cdm class dom ⁡ iEdg ⁡ y
19 16 18 13 wf1o wff g : dom ⁡ iEdg ⁡ x ⟶ 1-1 onto dom ⁡ iEdg ⁡ y
20 vi setvar i
21 20 cv setvar i
22 21 15 cfv class iEdg ⁡ x ⁡ i
23 6 22 cima class f iEdg ⁡ x ⁡ i
24 21 13 cfv class g ⁡ i
25 24 17 cfv class iEdg ⁡ y ⁡ g ⁡ i
26 23 25 wceq wff f iEdg ⁡ x ⁡ i = iEdg ⁡ y ⁡ g ⁡ i
27 26 20 16 wral wff ∀ i ∈ dom ⁡ iEdg ⁡ x f iEdg ⁡ x ⁡ i = iEdg ⁡ y ⁡ g ⁡ i
28 12 19 27 w3a wff f : Vtx ⁡ x ⟶ 1-1 onto Vtx ⁡ y ∧ g : dom ⁡ iEdg ⁡ x ⟶ 1-1 onto dom ⁡ iEdg ⁡ y ∧ ∀ i ∈ dom ⁡ iEdg ⁡ x f iEdg ⁡ x ⁡ i = iEdg ⁡ y ⁡ g ⁡ i
29 28 4 5 copab class f g | f : Vtx ⁡ x ⟶ 1-1 onto Vtx ⁡ y ∧ g : dom ⁡ iEdg ⁡ x ⟶ 1-1 onto dom ⁡ iEdg ⁡ y ∧ ∀ i ∈ dom ⁡ iEdg ⁡ x f iEdg ⁡ x ⁡ i = iEdg ⁡ y ⁡ g ⁡ i
30 1 3 2 2 29 cmpo class x ∈ V , y ∈ V ⟼ f g | f : Vtx ⁡ x ⟶ 1-1 onto Vtx ⁡ y ∧ g : dom ⁡ iEdg ⁡ x ⟶ 1-1 onto dom ⁡ iEdg ⁡ y ∧ ∀ i ∈ dom ⁡ iEdg ⁡ x f iEdg ⁡ x ⁡ i = iEdg ⁡ y ⁡ g ⁡ i
31 0 30 wceq wff GraphIsom = x ∈ V , y ∈ V ⟼ f g | f : Vtx ⁡ x ⟶ 1-1 onto Vtx ⁡ y ∧ g : dom ⁡ iEdg ⁡ x ⟶ 1-1 onto dom ⁡ iEdg ⁡ y ∧ ∀ i ∈ dom ⁡ iEdg ⁡ x f iEdg ⁡ x ⁡ i = iEdg ⁡ y ⁡ g ⁡ i