Metamath Proof Explorer

Definition df-grim

Description: An isomorphism between two graphs is a bijection between the sets of vertices of the two graphs that preserves adjacency, see definition in Diestel p. 3. (Contributed by AV, 19-Apr-2025)

Ref Expression
Assertion df-grim 
|- GraphIso = ( g e. _V , h e. _V |-> { f | ( f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h ) /\ E. j [. ( iEdg ` g ) / e ]. [. ( iEdg ` h ) / d ]. ( j : dom e -1-1-onto-> dom d /\ A. i e. dom e ( d ` ( j ` i ) ) = ( f " ( e ` i ) ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgrim 
 |-  GraphIso
1 vg 
 |-  g
2 cvv 
 |-  _V
3 vh 
 |-  h
4 vf 
 |-  f
5 4 cv 
 |-  f
6 cvtx 
 |-  Vtx
7 1 cv 
 |-  g
8 7 6 cfv 
 |-  ( Vtx ` g )
9 3 cv 
 |-  h
10 9 6 cfv 
 |-  ( Vtx ` h )
11 8 10 5 wf1o 
 |-  f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h )
12 vj 
 |-  j
13 ciedg 
 |-  iEdg
14 7 13 cfv 
 |-  ( iEdg ` g )
15 ve 
 |-  e
16 9 13 cfv 
 |-  ( iEdg ` h )
17 vd 
 |-  d
18 12 cv 
 |-  j
19 15 cv 
 |-  e
20 19 cdm 
 |-  dom e
21 17 cv 
 |-  d
22 21 cdm 
 |-  dom d
23 20 22 18 wf1o 
 |-  j : dom e -1-1-onto-> dom d
24 vi 
 |-  i
25 24 cv 
 |-  i
26 25 18 cfv 
 |-  ( j ` i )
27 26 21 cfv 
 |-  ( d ` ( j ` i ) )
28 25 19 cfv 
 |-  ( e ` i )
29 5 28 cima 
 |-  ( f " ( e ` i ) )
30 27 29 wceq 
 |-  ( d ` ( j ` i ) ) = ( f " ( e ` i ) )
31 30 24 20 wral 
 |-  A. i e. dom e ( d ` ( j ` i ) ) = ( f " ( e ` i ) )
32 23 31 wa 
 |-  ( j : dom e -1-1-onto-> dom d /\ A. i e. dom e ( d ` ( j ` i ) ) = ( f " ( e ` i ) ) )
33 32 17 16 wsbc 
 |-  [. ( iEdg ` h ) / d ]. ( j : dom e -1-1-onto-> dom d /\ A. i e. dom e ( d ` ( j ` i ) ) = ( f " ( e ` i ) ) )
34 33 15 14 wsbc 
 |-  [. ( iEdg ` g ) / e ]. [. ( iEdg ` h ) / d ]. ( j : dom e -1-1-onto-> dom d /\ A. i e. dom e ( d ` ( j ` i ) ) = ( f " ( e ` i ) ) )
35 34 12 wex 
 |-  E. j [. ( iEdg ` g ) / e ]. [. ( iEdg ` h ) / d ]. ( j : dom e -1-1-onto-> dom d /\ A. i e. dom e ( d ` ( j ` i ) ) = ( f " ( e ` i ) ) )
36 11 35 wa 
 |-  ( f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h ) /\ E. j [. ( iEdg ` g ) / e ]. [. ( iEdg ` h ) / d ]. ( j : dom e -1-1-onto-> dom d /\ A. i e. dom e ( d ` ( j ` i ) ) = ( f " ( e ` i ) ) ) )
37 36 4 cab 
 |-  { f | ( f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h ) /\ E. j [. ( iEdg ` g ) / e ]. [. ( iEdg ` h ) / d ]. ( j : dom e -1-1-onto-> dom d /\ A. i e. dom e ( d ` ( j ` i ) ) = ( f " ( e ` i ) ) ) ) }
38 1 3 2 2 37 cmpo 
 |-  ( g e. _V , h e. _V |-> { f | ( f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h ) /\ E. j [. ( iEdg ` g ) / e ]. [. ( iEdg ` h ) / d ]. ( j : dom e -1-1-onto-> dom d /\ A. i e. dom e ( d ` ( j ` i ) ) = ( f " ( e ` i ) ) ) ) } )
39 0 38 wceq 
 |-  GraphIso = ( g e. _V , h e. _V |-> { f | ( f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h ) /\ E. j [. ( iEdg ` g ) / e ]. [. ( iEdg ` h ) / d ]. ( j : dom e -1-1-onto-> dom d /\ A. i e. dom e ( d ` ( j ` i ) ) = ( f " ( e ` i ) ) ) ) } )