Metamath Proof Explorer

Theorem grimfn

Description: The graph isomorphism function is a well-defined function. (Contributed by AV, 28-Apr-2025)

Ref Expression
Assertion grimfn 
|- GraphIso Fn ( _V X. _V )

Proof

Step Hyp Ref Expression
1 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 ) ) ) ) } )
2 f1of 
 |-  ( f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h ) -> f : ( Vtx ` g ) --> ( Vtx ` h ) )
3 fvex 
 |-  ( Vtx ` h ) e. _V
4 fvex 
 |-  ( Vtx ` g ) e. _V
5 3 4 elmap 
 |-  ( f e. ( ( Vtx ` h ) ^m ( Vtx ` g ) ) <-> f : ( Vtx ` g ) --> ( Vtx ` h ) )
6 2 5 sylibr 
 |-  ( f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h ) -> f e. ( ( Vtx ` h ) ^m ( Vtx ` g ) ) )
7 6 adantr 
 |-  ( ( 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 ) ) ) ) -> f e. ( ( Vtx ` h ) ^m ( Vtx ` g ) ) )
8 ovex 
 |-  ( ( Vtx ` h ) ^m ( Vtx ` g ) ) e. _V
9 7 8 abex 
 |-  { 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 ) ) ) ) } e. _V
10 1 9 fnmpoi 
 |-  GraphIso Fn ( _V X. _V )