Metamath Proof Explorer

Theorem uhgrimgrlim

Description: An isomorphism of hypergraphs is a local isomorphism between the two graphs. (Contributed by AV, 2-Jun-2025)

Ref Expression
Assertion uhgrimgrlim 
|- ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) -> F e. ( G GraphLocIso H ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 eqid 
 |-  ( Vtx ` H ) = ( Vtx ` H )
3 1 2 grimf1o 
 |-  ( F e. ( G GraphIso H ) -> F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) )
4 3 3ad2ant3 
 |-  ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) -> F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) )
5 simpl1 
 |-  ( ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) /\ v e. ( Vtx ` G ) ) -> G e. UHGraph )
6 simpl3 
 |-  ( ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) /\ v e. ( Vtx ` G ) ) -> F e. ( G GraphIso H ) )
7 1 clnbgrssvtx 
 |-  ( G ClNeighbVtx v ) C_ ( Vtx ` G )
8 7 a1i 
 |-  ( ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) /\ v e. ( Vtx ` G ) ) -> ( G ClNeighbVtx v ) C_ ( Vtx ` G ) )
9 1 uhgrimisgrgric 
 |-  ( ( G e. UHGraph /\ F e. ( G GraphIso H ) /\ ( G ClNeighbVtx v ) C_ ( Vtx ` G ) ) -> ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( F " ( G ClNeighbVtx v ) ) ) )
10 5 6 8 9 syl3anc 
 |-  ( ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) /\ v e. ( Vtx ` G ) ) -> ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( F " ( G ClNeighbVtx v ) ) ) )
11 df-3an 
 |-  ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) <-> ( ( G e. UHGraph /\ H e. UHGraph ) /\ F e. ( G GraphIso H ) ) )
12 1 clnbgrgrim 
 |-  ( ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ F e. ( G GraphIso H ) ) /\ v e. ( Vtx ` G ) ) -> ( H ClNeighbVtx ( F ` v ) ) = ( F " ( G ClNeighbVtx v ) ) )
13 11 12 sylanb 
 |-  ( ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) /\ v e. ( Vtx ` G ) ) -> ( H ClNeighbVtx ( F ` v ) ) = ( F " ( G ClNeighbVtx v ) ) )
14 13 oveq2d 
 |-  ( ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) /\ v e. ( Vtx ` G ) ) -> ( H ISubGr ( H ClNeighbVtx ( F ` v ) ) ) = ( H ISubGr ( F " ( G ClNeighbVtx v ) ) ) )
15 10 14 breqtrrd 
 |-  ( ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) /\ v e. ( Vtx ` G ) ) -> ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` v ) ) ) )
16 15 ralrimiva 
 |-  ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) -> A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` v ) ) ) )
17 1 2 isgrlim 
 |-  ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) -> ( F e. ( G GraphLocIso 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 ) ) ) ) ) )
18 4 16 17 mpbir2and 
 |-  ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) -> F e. ( G GraphLocIso H ) )