Metamath Proof Explorer

Definition df-isomgr

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

Ref Expression
Assertion df-isomgr ⊢IsomGr=xy|∃ff:Vtx⁡x⟶1-1 ontoVtx⁡y∧∃gg:dom⁡iEdg⁡x⟶1-1 ontodom⁡iEdg⁡y∧∀i∈dom⁡iEdg⁡xfiEdg⁡x⁡i=iEdg⁡y⁡g⁡i

Detailed syntax breakdown

Step Hyp Ref Expression
0 cisomgr classIsomGr
1 vx setvarx
2 vy setvary
3 vf setvarf
4 3 cv setvarf
5 cvtx classVtx
6 1 cv setvarx
7 6 5 cfv classVtx⁡x
8 2 cv setvary
9 8 5 cfv classVtx⁡y
10 7 9 4 wf1o wfff:Vtx⁡x⟶1-1 ontoVtx⁡y
11 vg setvarg
12 11 cv setvarg
13 ciedg classiEdg
14 6 13 cfv classiEdg⁡x
15 14 cdm classdom⁡iEdg⁡x
16 8 13 cfv classiEdg⁡y
17 16 cdm classdom⁡iEdg⁡y
18 15 17 12 wf1o wffg:dom⁡iEdg⁡x⟶1-1 ontodom⁡iEdg⁡y
19 vi setvari
20 19 cv setvari
21 20 14 cfv classiEdg⁡x⁡i
22 4 21 cima classfiEdg⁡x⁡i
23 20 12 cfv classg⁡i
24 23 16 cfv classiEdg⁡y⁡g⁡i
25 22 24 wceq wfffiEdg⁡x⁡i=iEdg⁡y⁡g⁡i
26 25 19 15 wral wff∀i∈dom⁡iEdg⁡xfiEdg⁡x⁡i=iEdg⁡y⁡g⁡i
27 18 26 wa wffg:dom⁡iEdg⁡x⟶1-1 ontodom⁡iEdg⁡y∧∀i∈dom⁡iEdg⁡xfiEdg⁡x⁡i=iEdg⁡y⁡g⁡i
28 27 11 wex wff∃gg:dom⁡iEdg⁡x⟶1-1 ontodom⁡iEdg⁡y∧∀i∈dom⁡iEdg⁡xfiEdg⁡x⁡i=iEdg⁡y⁡g⁡i
29 10 28 wa wfff:Vtx⁡x⟶1-1 ontoVtx⁡y∧∃gg:dom⁡iEdg⁡x⟶1-1 ontodom⁡iEdg⁡y∧∀i∈dom⁡iEdg⁡xfiEdg⁡x⁡i=iEdg⁡y⁡g⁡i
30 29 3 wex wff∃ff:Vtx⁡x⟶1-1 ontoVtx⁡y∧∃gg:dom⁡iEdg⁡x⟶1-1 ontodom⁡iEdg⁡y∧∀i∈dom⁡iEdg⁡xfiEdg⁡x⁡i=iEdg⁡y⁡g⁡i
31 30 1 2 copab classxy|∃ff:Vtx⁡x⟶1-1 ontoVtx⁡y∧∃gg:dom⁡iEdg⁡x⟶1-1 ontodom⁡iEdg⁡y∧∀i∈dom⁡iEdg⁡xfiEdg⁡x⁡i=iEdg⁡y⁡g⁡i
32 0 31 wceq wffIsomGr=xy|∃ff:Vtx⁡x⟶1-1 ontoVtx⁡y∧∃gg:dom⁡iEdg⁡x⟶1-1 ontodom⁡iEdg⁡y∧∀i∈dom⁡iEdg⁡xfiEdg⁡x⁡i=iEdg⁡y⁡g⁡i