Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-isomgr Structured version   Visualization version   GIF version

Definition df-isomgr 44278
 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
StepHypRef Expression
1 cisomgr 44276 . 2 class IsomGr
2 vx . . . . . . . 8 setvar 𝑥
32cv 1537 . . . . . . 7 class 𝑥
4 cvtx 26787 . . . . . . 7 class Vtx
53, 4cfv 6334 . . . . . 6 class (Vtx‘𝑥)
6 vy . . . . . . . 8 setvar 𝑦
76cv 1537 . . . . . . 7 class 𝑦
87, 4cfv 6334 . . . . . 6 class (Vtx‘𝑦)
9 vf . . . . . . 7 setvar 𝑓
109cv 1537 . . . . . 6 class 𝑓
115, 8, 10wf1o 6333 . . . . 5 wff 𝑓:(Vtx‘𝑥)–1-1-onto→(Vtx‘𝑦)
12 ciedg 26788 . . . . . . . . . 10 class iEdg
133, 12cfv 6334 . . . . . . . . 9 class (iEdg‘𝑥)
1413cdm 5532 . . . . . . . 8 class dom (iEdg‘𝑥)
157, 12cfv 6334 . . . . . . . . 9 class (iEdg‘𝑦)
1615cdm 5532 . . . . . . . 8 class dom (iEdg‘𝑦)
17 vg . . . . . . . . 9 setvar 𝑔
1817cv 1537 . . . . . . . 8 class 𝑔
1914, 16, 18wf1o 6333 . . . . . . 7 wff 𝑔:dom (iEdg‘𝑥)–1-1-onto→dom (iEdg‘𝑦)
20 vi . . . . . . . . . . . 12 setvar 𝑖
2120cv 1537 . . . . . . . . . . 11 class 𝑖
2221, 13cfv 6334 . . . . . . . . . 10 class ((iEdg‘𝑥)‘𝑖)
2310, 22cima 5535 . . . . . . . . 9 class (𝑓 “ ((iEdg‘𝑥)‘𝑖))
2421, 18cfv 6334 . . . . . . . . . 10 class (𝑔𝑖)
2524, 15cfv 6334 . . . . . . . . 9 class ((iEdg‘𝑦)‘(𝑔𝑖))
2623, 25wceq 1538 . . . . . . . 8 wff (𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔𝑖))
2726, 20, 14wral 3130 . . . . . . 7 wff 𝑖 ∈ dom (iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔𝑖))
2819, 27wa 399 . . . . . 6 wff (𝑔:dom (iEdg‘𝑥)–1-1-onto→dom (iEdg‘𝑦) ∧ ∀𝑖 ∈ dom (iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔𝑖)))
2928, 17wex 1781 . . . . 5 wff 𝑔(𝑔:dom (iEdg‘𝑥)–1-1-onto→dom (iEdg‘𝑦) ∧ ∀𝑖 ∈ dom (iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔𝑖)))
3011, 29wa 399 . . . 4 wff (𝑓:(Vtx‘𝑥)–1-1-onto→(Vtx‘𝑦) ∧ ∃𝑔(𝑔:dom (iEdg‘𝑥)–1-1-onto→dom (iEdg‘𝑦) ∧ ∀𝑖 ∈ dom (iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔𝑖))))
3130, 9wex 1781 . . 3 wff 𝑓(𝑓:(Vtx‘𝑥)–1-1-onto→(Vtx‘𝑦) ∧ ∃𝑔(𝑔:dom (iEdg‘𝑥)–1-1-onto→dom (iEdg‘𝑦) ∧ ∀𝑖 ∈ dom (iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔𝑖))))
3231, 2, 6copab 5104 . 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑓(𝑓:(Vtx‘𝑥)–1-1-onto→(Vtx‘𝑦) ∧ ∃𝑔(𝑔:dom (iEdg‘𝑥)–1-1-onto→dom (iEdg‘𝑦) ∧ ∀𝑖 ∈ dom (iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔𝑖))))}
331, 32wceq 1538 1 wff IsomGr = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓(𝑓:(Vtx‘𝑥)–1-1-onto→(Vtx‘𝑦) ∧ ∃𝑔(𝑔:dom (iEdg‘𝑥)–1-1-onto→dom (iEdg‘𝑦) ∧ ∀𝑖 ∈ dom (iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔𝑖))))}
 Colors of variables: wff setvar class This definition is referenced by:  isomgrrel  44279  isomgr  44280
 Copyright terms: Public domain W3C validator