Metamath Proof Explorer

Theorem cusgr3cyclex

Description: Every complete simple graph with more than two vertices has a 3-cycle. (Contributed by BTernaryTau, 4-Oct-2023)

Ref Expression
Hypothesis cusgr3cyclex.1 
|- V = ( Vtx ` G )
Assertion cusgr3cyclex 
|- ( ( G e. ComplUSGraph /\ 2 < ( # ` V ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) )

Proof

Step Hyp Ref Expression
1 cusgr3cyclex.1 
 |-  V = ( Vtx ` G )
2 3anass 
 |-  ( ( a e. V /\ b e. V /\ c e. V ) <-> ( a e. V /\ ( b e. V /\ c e. V ) ) )
3 2 bianass 
 |-  ( ( G e. ComplUSGraph /\ ( a e. V /\ b e. V /\ c e. V ) ) <-> ( ( G e. ComplUSGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) )
4 cusgrusgr 
 |-  ( G e. ComplUSGraph -> G e. USGraph )
5 usgrumgr 
 |-  ( G e. USGraph -> G e. UMGraph )
6 4 5 syl 
 |-  ( G e. ComplUSGraph -> G e. UMGraph )
7 3simpc 
 |-  ( ( a e. V /\ b e. V /\ c e. V ) -> ( b e. V /\ c e. V ) )
8 7 ancli 
 |-  ( ( a e. V /\ b e. V /\ c e. V ) -> ( ( a e. V /\ b e. V /\ c e. V ) /\ ( b e. V /\ c e. V ) ) )
9 df-3an 
 |-  ( ( a =/= b /\ a =/= c /\ b =/= c ) <-> ( ( a =/= b /\ a =/= c ) /\ b =/= c ) )
10 9 biimpi 
 |-  ( ( a =/= b /\ a =/= c /\ b =/= c ) -> ( ( a =/= b /\ a =/= c ) /\ b =/= c ) )
11 an32 
 |-  ( ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( b e. V /\ c e. V ) ) /\ ( a =/= b /\ a =/= c ) ) <-> ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( a =/= b /\ a =/= c ) ) /\ ( b e. V /\ c e. V ) ) )
12 11 anbi1i 
 |-  ( ( ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( b e. V /\ c e. V ) ) /\ ( a =/= b /\ a =/= c ) ) /\ b =/= c ) <-> ( ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( a =/= b /\ a =/= c ) ) /\ ( b e. V /\ c e. V ) ) /\ b =/= c ) )
13 anass 
 |-  ( ( ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( a =/= b /\ a =/= c ) ) /\ ( b e. V /\ c e. V ) ) /\ b =/= c ) <-> ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( a =/= b /\ a =/= c ) ) /\ ( ( b e. V /\ c e. V ) /\ b =/= c ) ) )
14 12 13 sylbb 
 |-  ( ( ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( b e. V /\ c e. V ) ) /\ ( a =/= b /\ a =/= c ) ) /\ b =/= c ) -> ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( a =/= b /\ a =/= c ) ) /\ ( ( b e. V /\ c e. V ) /\ b =/= c ) ) )
15 14 anasss 
 |-  ( ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( b e. V /\ c e. V ) ) /\ ( ( a =/= b /\ a =/= c ) /\ b =/= c ) ) -> ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( a =/= b /\ a =/= c ) ) /\ ( ( b e. V /\ c e. V ) /\ b =/= c ) ) )
16 8 10 15 syl2an 
 |-  ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( a =/= b /\ a =/= c /\ b =/= c ) ) -> ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( a =/= b /\ a =/= c ) ) /\ ( ( b e. V /\ c e. V ) /\ b =/= c ) ) )
17 anandi3 
 |-  ( ( a e. V /\ b e. V /\ c e. V ) <-> ( ( a e. V /\ b e. V ) /\ ( a e. V /\ c e. V ) ) )
18 17 anbi1i 
 |-  ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( a =/= b /\ a =/= c ) ) <-> ( ( ( a e. V /\ b e. V ) /\ ( a e. V /\ c e. V ) ) /\ ( a =/= b /\ a =/= c ) ) )
19 an4 
 |-  ( ( ( ( a e. V /\ b e. V ) /\ ( a e. V /\ c e. V ) ) /\ ( a =/= b /\ a =/= c ) ) <-> ( ( ( a e. V /\ b e. V ) /\ a =/= b ) /\ ( ( a e. V /\ c e. V ) /\ a =/= c ) ) )
20 18 19 sylbb 
 |-  ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( a =/= b /\ a =/= c ) ) -> ( ( ( a e. V /\ b e. V ) /\ a =/= b ) /\ ( ( a e. V /\ c e. V ) /\ a =/= c ) ) )
21 df-3an 
 |-  ( ( a e. V /\ b e. V /\ a =/= b ) <-> ( ( a e. V /\ b e. V ) /\ a =/= b ) )
22 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
23 1 22 cusgredgex2 
 |-  ( G e. ComplUSGraph -> ( ( a e. V /\ b e. V /\ a =/= b ) -> { a , b } e. ( Edg ` G ) ) )
