Metamath Proof Explorer

Theorem grilcbri2

Description: Implications of two graphs being locally isomorphic. (Contributed by AV, 9-Jun-2025)

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

Proof

Step Hyp Ref Expression
1 dfgrlic2.v 
 |-  V = ( Vtx ` G )
2 dfgrlic2.w 
 |-  W = ( Vtx ` H )
3 dfgrlic3.i 
 |-  I = ( iEdg ` G )
4 dfgrlic3.j 
 |-  J = ( iEdg ` H )
5 grilcbri2.n 
 |-  N = ( G ClNeighbVtx X )
6 grilcbri2.m 
 |-  M = ( H ClNeighbVtx ( f ` X ) )
7 grilcbri2.k 
 |-  K = { x e. dom I | ( I ` x ) C_ N }
8 grilcbri2.l 
 |-  L = { x e. dom J | ( J ` x ) C_ M }
9 brgrlic 
 |-  ( G ~=lgr H <-> ( G GraphLocIso H ) =/= (/) )
10 grlimdmrel 
 |-  Rel dom GraphLocIso
11 10 ovprc 
 |-  ( -. ( G e. _V /\ H e. _V ) -> ( G GraphLocIso H ) = (/) )
12 11 necon1ai 
 |-  ( ( G GraphLocIso H ) =/= (/) -> ( G e. _V /\ H e. _V ) )
13 9 12 sylbi 
 |-  ( G ~=lgr H -> ( G e. _V /\ H e. _V ) )
14 eqid 
 |-  ( G ClNeighbVtx v ) = ( G ClNeighbVtx v )
15 eqid 
 |-  ( H ClNeighbVtx ( f ` v ) ) = ( H ClNeighbVtx ( f ` v ) )
16 eqid 
 |-  { x e. dom I | ( I ` x ) C_ ( G ClNeighbVtx v ) } = { x e. dom I | ( I ` x ) C_ ( G ClNeighbVtx v ) }
17 eqid 
 |-  { x e. dom J | ( J ` x ) C_ ( H ClNeighbVtx ( f ` v ) ) } = { x e. dom J | ( J ` x ) C_ ( H ClNeighbVtx ( f ` v ) ) }
18 1 2 3 4 14 15 16 17 dfgrlic3 
 |-  ( ( G e. _V /\ H e. _V ) -> ( G ~=lgr H <-> E. f ( f : V -1-1-onto-> W /\ A. v e. V E. j ( j : ( G ClNeighbVtx v ) -1-1-onto-> ( H ClNeighbVtx ( f ` v ) ) /\ E. g ( g : { x e. dom I | ( I ` x ) C_ ( G ClNeighbVtx v ) } -1-1-onto-> { x e. dom J | ( J ` x ) C_ ( H ClNeighbVtx ( f ` v ) ) } /\ A. i e. { x e. dom I | ( I ` x ) C_ ( G ClNeighbVtx v ) } ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) ) )
19 eqidd 
 |-  ( v = X -> j = j )
20 oveq2 
 |-  ( v = X -> ( G ClNeighbVtx v ) = ( G ClNeighbVtx X ) )
21 20 5 eqtr4di 
 |-  ( v = X -> ( G ClNeighbVtx v ) = N )
22 fveq2 
 |-  ( v = X -> ( f ` v ) = ( f ` X ) )
23 22 oveq2d 
 |-  ( v = X -> ( H ClNeighbVtx ( f ` v ) ) = ( H ClNeighbVtx ( f ` X ) ) )
24 23 6 eqtr4di 
 |-  ( v = X -> ( H ClNeighbVtx ( f ` v ) ) = M )
25 19 21 24 f1oeq123d 
 |-  ( v = X -> ( j : ( G ClNeighbVtx v ) -1-1-onto-> ( H ClNeighbVtx ( f ` v ) ) <-> j : N -1-1-onto-> M ) )
26 eqidd 
 |-  ( v = X -> g = g )
27 21 sseq2d 
 |-  ( v = X -> ( ( I ` x ) C_ ( G ClNeighbVtx v ) <-> ( I ` x ) C_ N ) )
28 27 rabbidv 
 |-  ( v = X -> { x e. dom I | ( I ` x ) C_ ( G ClNeighbVtx v ) } = { x e. dom I | ( I ` x ) C_ N } )
29 28 7 eqtr4di 
 |-  ( v = X -> { x e. dom I | ( I ` x ) C_ ( G ClNeighbVtx v ) } = K )
30 24 sseq2d 
 |-  ( v = X -> ( ( J ` x ) C_ ( H ClNeighbVtx ( f ` v ) ) <-> ( J ` x ) C_ M ) )
31 30 rabbidv 
 |-  ( v = X -> { x e. dom J | ( J ` x ) C_ ( H ClNeighbVtx ( f ` v ) ) } = { x e. dom J | ( J ` x ) C_ M } )
32 31 8 eqtr4di 
 |-  ( v = X -> { x e. dom J | ( J ` x ) C_ ( H ClNeighbVtx ( f ` v ) ) } = L )
33 26 29 32 f1oeq123d 
 |-  ( v = X -> ( g : { x e. dom I | ( I ` x ) C_ ( G ClNeighbVtx v ) } -1-1-onto-> { x e. dom J | ( J ` x ) C_ ( H ClNeighbVtx ( f ` v ) ) } <-> g : K -1-1-onto-> L ) )
