Definition df-grisom 44005

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

Assertion

Ref	Expression
df-grisom	⊢ GrIsom = (𝑥 ∈ V, 𝑦 ∈ V ↦ {⟨𝑓, 𝑔⟩ ∣ (𝑓:(Vtx‘𝑥)–1-1-onto→(Vtx‘𝑦) ∧ 𝑔:dom (iEdg‘𝑥)–1-1-onto→dom (iEdg‘𝑦) ∧ ∀𝑖 ∈ dom (iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔‘𝑖)))})

Distinct variable group:   𝑓,𝑔,𝑖,𝑥,𝑦

Detailed syntax breakdown of Definition df-grisom

Step	Hyp	Ref	Expression
1		cgrisom 44003	. 2 class GrIsom
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cvv 3494	. . 3 class V
5	2	cv 1536	. . . . . . 7 class 𝑥
6		cvtx 26781	. . . . . . 7 class Vtx
7	5, 6	cfv 6355	. . . . . 6 class (Vtx‘𝑥)
8	3	cv 1536	. . . . . . 7 class 𝑦
9	8, 6	cfv 6355	. . . . . 6 class (Vtx‘𝑦)
10		vf	. . . . . . 7 setvar 𝑓
11	10	cv 1536	. . . . . 6 class 𝑓
12	7, 9, 11	wf1o 6354	. . . . 5 wff 𝑓:(Vtx‘𝑥)–1-1-onto→(Vtx‘𝑦)
13		ciedg 26782	. . . . . . . 8 class iEdg
14	5, 13	cfv 6355	. . . . . . 7 class (iEdg‘𝑥)
15	14	cdm 5555	. . . . . 6 class dom (iEdg‘𝑥)
16	8, 13	cfv 6355	. . . . . . 7 class (iEdg‘𝑦)
17	16	cdm 5555	. . . . . 6 class dom (iEdg‘𝑦)
18		vg	. . . . . . 7 setvar 𝑔
19	18	cv 1536	. . . . . 6 class 𝑔
20	15, 17, 19	wf1o 6354	. . . . 5 wff 𝑔:dom (iEdg‘𝑥)–1-1-onto→dom (iEdg‘𝑦)
21		vi	. . . . . . . . . 10 setvar 𝑖
22	21	cv 1536	. . . . . . . . 9 class 𝑖
23	22, 14	cfv 6355	. . . . . . . 8 class ((iEdg‘𝑥)‘𝑖)
24	11, 23	cima 5558	. . . . . . 7 class (𝑓 “ ((iEdg‘𝑥)‘𝑖))
25	22, 19	cfv 6355	. . . . . . . 8 class (𝑔‘𝑖)
26	25, 16	cfv 6355	. . . . . . 7 class ((iEdg‘𝑦)‘(𝑔‘𝑖))
27	24, 26	wceq 1537	. . . . . 6 wff (𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔‘𝑖))
28	27, 21, 15	wral 3138	. . . . 5 wff ∀𝑖 ∈ dom (iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔‘𝑖))
29	12, 20, 28	w3a 1083	. . . 4 wff (𝑓:(Vtx‘𝑥)–1-1-onto→(Vtx‘𝑦) ∧ 𝑔:dom (iEdg‘𝑥)–1-1-onto→dom (iEdg‘𝑦) ∧ ∀𝑖 ∈ dom (iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔‘𝑖)))
30	29, 10, 18	copab 5128	. . 3 class {⟨𝑓, 𝑔⟩ ∣ (𝑓:(Vtx‘𝑥)–1-1-onto→(Vtx‘𝑦) ∧ 𝑔:dom (iEdg‘𝑥)–1-1-onto→dom (iEdg‘𝑦) ∧ ∀𝑖 ∈ dom (iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔‘𝑖)))}
31	2, 3, 4, 4, 30	cmpo 7158	. 2 class (𝑥 ∈ V, 𝑦 ∈ V ↦ {⟨𝑓, 𝑔⟩ ∣ (𝑓:(Vtx‘𝑥)–1-1-onto→(Vtx‘𝑦) ∧ 𝑔:dom (iEdg‘𝑥)–1-1-onto→dom (iEdg‘𝑦) ∧ ∀𝑖 ∈ dom (iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔‘𝑖)))})
32	1, 31	wceq 1537	1 wff GrIsom = (𝑥 ∈ V, 𝑦 ∈ V ↦ {⟨𝑓, 𝑔⟩ ∣ (𝑓:(Vtx‘𝑥)–1-1-onto→(Vtx‘𝑦) ∧ 𝑔:dom (iEdg‘𝑥)–1-1-onto→dom (iEdg‘𝑦) ∧ ∀𝑖 ∈ dom (iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔‘𝑖)))})

This definition is referenced by: (None)