Metamath Proof Explorer

Theorem grlicsym

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

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

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 eqid 
 |-  ( Vtx ` S ) = ( Vtx ` S )
3 1 2 grilcbri 
 |-  ( G ~=lgr S -> E. f ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` S ) /\ A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( f ` v ) ) ) ) )
4 grlicrcl 
 |-  ( G ~=lgr S -> ( G e. _V /\ S e. _V ) )
5 vex 
 |-  f e. _V
6 cnvexg 
 |-  ( f e. _V -> `' f e. _V )
7 5 6 mp1i 
 |-  ( ( ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` S ) /\ A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( f ` v ) ) ) ) /\ G e. UHGraph ) -> `' f e. _V )
8 f1ocnv 
 |-  ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` S ) -> `' f : ( Vtx ` S ) -1-1-onto-> ( Vtx ` G ) )
9 8 ad2antrr 
 |-  ( ( ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` S ) /\ A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( f ` v ) ) ) ) /\ G e. UHGraph ) -> `' f : ( Vtx ` S ) -1-1-onto-> ( Vtx ` G ) )
10 f1ocnvdm 
 |-  ( ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` S ) /\ w e. ( Vtx ` S ) ) -> ( `' f ` w ) e. ( Vtx ` G ) )
11 10 3adant3 
 |-  ( ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` S ) /\ w e. ( Vtx ` S ) /\ G e. UHGraph ) -> ( `' f ` w ) e. ( Vtx ` G ) )
12 oveq2 
 |-  ( v = ( `' f ` w ) -> ( G ClNeighbVtx v ) = ( G ClNeighbVtx ( `' f ` w ) ) )
13 12 oveq2d 
 |-  ( v = ( `' f ` w ) -> ( G ISubGr ( G ClNeighbVtx v ) ) = ( G ISubGr ( G ClNeighbVtx ( `' f ` w ) ) ) )
14 fveq2 
 |-  ( v = ( `' f ` w ) -> ( f ` v ) = ( f ` ( `' f ` w ) ) )
15 14 oveq2d 
 |-  ( v = ( `' f ` w ) -> ( S ClNeighbVtx ( f ` v ) ) = ( S ClNeighbVtx ( f ` ( `' f ` w ) ) ) )
16 15 oveq2d 
 |-  ( v = ( `' f ` w ) -> ( S ISubGr ( S ClNeighbVtx ( f ` v ) ) ) = ( S ISubGr ( S ClNeighbVtx ( f ` ( `' f ` w ) ) ) ) )
17 13 16 breq12d 
 |-  ( v = ( `' f ` w ) -> ( ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( f ` v ) ) ) <-> ( G ISubGr ( G ClNeighbVtx ( `' f ` w ) ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( f ` ( `' f ` w ) ) ) ) ) )
