Definition df-grisom 47863

Description: Define the class of all isomorphisms between two graphs. In contrast to (𝐹 GraphIso 𝐻), which is a set of functions between the vertices, (𝐹 GraphIsom 𝐻) 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 47864. (Contributed by AV, 11-Dec-2022.) (New usage is discouraged.)

Assertion

Ref	Expression
df-grisom	⊢ GraphIsom = (𝑥 ∈ 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 47860	. 2 class GraphIsom
2		vx	. . 3 setvar 𝑥
3		vy	. . 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		ciedg 29014	. . . . . . . 8 class iEdg
14	5, 13	cfv 6561	. . . . . . 7 class (iEdg‘𝑥)
15	14	cdm 5685	. . . . . 6 class dom (iEdg‘𝑥)
16	8, 13	cfv 6561	. . . . . . 7 class (iEdg‘𝑦)
17	16	cdm 5685	. . . . . 6 class dom (iEdg‘𝑦)
18		vg	. . . . . . 7 setvar 𝑔
19	18	cv 1539	. . . . . 6 class 𝑔
20	15, 17, 19	wf1o 6560	. . . . 5 wff 𝑔:dom (iEdg‘𝑥)–1-1-onto→dom (iEdg‘𝑦)
21		vi	. . . . . . . . . 10 setvar 𝑖
22	21	cv 1539	. . . . . . . . 9 class 𝑖
23	22, 14	cfv 6561	. . . . . . . 8 class ((iEdg‘𝑥)‘𝑖)
24	11, 23	cima 5688	. . . . . . 7 class (𝑓 “ ((iEdg‘𝑥)‘𝑖))
25	22, 19	cfv 6561	. . . . . . . 8 class (𝑔‘𝑖)
26	25, 16	cfv 6561	. . . . . . 7 class ((iEdg‘𝑦)‘(𝑔‘𝑖))
27	24, 26	wceq 1540	. . . . . 6 wff (𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔‘𝑖))
28	27, 21, 15	wral 3061	. . . . 5 wff ∀𝑖 ∈ dom (iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔‘𝑖))
29	12, 20, 28	w3a 1087	. . . 4 wff (𝑓:(Vtx‘𝑥)–1-1-onto→(Vtx‘𝑦) ∧ 𝑔:dom (iEdg‘𝑥)–1-1-onto→dom (iEdg‘𝑦) ∧ ∀𝑖 ∈ dom (iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔‘𝑖)))
30	29, 10, 18	copab 5205	. . 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 7433	. 2 class (𝑥 ∈ V, 𝑦 ∈ V ↦ {⟨𝑓, 𝑔⟩ ∣ (𝑓:(Vtx‘𝑥)–1-1-onto→(Vtx‘𝑦) ∧ 𝑔:dom (iEdg‘𝑥)–1-1-onto→dom (iEdg‘𝑦) ∧ ∀𝑖 ∈ dom (iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔‘𝑖)))})
32	1, 31	wceq 1540	1 wff GraphIsom = (𝑥 ∈ V, 𝑦 ∈ V ↦ {⟨𝑓, 𝑔⟩ ∣ (𝑓:(Vtx‘𝑥)–1-1-onto→(Vtx‘𝑦) ∧ 𝑔:dom (iEdg‘𝑥)–1-1-onto→dom (iEdg‘𝑦) ∧ ∀𝑖 ∈ dom (iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔‘𝑖)))})

This definition is referenced by: (None)