Metamath Proof Explorer

Definition df-grisom

Description: Define the class of all isomorphisms between two graphs. (Contributed by AV, 11-Dec-2022)

Ref Expression
Assertion df-grisom ⊢ GrIsom = 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 GrIsom
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 GrIsom = 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