Metamath Proof Explorer

Theorem grlimfn

Description: The graph local isomorphism function is a well-defined function. (Contributed by AV, 20-May-2025)

Ref Expression
Assertion grlimfn 
|- GraphLocIso Fn ( _V X. _V )

Proof

Step Hyp Ref Expression
1 df-grlim 
 |-  GraphLocIso = ( g e. _V , h e. _V |-> { f | ( f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h ) /\ A. v e. ( Vtx ` g ) ( g ISubGr ( g ClNeighbVtx v ) ) ~=gr ( h ISubGr ( h ClNeighbVtx ( f ` v ) ) ) ) } )
2 fvex 
 |-  ( Vtx ` h ) e. _V
3 f1of 
 |-  ( f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h ) -> f : ( Vtx ` g ) --> ( Vtx ` h ) )
4 3 ad2antrl 
 |-  ( ( ( Vtx ` h ) e. _V /\ ( f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h ) /\ A. v e. ( Vtx ` g ) ( g ISubGr ( g ClNeighbVtx v ) ) ~=gr ( h ISubGr ( h ClNeighbVtx ( f ` v ) ) ) ) ) -> f : ( Vtx ` g ) --> ( Vtx ` h ) )
5 fvexd 
 |-  ( ( Vtx ` h ) e. _V -> ( Vtx ` g ) e. _V )
6 id 
 |-  ( ( Vtx ` h ) e. _V -> ( Vtx ` h ) e. _V )
7 4 5 6 fabexd 
 |-  ( ( Vtx ` h ) e. _V -> { f | ( f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h ) /\ A. v e. ( Vtx ` g ) ( g ISubGr ( g ClNeighbVtx v ) ) ~=gr ( h ISubGr ( h ClNeighbVtx ( f ` v ) ) ) ) } e. _V )
8 2 7 ax-mp 
 |-  { f | ( f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h ) /\ A. v e. ( Vtx ` g ) ( g ISubGr ( g ClNeighbVtx v ) ) ~=gr ( h ISubGr ( h ClNeighbVtx ( f ` v ) ) ) ) } e. _V
9 1 8 fnmpoi 
 |-  GraphLocIso Fn ( _V X. _V )