Metamath Proof Explorer

Theorem grlicref

Description: Graph local isomorphism is reflexive for hypergraphs. (Contributed by AV, 9-Jun-2025)

Ref Expression
Assertion grlicref 
|- ( G e. UHGraph -> G ~=lgr G )

Proof

Step Hyp Ref Expression
1 fvexd 
 |-  ( G e. UHGraph -> ( Vtx ` G ) e. _V )
2 1 resiexd 
 |-  ( G e. UHGraph -> ( _I |` ( Vtx ` G ) ) e. _V )
3 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
4 3 clnbgrssvtx 
 |-  ( G ClNeighbVtx v ) C_ ( Vtx ` G )
5 4 a1i 
 |-  ( v e. ( Vtx ` G ) -> ( G ClNeighbVtx v ) C_ ( Vtx ` G ) )
6 3 isubgruhgr 
 |-  ( ( G e. UHGraph /\ ( G ClNeighbVtx v ) C_ ( Vtx ` G ) ) -> ( G ISubGr ( G ClNeighbVtx v ) ) e. UHGraph )
7 5 6 sylan2 
 |-  ( ( G e. UHGraph /\ v e. ( Vtx ` G ) ) -> ( G ISubGr ( G ClNeighbVtx v ) ) e. UHGraph )
8 gricref 
 |-  ( ( G ISubGr ( G ClNeighbVtx v ) ) e. UHGraph -> ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( G ISubGr ( G ClNeighbVtx v ) ) )
9 7 8 syl 
 |-  ( ( G e. UHGraph /\ v e. ( Vtx ` G ) ) -> ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( G ISubGr ( G ClNeighbVtx v ) ) )
10 9 ralrimiva 
 |-  ( G e. UHGraph -> A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( G ISubGr ( G ClNeighbVtx v ) ) )
11 f1oi 
 |-  ( _I |` ( Vtx ` G ) ) : ( Vtx ` G ) -1-1-onto-> ( Vtx ` G )
12 10 11 jctil 
 |-  ( G e. UHGraph -> ( ( _I |` ( Vtx ` G ) ) : ( Vtx ` G ) -1-1-onto-> ( Vtx ` G ) /\ A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( G ISubGr ( G ClNeighbVtx v ) ) ) )
13 f1oeq1 
 |-  ( f = ( _I |` ( Vtx ` G ) ) -> ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` G ) <-> ( _I |` ( Vtx ` G ) ) : ( Vtx ` G ) -1-1-onto-> ( Vtx ` G ) ) )
14 fveq1 
 |-  ( f = ( _I |` ( Vtx ` G ) ) -> ( f ` v ) = ( ( _I |` ( Vtx ` G ) ) ` v ) )
15 14 oveq2d 
 |-  ( f = ( _I |` ( Vtx ` G ) ) -> ( G ClNeighbVtx ( f ` v ) ) = ( G ClNeighbVtx ( ( _I |` ( Vtx ` G ) ) ` v ) ) )
16 15 oveq2d 
 |-  ( f = ( _I |` ( Vtx ` G ) ) -> ( G ISubGr ( G ClNeighbVtx ( f ` v ) ) ) = ( G ISubGr ( G ClNeighbVtx ( ( _I |` ( Vtx ` G ) ) ` v ) ) ) )
17 16 breq2d 
 |-  ( f = ( _I |` ( Vtx ` G ) ) -> ( ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( G ISubGr ( G ClNeighbVtx ( f ` v ) ) ) <-> ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( G ISubGr ( G ClNeighbVtx ( ( _I |` ( Vtx ` G ) ) ` v ) ) ) ) )
18 fvresi 
 |-  ( v e. ( Vtx ` G ) -> ( ( _I |` ( Vtx ` G ) ) ` v ) = v )
19 18 oveq2d 
 |-  ( v e. ( Vtx ` G ) -> ( G ClNeighbVtx ( ( _I |` ( Vtx ` G ) ) ` v ) ) = ( G ClNeighbVtx v ) )
20 19 oveq2d 
 |-  ( v e. ( Vtx ` G ) -> ( G ISubGr ( G ClNeighbVtx ( ( _I |` ( Vtx ` G ) ) ` v ) ) ) = ( G ISubGr ( G ClNeighbVtx v ) ) )
21 20 breq2d 
 |-  ( v e. ( Vtx ` G ) -> ( ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( G ISubGr ( G ClNeighbVtx ( ( _I |` ( Vtx ` G ) ) ` v ) ) ) <-> ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( G ISubGr ( G ClNeighbVtx v ) ) ) )
22 17 21 sylan9bb 
 |-  ( ( f = ( _I |` ( Vtx ` G ) ) /\ v e. ( Vtx ` G ) ) -> ( ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( G ISubGr ( G ClNeighbVtx ( f ` v ) ) ) <-> ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( G ISubGr ( G ClNeighbVtx v ) ) ) )
23 22 ralbidva 
 |-  ( f = ( _I |` ( Vtx ` G ) ) -> ( A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( G ISubGr ( G ClNeighbVtx ( f ` v ) ) ) <-> A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( G ISubGr ( G ClNeighbVtx v ) ) ) )
24 13 23 anbi12d 
 |-  ( f = ( _I |` ( Vtx ` G ) ) -> ( ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` G ) /\ A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( G ISubGr ( G ClNeighbVtx ( f ` v ) ) ) ) <-> ( ( _I |` ( Vtx ` G ) ) : ( Vtx ` G ) -1-1-onto-> ( Vtx ` G ) /\ A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( G ISubGr ( G ClNeighbVtx v ) ) ) ) )
25 2 12 24 spcedv 
 |-  ( G e. UHGraph -> E. f ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` G ) /\ A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( G ISubGr ( G ClNeighbVtx ( f ` v ) ) ) ) )
26 3 3 dfgrlic2 
 |-  ( ( G e. UHGraph /\ G e. UHGraph ) -> ( G ~=lgr G <-> E. f ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` G ) /\ A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( G ISubGr ( G ClNeighbVtx ( f ` v ) ) ) ) ) )
27 26 anidms 
 |-  ( G e. UHGraph -> ( G ~=lgr G <-> E. f ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` G ) /\ A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( G ISubGr ( G ClNeighbVtx ( f ` v ) ) ) ) ) )
28 25 27 mpbird 
 |-  ( G e. UHGraph -> G ~=lgr G )