Metamath Proof Explorer

Definition df-isomgr

Description: Define the isomorphy relation for graphs. (Contributed by AV, 11-Nov-2022)

Ref Expression
Assertion df-isomgr ⊢ IsomGr = x y | ∃ f f : Vtx ⁡ x ⟶ 1-1 onto Vtx ⁡ y ∧ ∃ g 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 cisomgr class IsomGr
1 vx setvar x
2 vy setvar y
3 vf setvar f
4 3 cv setvar f
5 cvtx class Vtx
6 1 cv setvar x
7 6 5 cfv class Vtx ⁡ x
8 2 cv setvar y
9 8 5 cfv class Vtx ⁡ y
10 7 9 4 wf1o wff f : Vtx ⁡ x ⟶ 1-1 onto Vtx ⁡ y
11 vg setvar g
12 11 cv setvar g
13 ciedg class iEdg
14 6 13 cfv class iEdg ⁡ x
15 14 cdm class dom ⁡ iEdg ⁡ x
16 8 13 cfv class iEdg ⁡ y
17 16 cdm class dom ⁡ iEdg ⁡ y
18 15 17 12 wf1o wff g : dom ⁡ iEdg ⁡ x ⟶ 1-1 onto dom ⁡ iEdg ⁡ y
19 vi setvar i
20 19 cv setvar i
21 20 14 cfv class iEdg ⁡ x ⁡ i
22 4 21 cima class f iEdg ⁡ x ⁡ i
23 20 12 cfv class g ⁡ i
24 23 16 cfv class iEdg ⁡ y ⁡ g ⁡ i
25 22 24 wceq wff f iEdg ⁡ x ⁡ i = iEdg ⁡ y ⁡ g ⁡ i
26 25 19 15 wral wff ∀ i ∈ dom ⁡ iEdg ⁡ x f iEdg ⁡ x ⁡ i = iEdg ⁡ y ⁡ g ⁡ i
27 18 26 wa wff g : dom ⁡ iEdg ⁡ x ⟶ 1-1 onto dom ⁡ iEdg ⁡ y ∧ ∀ i ∈ dom ⁡ iEdg ⁡ x f iEdg ⁡ x ⁡ i = iEdg ⁡ y ⁡ g ⁡ i
28 27 11 wex wff ∃ g g : dom ⁡ iEdg ⁡ x ⟶ 1-1 onto dom ⁡ iEdg ⁡ y ∧ ∀ i ∈ dom ⁡ iEdg ⁡ x f iEdg ⁡ x ⁡ i = iEdg ⁡ y ⁡ g ⁡ i
29 10 28 wa wff f : Vtx ⁡ x ⟶ 1-1 onto Vtx ⁡ y ∧ ∃ g g : dom ⁡ iEdg ⁡ x ⟶ 1-1 onto dom ⁡ iEdg ⁡ y ∧ ∀ i ∈ dom ⁡ iEdg ⁡ x f iEdg ⁡ x ⁡ i = iEdg ⁡ y ⁡ g ⁡ i
30 29 3 wex wff ∃ f f : Vtx ⁡ x ⟶ 1-1 onto Vtx ⁡ y ∧ ∃ g g : dom ⁡ iEdg ⁡ x ⟶ 1-1 onto dom ⁡ iEdg ⁡ y ∧ ∀ i ∈ dom ⁡ iEdg ⁡ x f iEdg ⁡ x ⁡ i = iEdg ⁡ y ⁡ g ⁡ i
31 30 1 2 copab class x y | ∃ f f : Vtx ⁡ x ⟶ 1-1 onto Vtx ⁡ y ∧ ∃ g g : dom ⁡ iEdg ⁡ x ⟶ 1-1 onto dom ⁡ iEdg ⁡ y ∧ ∀ i ∈ dom ⁡ iEdg ⁡ x f iEdg ⁡ x ⁡ i = iEdg ⁡ y ⁡ g ⁡ i
32 0 31 wceq wff IsomGr = x y | ∃ f f : Vtx ⁡ x ⟶ 1-1 onto Vtx ⁡ y ∧ ∃ g g : dom ⁡ iEdg ⁡ x ⟶ 1-1 onto dom ⁡ iEdg ⁡ y ∧ ∀ i ∈ dom ⁡ iEdg ⁡ x f iEdg ⁡ x ⁡ i = iEdg ⁡ y ⁡ g ⁡ i