24 21 23 syl5bir 
 |-  ( G e. ComplUSGraph -> ( ( ( a e. V /\ b e. V ) /\ a =/= b ) -> { a , b } e. ( Edg ` G ) ) )
25 df-3an 
 |-  ( ( a e. V /\ c e. V /\ a =/= c ) <-> ( ( a e. V /\ c e. V ) /\ a =/= c ) )
26 1 22 cusgredgex2 
 |-  ( G e. ComplUSGraph -> ( ( a e. V /\ c e. V /\ a =/= c ) -> { a , c } e. ( Edg ` G ) ) )
27 25 26 syl5bir 
 |-  ( G e. ComplUSGraph -> ( ( ( a e. V /\ c e. V ) /\ a =/= c ) -> { a , c } e. ( Edg ` G ) ) )
28 24 27 anim12d 
 |-  ( G e. ComplUSGraph -> ( ( ( ( a e. V /\ b e. V ) /\ a =/= b ) /\ ( ( a e. V /\ c e. V ) /\ a =/= c ) ) -> ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) ) ) )
29 20 28 syl5 
 |-  ( G e. ComplUSGraph -> ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( a =/= b /\ a =/= c ) ) -> ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) ) ) )
30 df-3an 
 |-  ( ( b e. V /\ c e. V /\ b =/= c ) <-> ( ( b e. V /\ c e. V ) /\ b =/= c ) )
31 1 22 cusgredgex2 
 |-  ( G e. ComplUSGraph -> ( ( b e. V /\ c e. V /\ b =/= c ) -> { b , c } e. ( Edg ` G ) ) )
32 30 31 syl5bir 
 |-  ( G e. ComplUSGraph -> ( ( ( b e. V /\ c e. V ) /\ b =/= c ) -> { b , c } e. ( Edg ` G ) ) )
33 29 32 anim12d 
 |-  ( G e. ComplUSGraph -> ( ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( a =/= b /\ a =/= c ) ) /\ ( ( b e. V /\ c e. V ) /\ b =/= c ) ) -> ( ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) ) /\ { b , c } e. ( Edg ` G ) ) ) )
34 16 33 syl5 
 |-  ( G e. ComplUSGraph -> ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( a =/= b /\ a =/= c /\ b =/= c ) ) -> ( ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) ) /\ { b , c } e. ( Edg ` G ) ) ) )
35 3anan32 
 |-  ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) ) <-> ( ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) ) /\ { b , c } e. ( Edg ` G ) ) )
36 prcom 
 |-  { a , c } = { c , a }
37 36 eleq1i 
 |-  ( { a , c } e. ( Edg ` G ) <-> { c , a } e. ( Edg ` G ) )
