Metamath Proof Explorer

Theorem isgrlim2

Description: A local isomorphism of graphs is a bijection between their vertices that preserves neighborhoods. Definitions expanded. (Contributed by AV, 29-May-2025)

Ref Expression
Hypotheses isgrlim.v 
|- V = ( Vtx ` G )
isgrlim.w 
|- W = ( Vtx ` H )
isgrlim2.n 
|- N = ( G ClNeighbVtx v )
isgrlim2.m 
|- M = ( H ClNeighbVtx ( F ` v ) )
isgrlim2.i 
|- I = ( iEdg ` G )
isgrlim2.j 
|- J = ( iEdg ` H )
isgrlim2.k 
|- K = { x e. dom I | ( I ` x ) C_ N }
isgrlim2.l 
|- L = { x e. dom J | ( J ` x ) C_ M }
Assertion isgrlim2 
|- ( ( G e. X /\ H e. Y /\ F e. Z ) -> ( F e. ( G GraphLocIso H ) <-> ( F : V -1-1-onto-> W /\ A. v e. V E. f ( f : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isgrlim.v 
 |-  V = ( Vtx ` G )
2 isgrlim.w 
 |-  W = ( Vtx ` H )
3 isgrlim2.n 
 |-  N = ( G ClNeighbVtx v )
4 isgrlim2.m 
 |-  M = ( H ClNeighbVtx ( F ` v ) )
5 isgrlim2.i 
 |-  I = ( iEdg ` G )
6 isgrlim2.j 
 |-  J = ( iEdg ` H )
7 isgrlim2.k 
 |-  K = { x e. dom I | ( I ` x ) C_ N }
8 isgrlim2.l 
 |-  L = { x e. dom J | ( J ` x ) C_ M }
9 1 2 isgrlim 
 |-  ( ( G e. X /\ H e. Y /\ F e. Z ) -> ( 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 3 eqcomi 
 |-  ( G ClNeighbVtx v ) = N
11 10 oveq2i 
 |-  ( G ISubGr ( G ClNeighbVtx v ) ) = ( G ISubGr N )
12 4 eqcomi 
 |-  ( H ClNeighbVtx ( F ` v ) ) = M
13 12 oveq2i 
 |-  ( H ISubGr ( H ClNeighbVtx ( F ` v ) ) ) = ( H ISubGr M )
14 11 13 breq12i 
 |-  ( ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` v ) ) ) <-> ( G ISubGr N ) ~=gr ( H ISubGr M ) )
15 14 a1i 
 |-  ( ( G e. X /\ H e. Y /\ F e. Z ) -> ( ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` v ) ) ) <-> ( G ISubGr N ) ~=gr ( H ISubGr M ) ) )
16 5 6 3 4 7 8 clnbgrisubgrgrim 
 |-  ( ( G e. X /\ H e. Y ) -> ( ( G ISubGr N ) ~=gr ( H ISubGr M ) <-> E. f ( f : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) )
17 16 3adant3 
 |-  ( ( G e. X /\ H e. Y /\ F e. Z ) -> ( ( G ISubGr N ) ~=gr ( H ISubGr M ) <-> E. f ( f : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) )
18 15 17 bitrd 
 |-  ( ( G e. X /\ H e. Y /\ F e. Z ) -> ( ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` v ) ) ) <-> E. f ( f : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) )
19 18 ralbidv 
 |-  ( ( G e. X /\ H e. Y /\ F e. Z ) -> ( A. v e. V ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` v ) ) ) <-> A. v e. V E. f ( f : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) )
20 19 anbi2d 
 |-  ( ( G e. X /\ H e. Y /\ F e. Z ) -> ( ( F : V -1-1-onto-> W /\ A. v e. V ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` v ) ) ) ) <-> ( F : V -1-1-onto-> W /\ A. v e. V E. f ( f : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) ) )
21 9 20 bitrd 
 |-  ( ( G e. X /\ H e. Y /\ F e. Z ) -> ( F e. ( G GraphLocIso H ) <-> ( F : V -1-1-onto-> W /\ A. v e. V E. f ( f : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) ) )