Metamath Proof Explorer

Theorem usgrexmpl12ngrlic

Description: The graphs H and G are not locally isomorphic ( H contains a triangle, see usgrexmpl1tri , whereas G does not, see usgrexmpl2trifr . (Contributed by AV, 24-Aug-2025)

Ref Expression
Hypotheses usgrexmpl2.v 
|- V = ( 0 ... 5 )
usgrexmpl2.e 
|- E = <" { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } ">
usgrexmpl2.g 
|- G = <. V , E >.
usgrexmpl1.k 
|- K = <" { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ">
usgrexmpl1.h 
|- H = <. V , K >.
Assertion usgrexmpl12ngrlic 
|- -. G ~=lgr H

Proof

Step Hyp Ref Expression
1 usgrexmpl2.v 
 |-  V = ( 0 ... 5 )
2 usgrexmpl2.e 
 |-  E = <" { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } ">
3 usgrexmpl2.g 
 |-  G = <. V , E >.
4 usgrexmpl1.k 
 |-  K = <" { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ">
5 usgrexmpl1.h 
 |-  H = <. V , K >.
6 1 2 3 usgrexmpl2 
 |-  G e. USGraph
7 usgruhgr 
 |-  ( G e. USGraph -> G e. UHGraph )
8 grlicsym 
 |-  ( G e. UHGraph -> ( G ~=lgr H -> H ~=lgr G ) )
9 6 7 8 mp2b 
 |-  ( G ~=lgr H -> H ~=lgr G )
10 1 4 5 usgrexmpl1tri 
 |-  { 0 , 1 , 2 } e. ( GrTriangles ` H )
11 brgrlic 
 |-  ( H ~=lgr G <-> ( H GraphLocIso G ) =/= (/) )
12 n0 
 |-  ( ( H GraphLocIso G ) =/= (/) <-> E. f f e. ( H GraphLocIso G ) )
13 11 12 bitri 
 |-  ( H ~=lgr G <-> E. f f e. ( H GraphLocIso G ) )
14 1 2 3 usgrexmpl2trifr 
 |-  -. E. t t e. ( GrTriangles ` G )
15 1 4 5 usgrexmpl1 
 |-  H e. USGraph
16 usgruspgr 
 |-  ( H e. USGraph -> H e. USPGraph )
17 15 16 mp1i 
 |-  ( ( f e. ( H GraphLocIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> H e. USPGraph )
18 usgruspgr 
 |-  ( G e. USGraph -> G e. USPGraph )
19 6 18 mp1i 
 |-  ( ( f e. ( H GraphLocIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> G e. USPGraph )
20 simpl 
 |-  ( ( f e. ( H GraphLocIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> f e. ( H GraphLocIso G ) )
21 simpr 
 |-  ( ( f e. ( H GraphLocIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> { 0 , 1 , 2 } e. ( GrTriangles ` H ) )
22 17 19 20 21 grlimgrtri 
 |-  ( ( f e. ( H GraphLocIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> E. t t e. ( GrTriangles ` G ) )
23 22 ex 
 |-  ( f e. ( H GraphLocIso G ) -> ( { 0 , 1 , 2 } e. ( GrTriangles ` H ) -> E. t t e. ( GrTriangles ` G ) ) )
24 pm2.21 
 |-  ( -. E. t t e. ( GrTriangles ` G ) -> ( E. t t e. ( GrTriangles ` G ) -> -. G ~=lgr H ) )
25 14 23 24 mpsylsyld 
 |-  ( f e. ( H GraphLocIso G ) -> ( { 0 , 1 , 2 } e. ( GrTriangles ` H ) -> -. G ~=lgr H ) )
26 25 exlimiv 
 |-  ( E. f f e. ( H GraphLocIso G ) -> ( { 0 , 1 , 2 } e. ( GrTriangles ` H ) -> -. G ~=lgr H ) )
27 13 26 sylbi 
 |-  ( H ~=lgr G -> ( { 0 , 1 , 2 } e. ( GrTriangles ` H ) -> -. G ~=lgr H ) )
28 9 10 27 mpisyl 
 |-  ( G ~=lgr H -> -. G ~=lgr H )
29 28 pm2.01i 
 |-  -. G ~=lgr H