Definition df-isomgr 45161

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

Assertion

Ref	Expression
df-isomgr	⊢ IsomGr = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓(𝑓:(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-isomgr

Step	Hyp	Ref	Expression
1		cisomgr 45159	. 2 class IsomGr
2		vx	. . . . . . . 8 setvar 𝑥
3	2	cv 1538	. . . . . . 7 class 𝑥
4		cvtx 27269	. . . . . . 7 class Vtx
5	3, 4	cfv 6418	. . . . . 6 class (Vtx‘𝑥)
6		vy	. . . . . . . 8 setvar 𝑦
7	6	cv 1538	. . . . . . 7 class 𝑦
8	7, 4	cfv 6418	. . . . . 6 class (Vtx‘𝑦)
9		vf	. . . . . . 7 setvar 𝑓
10	9	cv 1538	. . . . . 6 class 𝑓
11	5, 8, 10	wf1o 6417	. . . . 5 wff 𝑓:(Vtx‘𝑥)–1-1-onto→(Vtx‘𝑦)
12		ciedg 27270	. . . . . . . . . 10 class iEdg
13	3, 12	cfv 6418	. . . . . . . . 9 class (iEdg‘𝑥)
14	13	cdm 5580	. . . . . . . 8 class dom (iEdg‘𝑥)
15	7, 12	cfv 6418	. . . . . . . . 9 class (iEdg‘𝑦)
16	15	cdm 5580	. . . . . . . 8 class dom (iEdg‘𝑦)
17		vg	. . . . . . . . 9 setvar 𝑔
18	17	cv 1538	. . . . . . . 8 class 𝑔
19	14, 16, 18	wf1o 6417	. . . . . . 7 wff 𝑔:dom (iEdg‘𝑥)–1-1-onto→dom (iEdg‘𝑦)
20		vi	. . . . . . . . . . . 12 setvar 𝑖
21	20	cv 1538	. . . . . . . . . . 11 class 𝑖
22	21, 13	cfv 6418	. . . . . . . . . 10 class ((iEdg‘𝑥)‘𝑖)
23	10, 22	cima 5583	. . . . . . . . 9 class (𝑓 “ ((iEdg‘𝑥)‘𝑖))
24	21, 18	cfv 6418	. . . . . . . . . 10 class (𝑔‘𝑖)
25	24, 15	cfv 6418	. . . . . . . . 9 class ((iEdg‘𝑦)‘(𝑔‘𝑖))
26	23, 25	wceq 1539	. . . . . . . 8 wff (𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔‘𝑖))
27	26, 20, 14	wral 3063	. . . . . . 7 wff ∀𝑖 ∈ dom (iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔‘𝑖))
28	19, 27	wa 395	. . . . . 6 wff (𝑔:dom (iEdg‘𝑥)–1-1-onto→dom (iEdg‘𝑦) ∧ ∀𝑖 ∈ dom (iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔‘𝑖)))
29	28, 17	wex 1783	. . . . 5 wff ∃𝑔(𝑔:dom (iEdg‘𝑥)–1-1-onto→dom (iEdg‘𝑦) ∧ ∀𝑖 ∈ dom (iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔‘𝑖)))
30	11, 29	wa 395	. . . 4 wff (𝑓:(Vtx‘𝑥)–1-1-onto→(Vtx‘𝑦) ∧ ∃𝑔(𝑔:dom (iEdg‘𝑥)–1-1-onto→dom (iEdg‘𝑦) ∧ ∀𝑖 ∈ dom (iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔‘𝑖))))
31	30, 9	wex 1783	. . 3 wff ∃𝑓(𝑓:(Vtx‘𝑥)–1-1-onto→(Vtx‘𝑦) ∧ ∃𝑔(𝑔:dom (iEdg‘𝑥)–1-1-onto→dom (iEdg‘𝑦) ∧ ∀𝑖 ∈ dom (iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔‘𝑖))))
32	31, 2, 6	copab 5132	. 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑓(𝑓:(Vtx‘𝑥)–1-1-onto→(Vtx‘𝑦) ∧ ∃𝑔(𝑔:dom (iEdg‘𝑥)–1-1-onto→dom (iEdg‘𝑦) ∧ ∀𝑖 ∈ dom (iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔‘𝑖))))}
33	1, 32	wceq 1539	1 wff IsomGr = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓(𝑓:(Vtx‘𝑥)–1-1-onto→(Vtx‘𝑦) ∧ ∃𝑔(𝑔:dom (iEdg‘𝑥)–1-1-onto→dom (iEdg‘𝑦) ∧ ∀𝑖 ∈ dom (iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔‘𝑖))))}

This definition is referenced by:  isomgrrel  45162  isomgr  45163