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 = { <. x , y >. | E. f ( f : ( Vtx ` x ) -1-1-onto-> ( Vtx ` y ) /\ E. g ( g : dom ( iEdg ` x ) -1-1-onto-> dom ( iEdg ` y ) /\ A. i e. dom ( iEdg ` x ) ( f " ( ( iEdg ` x ) ` i ) ) = ( ( iEdg ` y ) ` ( g ` i ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cisomgr 
 |-  IsomGr
1 vx 
 |-  x
2 vy 
 |-  y
3 vf 
 |-  f
4 3 cv 
 |-  f
5 cvtx 
 |-  Vtx
6 1 cv 
 |-  x
7 6 5 cfv 
 |-  ( Vtx ` x )
8 2 cv 
 |-  y
9 8 5 cfv 
 |-  ( Vtx ` y )
10 7 9 4 wf1o 
 |-  f : ( Vtx ` x ) -1-1-onto-> ( Vtx ` y )
11 vg 
 |-  g
12 11 cv 
 |-  g
13 ciedg 
 |-  iEdg
14 6 13 cfv 
 |-  ( iEdg ` x )
15 14 cdm 
 |-  dom ( iEdg ` x )
16 8 13 cfv 
 |-  ( iEdg ` y )
17 16 cdm 
 |-  dom ( iEdg ` y )
18 15 17 12 wf1o 
 |-  g : dom ( iEdg ` x ) -1-1-onto-> dom ( iEdg ` y )
19 vi 
 |-  i
20 19 cv 
 |-  i
21 20 14 cfv 
 |-  ( ( iEdg ` x ) ` i )
22 4 21 cima 
 |-  ( f " ( ( iEdg ` x ) ` i ) )
23 20 12 cfv 
 |-  ( g ` i )
24 23 16 cfv 
 |-  ( ( iEdg ` y ) ` ( g ` i ) )
25 22 24 wceq 
 |-  ( f " ( ( iEdg ` x ) ` i ) ) = ( ( iEdg ` y ) ` ( g ` i ) )
26 25 19 15 wral 
 |-  A. i e. dom ( iEdg ` x ) ( f " ( ( iEdg ` x ) ` i ) ) = ( ( iEdg ` y ) ` ( g ` i ) )
27 18 26 wa 
 |-  ( g : dom ( iEdg ` x ) -1-1-onto-> dom ( iEdg ` y ) /\ A. i e. dom ( iEdg ` x ) ( f " ( ( iEdg ` x ) ` i ) ) = ( ( iEdg ` y ) ` ( g ` i ) ) )
28 27 11 wex 
 |-  E. g ( g : dom ( iEdg ` x ) -1-1-onto-> dom ( iEdg ` y ) /\ A. i e. dom ( iEdg ` x ) ( f " ( ( iEdg ` x ) ` i ) ) = ( ( iEdg ` y ) ` ( g ` i ) ) )
29 10 28 wa 
 |-  ( f : ( Vtx ` x ) -1-1-onto-> ( Vtx ` y ) /\ E. g ( g : dom ( iEdg ` x ) -1-1-onto-> dom ( iEdg ` y ) /\ A. i e. dom ( iEdg ` x ) ( f " ( ( iEdg ` x ) ` i ) ) = ( ( iEdg ` y ) ` ( g ` i ) ) ) )
30 29 3 wex 
 |-  E. f ( f : ( Vtx ` x ) -1-1-onto-> ( Vtx ` y ) /\ E. g ( g : dom ( iEdg ` x ) -1-1-onto-> dom ( iEdg ` y ) /\ A. i e. dom ( iEdg ` x ) ( f " ( ( iEdg ` x ) ` i ) ) = ( ( iEdg ` y ) ` ( g ` i ) ) ) )
31 30 1 2 copab 
 |-  { <. x , y >. | E. f ( f : ( Vtx ` x ) -1-1-onto-> ( Vtx ` y ) /\ E. g ( g : dom ( iEdg ` x ) -1-1-onto-> dom ( iEdg ` y ) /\ A. i e. dom ( iEdg ` x ) ( f " ( ( iEdg ` x ) ` i ) ) = ( ( iEdg ` y ) ` ( g ` i ) ) ) ) }
32 0 31 wceq 
 |-  IsomGr = { <. x , y >. | E. f ( f : ( Vtx ` x ) -1-1-onto-> ( Vtx ` y ) /\ E. g ( g : dom ( iEdg ` x ) -1-1-onto-> dom ( iEdg ` y ) /\ A. i e. dom ( iEdg ` x ) ( f " ( ( iEdg ` x ) ` i ) ) = ( ( iEdg ` y ) ` ( g ` i ) ) ) ) }