38 37 3anbi3i 
 |-  ( ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) ) <-> ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , a } e. ( Edg ` G ) ) )
39 35 38 bitr3i 
 |-  ( ( ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) ) /\ { b , c } e. ( Edg ` G ) ) <-> ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , a } e. ( Edg ` G ) ) )
40 34 39 syl6ib 
 |-  ( G e. ComplUSGraph -> ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( a =/= b /\ a =/= c /\ b =/= c ) ) -> ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , a } e. ( Edg ` G ) ) ) )
41 pm5.3 
 |-  ( ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( a =/= b /\ a =/= c /\ b =/= c ) ) -> ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , a } e. ( Edg ` G ) ) ) <-> ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( a =/= b /\ a =/= c /\ b =/= c ) ) -> ( ( a e. V /\ b e. V /\ c e. V ) /\ ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , a } e. ( Edg ` G ) ) ) ) )
42 40 41 sylib 
 |-  ( G e. ComplUSGraph -> ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( a =/= b /\ a =/= c /\ b =/= c ) ) -> ( ( a e. V /\ b e. V /\ c e. V ) /\ ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , a } e. ( Edg ` G ) ) ) ) )
43 1 22 umgr3cyclex 
 |-  ( ( G e. UMGraph /\ ( a e. V /\ b e. V /\ c e. V ) /\ ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , a } e. ( Edg ` G ) ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = a ) )
44 3simpa 
 |-  ( ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = a ) -> ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) )
45 44 2eximi 
 |-  ( E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = a ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) )
46 43 45 syl 
 |-  ( ( G e. UMGraph /\ ( a e. V /\ b e. V /\ c e. V ) /\ ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , a } e. ( Edg ` G ) ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) )
47 46 3expib 
 |-  ( G e. UMGraph -> ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( { a , b } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) /\ { c , a } e. ( Edg ` G ) ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) ) )
48 6 42 47 sylsyld 
 |-  ( G e. ComplUSGraph -> ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( a =/= b /\ a =/= c /\ b =/= c ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) ) )
49 48 expdimp 
 |-  ( ( G e. ComplUSGraph /\ ( a e. V /\ b e. V /\ c e. V ) ) -> ( ( a =/= b /\ a =/= c /\ b =/= c ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) ) )
50 3 49 sylbir 
 |-  ( ( ( G e. ComplUSGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) -> ( ( a =/= b /\ a =/= c /\ b =/= c ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) ) )
51 50 reximdvva 
 |-  ( ( G e. ComplUSGraph /\ a e. V ) -> ( E. b e. V E. c e. V ( a =/= b /\ a =/= c /\ b =/= c ) -> E. b e. V E. c e. V E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) ) )
52 51 reximdva 
 |-  ( G e. ComplUSGraph -> ( E. a e. V E. b e. V E. c e. V ( a =/= b /\ a =/= c /\ b =/= c ) -> E. a e. V E. b e. V E. c e. V E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) ) )
53 id 
 |-  ( E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) )
54 53 rexlimivw 
 |-  ( E. c e. V E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) )
55 54 rexlimivw 
 |-  ( E. b e. V E. c e. V E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) )
56 55 rexlimivw 
 |-  ( E. a e. V E. b e. V E. c e. V E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) )
57 52 56 syl6 
 |-  ( G e. ComplUSGraph -> ( E. a e. V E. b e. V E. c e. V ( a =/= b /\ a =/= c /\ b =/= c ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) ) )
58 1 fvexi 
 |-  V e. _V
59 hashgt23el 
 |-  ( ( V e. _V /\ 2 < ( # ` V ) ) -> E. a e. V E. b e. V E. c e. V ( a =/= b /\ a =/= c /\ b =/= c ) )
60 58 59 mpan 
 |-  ( 2 < ( # ` V ) -> E. a e. V E. b e. V E. c e. V ( a =/= b /\ a =/= c /\ b =/= c ) )
61 57 60 impel 
 |-  ( ( G e. ComplUSGraph /\ 2 < ( # ` V ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) )