Metamath Proof Explorer

Theorem usgrexmpl12ngric

Description: The graphs H and G are not isomorphic ( H contains a triangle, see usgrexmpl1tri , whereas G does not, see usgrexmpl2trifr . (Contributed by AV, 10-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 usgrexmpl12ngric 
|- -. G ~=gr 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 6 7 ax-mp 
 |-  G e. UHGraph
9 gricsym 
 |-  ( G e. UHGraph -> ( G ~=gr H -> H ~=gr G ) )
10 8 9 ax-mp 
 |-  ( G ~=gr H -> H ~=gr G )
11 1 4 5 usgrexmpl1tri 
 |-  { 0 , 1 , 2 } e. ( GrTriangles ` H )
12 brgric 
 |-  ( H ~=gr G <-> ( H GraphIso G ) =/= (/) )
13 n0 
 |-  ( ( H GraphIso G ) =/= (/) <-> E. f f e. ( H GraphIso G ) )
14 12 13 bitri 
 |-  ( H ~=gr G <-> E. f f e. ( H GraphIso G ) )
15 1 2 3 usgrexmpl2trifr 
 |-  -. E. t t e. ( GrTriangles ` G )
16 1 4 5 usgrexmpl1 
 |-  H e. USGraph
17 usgruhgr 
 |-  ( H e. USGraph -> H e. UHGraph )
18 16 17 ax-mp 
 |-  H e. UHGraph
19 18 a1i 
 |-  ( ( f e. ( H GraphIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> H e. UHGraph )
20 8 a1i 
 |-  ( ( f e. ( H GraphIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> G e. UHGraph )
21 simpl 
 |-  ( ( f e. ( H GraphIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> f e. ( H GraphIso G ) )
22 simpr 
 |-  ( ( f e. ( H GraphIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> { 0 , 1 , 2 } e. ( GrTriangles ` H ) )
23 19 20 21 22 grimgrtri 
 |-  ( ( f e. ( H GraphIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> ( f " { 0 , 1 , 2 } ) e. ( GrTriangles ` G ) )
24 23 ex 
 |-  ( f e. ( H GraphIso G ) -> ( { 0 , 1 , 2 } e. ( GrTriangles ` H ) -> ( f " { 0 , 1 , 2 } ) e. ( GrTriangles ` G ) ) )
25 alnex 
 |-  ( A. t -. t e. ( GrTriangles ` G ) <-> -. E. t t e. ( GrTriangles ` G ) )
26 vex 
 |-  f e. _V
27 26 imaex 
 |-  ( f " { 0 , 1 , 2 } ) e. _V
28 id 
 |-  ( ( f " { 0 , 1 , 2 } ) e. _V -> ( f " { 0 , 1 , 2 } ) e. _V )
29 eleq1 
 |-  ( t = ( f " { 0 , 1 , 2 } ) -> ( t e. ( GrTriangles ` G ) <-> ( f " { 0 , 1 , 2 } ) e. ( GrTriangles ` G ) ) )
30 29 notbid 
 |-  ( t = ( f " { 0 , 1 , 2 } ) -> ( -. t e. ( GrTriangles ` G ) <-> -. ( f " { 0 , 1 , 2 } ) e. ( GrTriangles ` G ) ) )
31 30 adantl 
 |-  ( ( ( f " { 0 , 1 , 2 } ) e. _V /\ t = ( f " { 0 , 1 , 2 } ) ) -> ( -. t e. ( GrTriangles ` G ) <-> -. ( f " { 0 , 1 , 2 } ) e. ( GrTriangles ` G ) ) )
32 28 31 spcdv 
 |-  ( ( f " { 0 , 1 , 2 } ) e. _V -> ( A. t -. t e. ( GrTriangles ` G ) -> -. ( f " { 0 , 1 , 2 } ) e. ( GrTriangles ` G ) ) )
33 27 32 ax-mp 
 |-  ( A. t -. t e. ( GrTriangles ` G ) -> -. ( f " { 0 , 1 , 2 } ) e. ( GrTriangles ` G ) )
34 33 pm2.21d 
 |-  ( A. t -. t e. ( GrTriangles ` G ) -> ( ( f " { 0 , 1 , 2 } ) e. ( GrTriangles ` G ) -> -. G ~=gr H ) )
35 25 34 sylbir 
 |-  ( -. E. t t e. ( GrTriangles ` G ) -> ( ( f " { 0 , 1 , 2 } ) e. ( GrTriangles ` G ) -> -. G ~=gr H ) )
36 15 24 35 mpsylsyld 
 |-  ( f e. ( H GraphIso G ) -> ( { 0 , 1 , 2 } e. ( GrTriangles ` H ) -> -. G ~=gr H ) )
37 36 exlimiv 
 |-  ( E. f f e. ( H GraphIso G ) -> ( { 0 , 1 , 2 } e. ( GrTriangles ` H ) -> -. G ~=gr H ) )
38 14 37 sylbi 
 |-  ( H ~=gr G -> ( { 0 , 1 , 2 } e. ( GrTriangles ` H ) -> -. G ~=gr H ) )
39 10 11 38 mpisyl 
 |-  ( G ~=gr H -> -. G ~=gr H )
40 39 pm2.01i 
 |-  -. G ~=gr H