34 29 raleqdv 
 |-  ( v = X -> ( A. i e. { x e. dom I | ( I ` x ) C_ ( G ClNeighbVtx v ) } ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) <-> A. i e. K ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) )
35 33 34 anbi12d 
 |-  ( v = X -> ( ( g : { x e. dom I | ( I ` x ) C_ ( G ClNeighbVtx v ) } -1-1-onto-> { x e. dom J | ( J ` x ) C_ ( H ClNeighbVtx ( f ` v ) ) } /\ A. i e. { x e. dom I | ( I ` x ) C_ ( G ClNeighbVtx v ) } ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) <-> ( g : K -1-1-onto-> L /\ A. i e. K ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) )
36 35 exbidv 
 |-  ( v = X -> ( E. g ( g : { x e. dom I | ( I ` x ) C_ ( G ClNeighbVtx v ) } -1-1-onto-> { x e. dom J | ( J ` x ) C_ ( H ClNeighbVtx ( f ` v ) ) } /\ A. i e. { x e. dom I | ( I ` x ) C_ ( G ClNeighbVtx v ) } ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) <-> E. g ( g : K -1-1-onto-> L /\ A. i e. K ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) )
37 25 36 anbi12d 
 |-  ( v = X -> ( ( j : ( G ClNeighbVtx v ) -1-1-onto-> ( H ClNeighbVtx ( f ` v ) ) /\ E. g ( g : { x e. dom I | ( I ` x ) C_ ( G ClNeighbVtx v ) } -1-1-onto-> { x e. dom J | ( J ` x ) C_ ( H ClNeighbVtx ( f ` v ) ) } /\ A. i e. { x e. dom I | ( I ` x ) C_ ( G ClNeighbVtx v ) } ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) <-> ( j : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) )
38 37 exbidv 
 |-  ( v = X -> ( E. j ( j : ( G ClNeighbVtx v ) -1-1-onto-> ( H ClNeighbVtx ( f ` v ) ) /\ E. g ( g : { x e. dom I | ( I ` x ) C_ ( G ClNeighbVtx v ) } -1-1-onto-> { x e. dom J | ( J ` x ) C_ ( H ClNeighbVtx ( f ` v ) ) } /\ A. i e. { x e. dom I | ( I ` x ) C_ ( G ClNeighbVtx v ) } ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) <-> E. j ( j : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) )
39 38 rspcv 
 |-  ( X e. V -> ( A. v e. V E. j ( j : ( G ClNeighbVtx v ) -1-1-onto-> ( H ClNeighbVtx ( f ` v ) ) /\ E. g ( g : { x e. dom I | ( I ` x ) C_ ( G ClNeighbVtx v ) } -1-1-onto-> { x e. dom J | ( J ` x ) C_ ( H ClNeighbVtx ( f ` v ) ) } /\ A. i e. { x e. dom I | ( I ` x ) C_ ( G ClNeighbVtx v ) } ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) -> E. j ( j : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) )
40 39 com12 
 |-  ( A. v e. V E. j ( j : ( G ClNeighbVtx v ) -1-1-onto-> ( H ClNeighbVtx ( f ` v ) ) /\ E. g ( g : { x e. dom I | ( I ` x ) C_ ( G ClNeighbVtx v ) } -1-1-onto-> { x e. dom J | ( J ` x ) C_ ( H ClNeighbVtx ( f ` v ) ) } /\ A. i e. { x e. dom I | ( I ` x ) C_ ( G ClNeighbVtx v ) } ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) -> ( X e. V -> E. j ( j : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) )
41 40 a1i 
 |-  ( ( G e. _V /\ H e. _V ) -> ( A. v e. V E. j ( j : ( G ClNeighbVtx v ) -1-1-onto-> ( H ClNeighbVtx ( f ` v ) ) /\ E. g ( g : { x e. dom I | ( I ` x ) C_ ( G ClNeighbVtx v ) } -1-1-onto-> { x e. dom J | ( J ` x ) C_ ( H ClNeighbVtx ( f ` v ) ) } /\ A. i e. { x e. dom I | ( I ` x ) C_ ( G ClNeighbVtx v ) } ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) -> ( X e. V -> E. j ( j : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) ) )
42 41 anim2d 
 |-  ( ( G e. _V /\ H e. _V ) -> ( ( f : V -1-1-onto-> W /\ A. v e. V E. j ( j : ( G ClNeighbVtx v ) -1-1-onto-> ( H ClNeighbVtx ( f ` v ) ) /\ E. g ( g : { x e. dom I | ( I ` x ) C_ ( G ClNeighbVtx v ) } -1-1-onto-> { x e. dom J | ( J ` x ) C_ ( H ClNeighbVtx ( f ` v ) ) } /\ A. i e. { x e. dom I | ( I ` x ) C_ ( G ClNeighbVtx v ) } ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) -> ( f : V -1-1-onto-> W /\ ( X e. V -> E. j ( j : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) ) ) )
43 42 eximdv 
 |-  ( ( G e. _V /\ H e. _V ) -> ( E. f ( f : V -1-1-onto-> W /\ A. v e. V E. j ( j : ( G ClNeighbVtx v ) -1-1-onto-> ( H ClNeighbVtx ( f ` v ) ) /\ E. g ( g : { x e. dom I | ( I ` x ) C_ ( G ClNeighbVtx v ) } -1-1-onto-> { x e. dom J | ( J ` x ) C_ ( H ClNeighbVtx ( f ` v ) ) } /\ A. i e. { x e. dom I | ( I ` x ) C_ ( G ClNeighbVtx v ) } ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) -> E. f ( f : V -1-1-onto-> W /\ ( X e. V -> E. j ( j : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) ) ) )
44 18 43 sylbid 
 |-  ( ( G e. _V /\ H e. _V ) -> ( G ~=lgr H -> E. f ( f : V -1-1-onto-> W /\ ( X e. V -> E. j ( j : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) ) ) )
45 13 44 mpcom 
 |-  ( G ~=lgr H -> E. f ( f : V -1-1-onto-> W /\ ( X e. V -> E. j ( j : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) ) )