Metamath Proof Explorer

Theorem grlimprop2

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

Ref Expression
Hypotheses grlimprop.v 
|- V = ( Vtx ` G )
grlimprop.w 
|- W = ( Vtx ` H )
grlimprop2.n 
|- N = ( G ClNeighbVtx v )
grlimprop2.m 
|- M = ( H ClNeighbVtx ( F ` v ) )
grlimprop2.i 
|- I = ( iEdg ` G )
grlimprop2.j 
|- J = ( iEdg ` H )
grlimprop2.k 
|- K = { x e. dom I | ( I ` x ) C_ N }
grlimprop2.l 
|- L = { x e. dom J | ( J ` x ) C_ M }
Assertion grlimprop2 
|- ( 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 grlimprop.v 
 |-  V = ( Vtx ` G )
2 grlimprop.w 
 |-  W = ( Vtx ` H )
3 grlimprop2.n 
 |-  N = ( G ClNeighbVtx v )
4 grlimprop2.m 
 |-  M = ( H ClNeighbVtx ( F ` v ) )
5 grlimprop2.i 
 |-  I = ( iEdg ` G )
6 grlimprop2.j 
 |-  J = ( iEdg ` H )
7 grlimprop2.k 
 |-  K = { x e. dom I | ( I ` x ) C_ N }
8 grlimprop2.l 
 |-  L = { x e. dom J | ( J ` x ) C_ M }
9 grlimdmrel 
 |-  Rel dom GraphLocIso
10 9 ovrcl 
 |-  ( F e. ( G GraphLocIso H ) -> ( G e. _V /\ H e. _V ) )
11 id 
 |-  ( F e. ( G GraphLocIso H ) -> F e. ( G GraphLocIso H ) )
12 df-3an 
 |-  ( ( G e. _V /\ H e. _V /\ F e. ( G GraphLocIso H ) ) <-> ( ( G e. _V /\ H e. _V ) /\ F e. ( G GraphLocIso H ) ) )
13 10 11 12 sylanbrc 
 |-  ( F e. ( G GraphLocIso H ) -> ( G e. _V /\ H e. _V /\ F e. ( G GraphLocIso H ) ) )
14 1 2 3 4 5 6 7 8 isgrlim2 
 |-  ( ( 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 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 ) ) ) ) ) ) )
15 13 14 syl 
 |-  ( F e. ( G GraphLocIso H ) -> ( 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 ) ) ) ) ) ) )
16 15 ibi 
 |-  ( 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 ) ) ) ) ) )