18 17 rspcv 
 |-  ( ( `' f ` w ) e. ( Vtx ` G ) -> ( A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( f ` v ) ) ) -> ( G ISubGr ( G ClNeighbVtx ( `' f ` w ) ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( f ` ( `' f ` w ) ) ) ) ) )
19 11 18 syl 
 |-  ( ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` S ) /\ w e. ( Vtx ` S ) /\ G e. UHGraph ) -> ( A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( f ` v ) ) ) -> ( G ISubGr ( G ClNeighbVtx ( `' f ` w ) ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( f ` ( `' f ` w ) ) ) ) ) )
20 f1ocnvfv2 
 |-  ( ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` S ) /\ w e. ( Vtx ` S ) ) -> ( f ` ( `' f ` w ) ) = w )
21 20 3adant3 
 |-  ( ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` S ) /\ w e. ( Vtx ` S ) /\ G e. UHGraph ) -> ( f ` ( `' f ` w ) ) = w )
22 21 oveq2d 
 |-  ( ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` S ) /\ w e. ( Vtx ` S ) /\ G e. UHGraph ) -> ( S ClNeighbVtx ( f ` ( `' f ` w ) ) ) = ( S ClNeighbVtx w ) )
23 22 oveq2d 
 |-  ( ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` S ) /\ w e. ( Vtx ` S ) /\ G e. UHGraph ) -> ( S ISubGr ( S ClNeighbVtx ( f ` ( `' f ` w ) ) ) ) = ( S ISubGr ( S ClNeighbVtx w ) ) )
24 23 breq2d 
 |-  ( ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` S ) /\ w e. ( Vtx ` S ) /\ G e. UHGraph ) -> ( ( G ISubGr ( G ClNeighbVtx ( `' f ` w ) ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( f ` ( `' f ` w ) ) ) ) <-> ( G ISubGr ( G ClNeighbVtx ( `' f ` w ) ) ) ~=gr ( S ISubGr ( S ClNeighbVtx w ) ) ) )
25 simp3 
 |-  ( ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` S ) /\ w e. ( Vtx ` S ) /\ G e. UHGraph ) -> G e. UHGraph )
26 1 clnbgrssvtx 
 |-  ( G ClNeighbVtx ( `' f ` w ) ) C_ ( Vtx ` G )
27 1 isubgruhgr 
 |-  ( ( G e. UHGraph /\ ( G ClNeighbVtx ( `' f ` w ) ) C_ ( Vtx ` G ) ) -> ( G ISubGr ( G ClNeighbVtx ( `' f ` w ) ) ) e. UHGraph )
28 25 26 27 sylancl 
 |-  ( ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` S ) /\ w e. ( Vtx ` S ) /\ G e. UHGraph ) -> ( G ISubGr ( G ClNeighbVtx ( `' f ` w ) ) ) e. UHGraph )
29 gricsym 
 |-  ( ( G ISubGr ( G ClNeighbVtx ( `' f ` w ) ) ) e. UHGraph -> ( ( G ISubGr ( G ClNeighbVtx ( `' f ` w ) ) ) ~=gr ( S ISubGr ( S ClNeighbVtx w ) ) -> ( S ISubGr ( S ClNeighbVtx w ) ) ~=gr ( G ISubGr ( G ClNeighbVtx ( `' f ` w ) ) ) ) )
30 28 29 syl 
 |-  ( ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` S ) /\ w e. ( Vtx ` S ) /\ G e. UHGraph ) -> ( ( G ISubGr ( G ClNeighbVtx ( `' f ` w ) ) ) ~=gr ( S ISubGr ( S ClNeighbVtx w ) ) -> ( S ISubGr ( S ClNeighbVtx w ) ) ~=gr ( G ISubGr ( G ClNeighbVtx ( `' f ` w ) ) ) ) )
31 24 30 sylbid 
 |-  ( ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` S ) /\ w e. ( Vtx ` S ) /\ G e. UHGraph ) -> ( ( G ISubGr ( G ClNeighbVtx ( `' f ` w ) ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( f ` ( `' f ` w ) ) ) ) -> ( S ISubGr ( S ClNeighbVtx w ) ) ~=gr ( G ISubGr ( G ClNeighbVtx ( `' f ` w ) ) ) ) )
32 19 31 syld 
 |-  ( ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` S ) /\ w e. ( Vtx ` S ) /\ G e. UHGraph ) -> ( A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( f ` v ) ) ) -> ( S ISubGr ( S ClNeighbVtx w ) ) ~=gr ( G ISubGr ( G ClNeighbVtx ( `' f ` w ) ) ) ) )
33 32 3exp 
 |-  ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` S ) -> ( w e. ( Vtx ` S ) -> ( G e. UHGraph -> ( A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( f ` v ) ) ) -> ( S ISubGr ( S ClNeighbVtx w ) ) ~=gr ( G ISubGr ( G ClNeighbVtx ( `' f ` w ) ) ) ) ) ) )
34 33 com24 
 |-  ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` S ) -> ( A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( f ` v ) ) ) -> ( G e. UHGraph -> ( w e. ( Vtx ` S ) -> ( S ISubGr ( S ClNeighbVtx w ) ) ~=gr ( G ISubGr ( G ClNeighbVtx ( `' f ` w ) ) ) ) ) ) )
35 34 imp31 
 |-  ( ( ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` S ) /\ A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( f ` v ) ) ) ) /\ G e. UHGraph ) -> ( w e. ( Vtx ` S ) -> ( S ISubGr ( S ClNeighbVtx w ) ) ~=gr ( G ISubGr ( G ClNeighbVtx ( `' f ` w ) ) ) ) )
36 35 ralrimiv 
 |-  ( ( ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` S ) /\ A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( f ` v ) ) ) ) /\ G e. UHGraph ) -> A. w e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx w ) ) ~=gr ( G ISubGr ( G ClNeighbVtx ( `' f ` w ) ) ) )
37 9 36 jca 
 |-  ( ( ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` S ) /\ A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( f ` v ) ) ) ) /\ G e. UHGraph ) -> ( `' f : ( Vtx ` S ) -1-1-onto-> ( Vtx ` G ) /\ A. w e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx w ) ) ~=gr ( G ISubGr ( G ClNeighbVtx ( `' f ` w ) ) ) ) )
38 f1oeq1 
 |-  ( g = `' f -> ( g : ( Vtx ` S ) -1-1-onto-> ( Vtx ` G ) <-> `' f : ( Vtx ` S ) -1-1-onto-> ( Vtx ` G ) ) )
39 fveq1 
 |-  ( g = `' f -> ( g ` w ) = ( `' f ` w ) )
40 39 oveq2d 
 |-  ( g = `' f -> ( G ClNeighbVtx ( g ` w ) ) = ( G ClNeighbVtx ( `' f ` w ) ) )
