Metamath Proof Explorer

Theorem pgn4cyclex

Description: A cycle in a Petersen graph does not have length 4. (Contributed by AV, 9-Nov-2025)

Ref Expression
Hypothesis pgn4cyclex.g 
|- G = ( 5 gPetersenGr 2 )
Assertion pgn4cyclex 
|- ( F ( Cycles ` G ) P -> ( # ` F ) =/= 4 )

Proof

Step Hyp Ref Expression
1 pgn4cyclex.g 
 |-  G = ( 5 gPetersenGr 2 )
2 pgjsgr 
 |-  ( 5 gPetersenGr 2 ) e. USGraph
3 1 2 eqeltri 
 |-  G e. USGraph
4 usgrupgr 
 |-  ( G e. USGraph -> G e. UPGraph )
5 3 4 ax-mp 
 |-  G e. UPGraph
6 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
7 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
8 6 7 upgr4cycl4dv4e 
 |-  ( ( G e. UPGraph /\ F ( Cycles ` G ) P /\ ( # ` F ) = 4 ) -> E. a e. ( Vtx ` G ) E. b e. ( Vtx ` G ) E. c e. ( Vtx ` G ) E. d e. ( Vtx ` G ) ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) )
9 5 8 mp3an1 
 |-  ( ( F ( Cycles ` G ) P /\ ( # ` F ) = 4 ) -> E. a e. ( Vtx ` G ) E. b e. ( Vtx ` G ) E. c e. ( Vtx ` G ) E. d e. ( Vtx ` G ) ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) )
10 7 nbusgreledg 
 |-  ( G e. USGraph -> ( a e. ( G NeighbVtx b ) <-> { a , b } e. ( Edg ` G ) ) )
11 10 bicomd 
 |-  ( G e. USGraph -> ( { a , b } e. ( Edg ` G ) <-> a e. ( G NeighbVtx b ) ) )
12 3 11 ax-mp 
 |-  ( { a , b } e. ( Edg ` G ) <-> a e. ( G NeighbVtx b ) )
13 12 biimpi 
 |-  ( { a , b } e. ( Edg ` G ) -> a e. ( G NeighbVtx b ) )
14 13 ad3antrrr 
 |-  ( ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) -> a e. ( G NeighbVtx b ) )
15 prcom 
 |-  { b , c } = { c , b }
16 15 eleq1i 
 |-  ( { b , c } e. ( Edg ` G ) <-> { c , b } e. ( Edg ` G ) )
17 16 biimpi 
 |-  ( { b , c } e. ( Edg ` G ) -> { c , b } e. ( Edg ` G ) )
18 7 nbusgreledg 
 |-  ( G e. USGraph -> ( c e. ( G NeighbVtx b ) <-> { c , b } e. ( Edg ` G ) ) )
19 3 18 ax-mp 
 |-  ( c e. ( G NeighbVtx b ) <-> { c , b } e. ( Edg ` G ) )
20 17 19 sylibr 
 |-  ( { b , c } e. ( Edg ` G ) -> c e. ( G NeighbVtx b ) )
21 20 ad3antlr 
 |-  ( ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) -> c e. ( G NeighbVtx b ) )
22 simprl2 
 |-  ( ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) -> a =/= c )
23 22 adantl 
 |-  ( ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( c e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) ) /\ ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) -> a =/= c )
24 eqid 
 |-  ( G NeighbVtx b ) = ( G NeighbVtx b )
25 1 6 7 24 pgnbgreunbgr 
 |-  ( ( a e. ( G NeighbVtx b ) /\ c e. ( G NeighbVtx b ) /\ a =/= c ) -> E! x e. ( Vtx ` G ) { { a , x } , { x , c } } C_ ( Edg ` G ) )
26 14 21 23 25 syl2an23an 
 |-  ( ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( c e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) ) /\ ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) -> E! x e. ( Vtx ` G ) { { a , x } , { x , c } } C_ ( Edg ` G ) )
27 simpll 
 |-  ( ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) -> ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) )
28 simplr 
 |-  ( ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) -> ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) )
29 simpr 
 |-  ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) -> b e. ( Vtx ` G ) )
30 simpr 
 |-  ( ( c e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) -> d e. ( Vtx ` G ) )
31 29 30 anim12i 
 |-  ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( c e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) ) -> ( b e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) )
32 simprr2 
 |-  ( ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) -> b =/= d )
33 31 32 anim12i 
 |-  ( ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( c e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) ) /\ ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) -> ( ( b e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) /\ b =/= d ) )
34 df-3an 
 |-  ( ( b e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) /\ b =/= d ) <-> ( ( b e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) /\ b =/= d ) )
35 33 34 sylibr 
 |-  ( ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( c e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) ) /\ ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) -> ( b e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) /\ b =/= d ) )
36 4cycl2vnunb 
 |-  ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) /\ ( b e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) /\ b =/= d ) ) -> -. E! x e. ( Vtx ` G ) { { a , x } , { x , c } } C_ ( Edg ` G ) )
37 27 28 35 36 syl2an23an 
 |-  ( ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( c e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) ) /\ ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) -> -. E! x e. ( Vtx ` G ) { { a , x } , { x , c } } C_ ( Edg ` G ) )
38 26 37 pm2.21dd 
 |-  ( ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( c e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) ) /\ ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) -> ( # ` F ) =/= 4 )
39 38 ex 
 |-  ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ ( c e. ( Vtx ` G ) /\ d e. ( Vtx ` G ) ) ) -> ( ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) -> ( # ` F ) =/= 4 ) )
40 39 rexlimdvva 
 |-  ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) -> ( E. c e. ( Vtx ` G ) E. d e. ( Vtx ` G ) ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) -> ( # ` F ) =/= 4 ) )
41 40 rexlimivv 
 |-  ( E. a e. ( Vtx ` G ) E. b e. ( Vtx ` G ) E. c e. ( Vtx ` G ) E. d e. ( Vtx ` G ) ( ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) /\ ( { c , d } e. ( Edg ` G ) /\ { d , a } e. ( Edg ` G ) ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) -> ( # ` F ) =/= 4 )
42 9 41 syl 
 |-  ( ( F ( Cycles ` G ) P /\ ( # ` F ) = 4 ) -> ( # ` F ) =/= 4 )
43 42 ex 
 |-  ( F ( Cycles ` G ) P -> ( ( # ` F ) = 4 -> ( # ` F ) =/= 4 ) )
44 neqne 
 |-  ( -. ( # ` F ) = 4 -> ( # ` F ) =/= 4 )
45 43 44 pm2.61d1 
 |-  ( F ( Cycles ` G ) P -> ( # ` F ) =/= 4 )