Metamath Proof Explorer

Theorem isgrlim

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

Ref Expression
Hypotheses isgrlim.v 
|- V = ( Vtx ` G )
isgrlim.w 
|- W = ( Vtx ` H )
Assertion 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 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isgrlim.v 
 |-  V = ( Vtx ` G )
2 isgrlim.w 
 |-  W = ( Vtx ` H )
3 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 ) ) ) ) } )
4 elex 
 |-  ( G e. X -> G e. _V )
5 4 3ad2ant1 
 |-  ( ( G e. X /\ H e. Y /\ F e. Z ) -> G e. _V )
6 elex 
 |-  ( H e. Y -> H e. _V )
7 6 3ad2ant2 
 |-  ( ( G e. X /\ H e. Y /\ F e. Z ) -> H e. _V )
8 f1of 
 |-  ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) -> f : ( Vtx ` G ) --> ( Vtx ` H ) )
9 8 adantr 
 |-  ( ( 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 ) )
10 9 adantl 
 |-  ( ( ( G e. X /\ H e. Y /\ F e. Z ) /\ ( 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 ) )
11 fvexd 
 |-  ( ( G e. X /\ H e. Y /\ F e. Z ) -> ( Vtx ` G ) e. _V )
12 fvexd 
 |-  ( ( G e. X /\ H e. Y /\ F e. Z ) -> ( Vtx ` H ) e. _V )
13 10 11 12 fabexd 
 |-  ( ( G e. X /\ H e. Y /\ F e. Z ) -> { 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 )
14 eqidd 
 |-  ( ( g = G /\ h = H ) -> f = f )
15 fveq2 
 |-  ( g = G -> ( Vtx ` g ) = ( Vtx ` G ) )
16 15 adantr 
 |-  ( ( g = G /\ h = H ) -> ( Vtx ` g ) = ( Vtx ` G ) )
17 fveq2 
 |-  ( h = H -> ( Vtx ` h ) = ( Vtx ` H ) )
18 17 adantl 
 |-  ( ( g = G /\ h = H ) -> ( Vtx ` h ) = ( Vtx ` H ) )
19 14 16 18 f1oeq123d 
 |-  ( ( g = G /\ h = H ) -> ( f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h ) <-> f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) )
20 id 
 |-  ( g = G -> g = G )
21 oveq1 
 |-  ( g = G -> ( g ClNeighbVtx v ) = ( G ClNeighbVtx v ) )
22 20 21 oveq12d 
 |-  ( g = G -> ( g ISubGr ( g ClNeighbVtx v ) ) = ( G ISubGr ( G ClNeighbVtx v ) ) )
23 id 
 |-  ( h = H -> h = H )
24 oveq1 
 |-  ( h = H -> ( h ClNeighbVtx ( f ` v ) ) = ( H ClNeighbVtx ( f ` v ) ) )
25 23 24 oveq12d 
 |-  ( h = H -> ( h ISubGr ( h ClNeighbVtx ( f ` v ) ) ) = ( H ISubGr ( H ClNeighbVtx ( f ` v ) ) ) )
26 22 25 breqan12d 
 |-  ( ( g = G /\ h = H ) -> ( ( g ISubGr ( g ClNeighbVtx v ) ) ~=gr ( h ISubGr ( h ClNeighbVtx ( f ` v ) ) ) <-> ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( f ` v ) ) ) ) )
27 16 26 raleqbidv 
 |-  ( ( g = G /\ h = H ) -> ( A. v e. ( Vtx ` g ) ( g ISubGr ( g ClNeighbVtx v ) ) ~=gr ( h ISubGr ( h ClNeighbVtx ( f ` v ) ) ) <-> A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( f ` v ) ) ) ) )
28 19 27 anbi12d 
 |-  ( ( g = G /\ h = H ) -> ( ( 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 ) -1-1-onto-> ( Vtx ` H ) /\ A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( f ` v ) ) ) ) ) )
29 28 abbidv 
 |-  ( ( g = G /\ h = H ) -> { 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 ) ) ) ) } = { 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 ) ) ) ) } )
30 3 5 7 13 29 elovmpod 
 |-  ( ( G e. X /\ H e. Y /\ F e. Z ) -> ( F e. ( G GraphLocIso H ) <-> F e. { 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 ) ) ) ) } ) )
31 f1oeq1 
 |-  ( f = F -> ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) <-> F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) )
32 fveq1 
 |-  ( f = F -> ( f ` v ) = ( F ` v ) )
33 32 oveq2d 
 |-  ( f = F -> ( H ClNeighbVtx ( f ` v ) ) = ( H ClNeighbVtx ( F ` v ) ) )
34 33 oveq2d 
 |-  ( f = F -> ( H ISubGr ( H ClNeighbVtx ( f ` v ) ) ) = ( H ISubGr ( H ClNeighbVtx ( F ` v ) ) ) )
35 34 breq2d 
 |-  ( f = F -> ( ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( f ` v ) ) ) <-> ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` v ) ) ) ) )
36 35 ralbidv 
 |-  ( f = F -> ( A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( f ` v ) ) ) <-> A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` v ) ) ) ) )
37 31 36 anbi12d 
 |-  ( f = 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 ) ) ) ) <-> ( 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 ) ) ) ) ) )
38 37 elabg 
 |-  ( F e. Z -> ( F e. { 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 ) ) ) ) } <-> ( 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 ) ) ) ) ) )
39 38 3ad2ant3 
 |-  ( ( G e. X /\ H e. Y /\ F e. Z ) -> ( F e. { 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 ) ) ) ) } <-> ( 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 ) ) ) ) ) )
40 f1oeq23 
 |-  ( ( V = ( Vtx ` G ) /\ W = ( Vtx ` H ) ) -> ( F : V -1-1-onto-> W <-> F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) )
41 1 2 40 mp2an 
 |-  ( F : V -1-1-onto-> W <-> F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) )
42 1 raleqi 
 |-  ( A. v e. V ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` v ) ) ) <-> A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` v ) ) ) )
43 41 42 anbi12i 
 |-  ( ( F : V -1-1-onto-> W /\ A. v e. V ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` 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 ) ) ) ) )
44 39 43 bitr4di 
 |-  ( ( G e. X /\ H e. Y /\ F e. Z ) -> ( F e. { 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 ) ) ) ) } <-> ( F : V -1-1-onto-> W /\ A. v e. V ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` v ) ) ) ) ) )
45 30 44 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 ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` v ) ) ) ) ) )