This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem usgrlimprop

Description: Properties of a local isomorphism of simple pseudographs. (Contributed by AV, 17-Aug-2025)

Ref Expression
Hypotheses usgrlimprop.v 
|- V = ( Vtx ` G )
usgrlimprop.w 
|- W = ( Vtx ` H )
usgrlimprop.n 
|- N = ( G ClNeighbVtx v )
usgrlimprop.m 
|- M = ( H ClNeighbVtx ( F ` v ) )
usgrlimprop.i 
|- I = ( Edg ` G )
usgrlimprop.j 
|- J = ( Edg ` H )
usgrlimprop.k 
|- K = { x e. I | x C_ N }
usgrlimprop.l 
|- L = { x e. J | x C_ M }
Assertion usgrlimprop 
|- ( ( G e. USPGraph /\ H e. USPGraph /\ 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. e e. K ( f " e ) = ( g ` e ) ) ) ) )

Proof

Step Hyp Ref Expression
1 usgrlimprop.v 
 |-  V = ( Vtx ` G )
2 usgrlimprop.w 
 |-  W = ( Vtx ` H )
3 usgrlimprop.n 
 |-  N = ( G ClNeighbVtx v )
4 usgrlimprop.m 
 |-  M = ( H ClNeighbVtx ( F ` v ) )
5 usgrlimprop.i 
 |-  I = ( Edg ` G )
6 usgrlimprop.j 
 |-  J = ( Edg ` H )
7 usgrlimprop.k 
 |-  K = { x e. I | x C_ N }
8 usgrlimprop.l 
 |-  L = { x e. J | x C_ M }
9 simp3 
 |-  ( ( G e. USPGraph /\ H e. USPGraph /\ F e. ( G GraphLocIso H ) ) -> F e. ( G GraphLocIso H ) )
10 1 2 3 4 5 6 7 8 uspgrlim 
 |-  ( ( G e. USPGraph /\ H e. USPGraph /\ 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. e e. K ( f " e ) = ( g ` e ) ) ) ) ) )
11 9 10 mpbid 
 |-  ( ( G e. USPGraph /\ H e. USPGraph /\ 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. e e. K ( f " e ) = ( g ` e ) ) ) ) )