Metamath Proof Explorer

Theorem grlimprop

Description: Properties of a local isomorphism of graphs. (Contributed by AV, 21-May-2025)

Ref Expression
Hypotheses grlimprop.v 
|- V = ( Vtx ` G )
grlimprop.w 
|- W = ( Vtx ` H )
Assertion grlimprop 
|- ( F e. ( G GraphLocIso H ) -> ( F : V -1-1-onto-> W /\ A. v e. V ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` v ) ) ) ) )

Proof

Step Hyp Ref Expression
1 grlimprop.v 
 |-  V = ( Vtx ` G )
2 grlimprop.w 
 |-  W = ( Vtx ` H )
3 grlimdmrel 
 |-  Rel dom GraphLocIso
4 3 ovrcl 
 |-  ( F e. ( G GraphLocIso H ) -> ( G e. _V /\ H e. _V ) )
5 4 simpld 
 |-  ( F e. ( G GraphLocIso H ) -> G e. _V )
6 4 simprd 
 |-  ( F e. ( G GraphLocIso H ) -> H e. _V )
7 id 
 |-  ( F e. ( G GraphLocIso H ) -> F e. ( G GraphLocIso H ) )
8 5 6 7 3jca 
 |-  ( F e. ( G GraphLocIso H ) -> ( G e. _V /\ H e. _V /\ F e. ( G GraphLocIso H ) ) )
9 1 2 isgrlim 
 |-  ( ( G e. _V /\ H e. _V /\ F e. ( G GraphLocIso H ) ) -> ( F e. ( G GraphLocIso H ) <-> ( F : V -1-1-onto-> W /\ A. v e. V ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` v ) ) ) ) ) )
10 9 biimpd 
 |-  ( ( G e. _V /\ H e. _V /\ F e. ( G GraphLocIso H ) ) -> ( F e. ( G GraphLocIso H ) -> ( F : V -1-1-onto-> W /\ A. v e. V ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` v ) ) ) ) ) )
11 8 10 mpcom 
 |-  ( F e. ( G GraphLocIso H ) -> ( F : V -1-1-onto-> W /\ A. v e. V ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` v ) ) ) ) )