Metamath Proof Explorer

Theorem lgricngricex

Description: There are two different locally isomorphic graphs which are not isomorphic. (Contributed by AV, 23-Nov-2025)

Ref Expression
Assertion lgricngricex 
|- E. g E. h ( g ~=lgr h /\ -. g ~=gr h )

Proof

Step Hyp Ref Expression
1 gpg5grlic 
 |-  ( 5 gPetersenGr 1 ) ~=lgr ( 5 gPetersenGr 2 )
2 gpg5ngric 
 |-  -. ( 5 gPetersenGr 1 ) ~=gr ( 5 gPetersenGr 2 )
3 ovex 
 |-  ( 5 gPetersenGr 1 ) e. _V
4 ovex 
 |-  ( 5 gPetersenGr 2 ) e. _V
5 breq12 
 |-  ( ( g = ( 5 gPetersenGr 1 ) /\ h = ( 5 gPetersenGr 2 ) ) -> ( g ~=lgr h <-> ( 5 gPetersenGr 1 ) ~=lgr ( 5 gPetersenGr 2 ) ) )
6 breq12 
 |-  ( ( g = ( 5 gPetersenGr 1 ) /\ h = ( 5 gPetersenGr 2 ) ) -> ( g ~=gr h <-> ( 5 gPetersenGr 1 ) ~=gr ( 5 gPetersenGr 2 ) ) )
7 6 notbid 
 |-  ( ( g = ( 5 gPetersenGr 1 ) /\ h = ( 5 gPetersenGr 2 ) ) -> ( -. g ~=gr h <-> -. ( 5 gPetersenGr 1 ) ~=gr ( 5 gPetersenGr 2 ) ) )
8 5 7 anbi12d 
 |-  ( ( g = ( 5 gPetersenGr 1 ) /\ h = ( 5 gPetersenGr 2 ) ) -> ( ( g ~=lgr h /\ -. g ~=gr h ) <-> ( ( 5 gPetersenGr 1 ) ~=lgr ( 5 gPetersenGr 2 ) /\ -. ( 5 gPetersenGr 1 ) ~=gr ( 5 gPetersenGr 2 ) ) ) )
9 3 4 8 spc2ev 
 |-  ( ( ( 5 gPetersenGr 1 ) ~=lgr ( 5 gPetersenGr 2 ) /\ -. ( 5 gPetersenGr 1 ) ~=gr ( 5 gPetersenGr 2 ) ) -> E. g E. h ( g ~=lgr h /\ -. g ~=gr h ) )
10 1 2 9 mp2an 
 |-  E. g E. h ( g ~=lgr h /\ -. g ~=gr h )