Metamath Proof Explorer

Definition df-grisom

Description: Define the class of all isomorphisms between two graphs. (Contributed by AV, 11-Dec-2022)

Ref Expression
Assertion df-grisom 
|- GrIsom = ( x e. _V , y e. _V |-> { <. f , g >. | ( f : ( Vtx ` x ) -1-1-onto-> ( Vtx ` y ) /\ 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 cgrisom 
 |-  GrIsom
1 vx 
 |-  x
2 cvv 
 |-  _V
3 vy 
 |-  y
4 vf 
 |-  f
5 vg 
 |-  g
6 4 cv 
 |-  f
7 cvtx 
 |-  Vtx
8 1 cv 
 |-  x
9 8 7 cfv 
 |-  ( Vtx ` x )
10 3 cv 
 |-  y
11 10 7 cfv 
 |-  ( Vtx ` y )
12 9 11 6 wf1o 
 |-  f : ( Vtx ` x ) -1-1-onto-> ( Vtx ` y )
13 5 cv 
 |-  g
14 ciedg 
 |-  iEdg
15 8 14 cfv 
 |-  ( iEdg ` x )
16 15 cdm 
 |-  dom ( iEdg ` x )
17 10 14 cfv 
 |-  ( iEdg ` y )
18 17 cdm 
 |-  dom ( iEdg ` y )
19 16 18 13 wf1o 
 |-  g : dom ( iEdg ` x ) -1-1-onto-> dom ( iEdg ` y )
20 vi 
 |-  i
21 20 cv 
 |-  i
22 21 15 cfv 
 |-  ( ( iEdg ` x ) ` i )
23 6 22 cima 
 |-  ( f " ( ( iEdg ` x ) ` i ) )
24 21 13 cfv 
 |-  ( g ` i )
25 24 17 cfv 
 |-  ( ( iEdg ` y ) ` ( g ` i ) )
26 23 25 wceq 
 |-  ( f " ( ( iEdg ` x ) ` i ) ) = ( ( iEdg ` y ) ` ( g ` i ) )
27 26 20 16 wral 
 |-  A. i e. dom ( iEdg ` x ) ( f " ( ( iEdg ` x ) ` i ) ) = ( ( iEdg ` y ) ` ( g ` i ) )
28 12 19 27 w3a 
 |-  ( f : ( Vtx ` x ) -1-1-onto-> ( Vtx ` y ) /\ 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 28 4 5 copab 
 |-  { <. f , g >. | ( f : ( Vtx ` x ) -1-1-onto-> ( Vtx ` y ) /\ 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 1 3 2 2 29 cmpo 
 |-  ( x e. _V , y e. _V |-> { <. f , g >. | ( f : ( Vtx ` x ) -1-1-onto-> ( Vtx ` y ) /\ 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 0 30 wceq 
 |-  GrIsom = ( x e. _V , y e. _V |-> { <. f , g >. | ( f : ( Vtx ` x ) -1-1-onto-> ( Vtx ` y ) /\ g : dom ( iEdg ` x ) -1-1-onto-> dom ( iEdg ` y ) /\ A. i e. dom ( iEdg ` x ) ( f " ( ( iEdg ` x ) ` i ) ) = ( ( iEdg ` y ) ` ( g ` i ) ) ) } )