Definition df-grim 47864

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.)

Assertion

Ref	Expression
df-grim	⊢ GraphIso = (𝑔 ∈ V, ℎ ∈ V ↦ {𝑓 ∣ (𝑓:(Vtx‘𝑔)–1-1-onto→(Vtx‘ℎ) ∧ ∃𝑗[(iEdg‘𝑔) / 𝑒][(iEdg‘ℎ) / 𝑑](𝑗:dom 𝑒–1-1-onto→dom 𝑑 ∧ ∀𝑖 ∈ dom 𝑒(𝑑‘(𝑗‘𝑖)) = (𝑓 “ (𝑒‘𝑖))))})

Distinct variable group:   𝑒,𝑑,𝑓,𝑔,ℎ,𝑖,𝑗

Detailed syntax breakdown of Definition df-grim

Step	Hyp	Ref	Expression
1		cgrim 47861	. 2 class GraphIso
2		vg	. . 3 setvar 𝑔
3		vh	. . 3 setvar ℎ
4		cvv 3480	. . 3 class V
5	2	cv 1539	. . . . . . 7 class 𝑔
6		cvtx 29013	. . . . . . 7 class Vtx
7	5, 6	cfv 6561	. . . . . 6 class (Vtx‘𝑔)
8	3	cv 1539	. . . . . . 7 class ℎ
9	8, 6	cfv 6561	. . . . . 6 class (Vtx‘ℎ)
10		vf	. . . . . . 7 setvar 𝑓
11	10	cv 1539	. . . . . 6 class 𝑓
12	7, 9, 11	wf1o 6560	. . . . 5 wff 𝑓:(Vtx‘𝑔)–1-1-onto→(Vtx‘ℎ)
13		ve	. . . . . . . . . . . 12 setvar 𝑒
14	13	cv 1539	. . . . . . . . . . 11 class 𝑒
15	14	cdm 5685	. . . . . . . . . 10 class dom 𝑒
16		vd	. . . . . . . . . . . 12 setvar 𝑑
17	16	cv 1539	. . . . . . . . . . 11 class 𝑑
18	17	cdm 5685	. . . . . . . . . 10 class dom 𝑑
19		vj	. . . . . . . . . . 11 setvar 𝑗
20	19	cv 1539	. . . . . . . . . 10 class 𝑗
21	15, 18, 20	wf1o 6560	. . . . . . . . 9 wff 𝑗:dom 𝑒–1-1-onto→dom 𝑑
22		vi	. . . . . . . . . . . . . 14 setvar 𝑖
23	22	cv 1539	. . . . . . . . . . . . 13 class 𝑖
24	23, 20	cfv 6561	. . . . . . . . . . . 12 class (𝑗‘𝑖)
25	24, 17	cfv 6561	. . . . . . . . . . 11 class (𝑑‘(𝑗‘𝑖))
26	23, 14	cfv 6561	. . . . . . . . . . . 12 class (𝑒‘𝑖)
27	11, 26	cima 5688	. . . . . . . . . . 11 class (𝑓 “ (𝑒‘𝑖))
28	25, 27	wceq 1540	. . . . . . . . . 10 wff (𝑑‘(𝑗‘𝑖)) = (𝑓 “ (𝑒‘𝑖))
29	28, 22, 15	wral 3061	. . . . . . . . 9 wff ∀𝑖 ∈ dom 𝑒(𝑑‘(𝑗‘𝑖)) = (𝑓 “ (𝑒‘𝑖))
30	21, 29	wa 395	. . . . . . . 8 wff (𝑗:dom 𝑒–1-1-onto→dom 𝑑 ∧ ∀𝑖 ∈ dom 𝑒(𝑑‘(𝑗‘𝑖)) = (𝑓 “ (𝑒‘𝑖)))
31		ciedg 29014	. . . . . . . . 9 class iEdg
32	8, 31	cfv 6561	. . . . . . . 8 class (iEdg‘ℎ)
33	30, 16, 32	wsbc 3788	. . . . . . 7 wff [(iEdg‘ℎ) / 𝑑](𝑗:dom 𝑒–1-1-onto→dom 𝑑 ∧ ∀𝑖 ∈ dom 𝑒(𝑑‘(𝑗‘𝑖)) = (𝑓 “ (𝑒‘𝑖)))
34	5, 31	cfv 6561	. . . . . . 7 class (iEdg‘𝑔)
35	33, 13, 34	wsbc 3788	. . . . . 6 wff [(iEdg‘𝑔) / 𝑒][(iEdg‘ℎ) / 𝑑](𝑗:dom 𝑒–1-1-onto→dom 𝑑 ∧ ∀𝑖 ∈ dom 𝑒(𝑑‘(𝑗‘𝑖)) = (𝑓 “ (𝑒‘𝑖)))
36	35, 19	wex 1779	. . . . 5 wff ∃𝑗[(iEdg‘𝑔) / 𝑒][(iEdg‘ℎ) / 𝑑](𝑗:dom 𝑒–1-1-onto→dom 𝑑 ∧ ∀𝑖 ∈ dom 𝑒(𝑑‘(𝑗‘𝑖)) = (𝑓 “ (𝑒‘𝑖)))
37	12, 36	wa 395	. . . 4 wff (𝑓:(Vtx‘𝑔)–1-1-onto→(Vtx‘ℎ) ∧ ∃𝑗[(iEdg‘𝑔) / 𝑒][(iEdg‘ℎ) / 𝑑](𝑗:dom 𝑒–1-1-onto→dom 𝑑 ∧ ∀𝑖 ∈ dom 𝑒(𝑑‘(𝑗‘𝑖)) = (𝑓 “ (𝑒‘𝑖))))
38	37, 10	cab 2714	. . 3 class {𝑓 ∣ (𝑓:(Vtx‘𝑔)–1-1-onto→(Vtx‘ℎ) ∧ ∃𝑗[(iEdg‘𝑔) / 𝑒][(iEdg‘ℎ) / 𝑑](𝑗:dom 𝑒–1-1-onto→dom 𝑑 ∧ ∀𝑖 ∈ dom 𝑒(𝑑‘(𝑗‘𝑖)) = (𝑓 “ (𝑒‘𝑖))))}
39	2, 3, 4, 4, 38	cmpo 7433	. 2 class (𝑔 ∈ V, ℎ ∈ V ↦ {𝑓 ∣ (𝑓:(Vtx‘𝑔)–1-1-onto→(Vtx‘ℎ) ∧ ∃𝑗[(iEdg‘𝑔) / 𝑒][(iEdg‘ℎ) / 𝑑](𝑗:dom 𝑒–1-1-onto→dom 𝑑 ∧ ∀𝑖 ∈ dom 𝑒(𝑑‘(𝑗‘𝑖)) = (𝑓 “ (𝑒‘𝑖))))})
40	1, 39	wceq 1540	1 wff GraphIso = (𝑔 ∈ V, ℎ ∈ V ↦ {𝑓 ∣ (𝑓:(Vtx‘𝑔)–1-1-onto→(Vtx‘ℎ) ∧ ∃𝑗[(iEdg‘𝑔) / 𝑒][(iEdg‘ℎ) / 𝑑](𝑗:dom 𝑒–1-1-onto→dom 𝑑 ∧ ∀𝑖 ∈ dom 𝑒(𝑑‘(𝑗‘𝑖)) = (𝑓 “ (𝑒‘𝑖))))})

This definition is referenced by:  grimfn  47865  grimdmrel  47866  isgrim  47868