41 40 oveq2d 
 |-  ( g = `' f -> ( G ISubGr ( G ClNeighbVtx ( g ` w ) ) ) = ( G ISubGr ( G ClNeighbVtx ( `' f ` w ) ) ) )
42 41 breq2d 
 |-  ( g = `' f -> ( ( S ISubGr ( S ClNeighbVtx w ) ) ~=gr ( G ISubGr ( G ClNeighbVtx ( g ` w ) ) ) <-> ( S ISubGr ( S ClNeighbVtx w ) ) ~=gr ( G ISubGr ( G ClNeighbVtx ( `' f ` w ) ) ) ) )
43 42 ralbidv 
 |-  ( g = `' f -> ( A. w e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx w ) ) ~=gr ( G ISubGr ( G ClNeighbVtx ( g ` w ) ) ) <-> A. w e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx w ) ) ~=gr ( G ISubGr ( G ClNeighbVtx ( `' f ` w ) ) ) ) )
44 38 43 anbi12d 
 |-  ( g = `' f -> ( ( g : ( Vtx ` S ) -1-1-onto-> ( Vtx ` G ) /\ A. w e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx w ) ) ~=gr ( G ISubGr ( G ClNeighbVtx ( g ` w ) ) ) ) <-> ( `' f : ( Vtx ` S ) -1-1-onto-> ( Vtx ` G ) /\ A. w e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx w ) ) ~=gr ( G ISubGr ( G ClNeighbVtx ( `' f ` w ) ) ) ) ) )
45 7 37 44 spcedv 
 |-  ( ( ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` S ) /\ A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( f ` v ) ) ) ) /\ G e. UHGraph ) -> E. g ( g : ( Vtx ` S ) -1-1-onto-> ( Vtx ` G ) /\ A. w e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx w ) ) ~=gr ( G ISubGr ( G ClNeighbVtx ( g ` w ) ) ) ) )
46 45 3adant3 
 |-  ( ( ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` S ) /\ A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( f ` v ) ) ) ) /\ G e. UHGraph /\ ( G e. _V /\ S e. _V ) ) -> E. g ( g : ( Vtx ` S ) -1-1-onto-> ( Vtx ` G ) /\ A. w e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx w ) ) ~=gr ( G ISubGr ( G ClNeighbVtx ( g ` w ) ) ) ) )
47 2 1 dfgrlic2 
 |-  ( ( S e. _V /\ G e. _V ) -> ( S ~=lgr G <-> E. g ( g : ( Vtx ` S ) -1-1-onto-> ( Vtx ` G ) /\ A. w e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx w ) ) ~=gr ( G ISubGr ( G ClNeighbVtx ( g ` w ) ) ) ) ) )
48 47 ancoms 
 |-  ( ( G e. _V /\ S e. _V ) -> ( S ~=lgr G <-> E. g ( g : ( Vtx ` S ) -1-1-onto-> ( Vtx ` G ) /\ A. w e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx w ) ) ~=gr ( G ISubGr ( G ClNeighbVtx ( g ` w ) ) ) ) ) )
49 48 3ad2ant3 
 |-  ( ( ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` S ) /\ A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( f ` v ) ) ) ) /\ G e. UHGraph /\ ( G e. _V /\ S e. _V ) ) -> ( S ~=lgr G <-> E. g ( g : ( Vtx ` S ) -1-1-onto-> ( Vtx ` G ) /\ A. w e. ( Vtx ` S ) ( S ISubGr ( S ClNeighbVtx w ) ) ~=gr ( G ISubGr ( G ClNeighbVtx ( g ` w ) ) ) ) ) )
50 46 49 mpbird 
 |-  ( ( ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` S ) /\ A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( f ` v ) ) ) ) /\ G e. UHGraph /\ ( G e. _V /\ S e. _V ) ) -> S ~=lgr G )
51 50 3exp 
 |-  ( ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` S ) /\ A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( f ` v ) ) ) ) -> ( G e. UHGraph -> ( ( G e. _V /\ S e. _V ) -> S ~=lgr G ) ) )
52 51 com23 
 |-  ( ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` S ) /\ A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( f ` v ) ) ) ) -> ( ( G e. _V /\ S e. _V ) -> ( G e. UHGraph -> S ~=lgr G ) ) )
53 52 exlimiv 
 |-  ( E. f ( f : ( Vtx ` G ) -1-1-onto-> ( Vtx ` S ) /\ A. v e. ( Vtx ` G ) ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( S ISubGr ( S ClNeighbVtx ( f ` v ) ) ) ) -> ( ( G e. _V /\ S e. _V ) -> ( G e. UHGraph -> S ~=lgr G ) ) )
54 3 4 53 sylc 
 |-  ( G ~=lgr S -> ( G e. UHGraph -> S ~=lgr G ) )
55 54 com12 
 |-  ( G e. UHGraph -> ( G ~=lgr S -> S ~=lgr G ) )