Metamath Proof Explorer

Theorem cusgracyclt3v

Description: A complete simple graph is acyclic if and only if it has fewer than three vertices. (Contributed by BTernaryTau, 20-Oct-2023)

Ref Expression
Hypothesis cusgracyclt3v.1 
|- V = ( Vtx ` G )
Assertion cusgracyclt3v 
|- ( G e. ComplUSGraph -> ( G e. AcyclicGraph <-> ( # ` V ) < 3 ) )

Proof

Step Hyp Ref Expression
1 cusgracyclt3v.1 
 |-  V = ( Vtx ` G )
2 isacycgr 
 |-  ( G e. ComplUSGraph -> ( G e. AcyclicGraph <-> -. E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) ) )
3 3nn0 
 |-  3 e. NN0
4 1 fvexi 
 |-  V e. _V
5 hashxnn0 
 |-  ( V e. _V -> ( # ` V ) e. NN0* )
6 4 5 ax-mp 
 |-  ( # ` V ) e. NN0*
7 xnn0lem1lt 
 |-  ( ( 3 e. NN0 /\ ( # ` V ) e. NN0* ) -> ( 3 <_ ( # ` V ) <-> ( 3 - 1 ) < ( # ` V ) ) )
8 3 6 7 mp2an 
 |-  ( 3 <_ ( # ` V ) <-> ( 3 - 1 ) < ( # ` V ) )
9 3re 
 |-  3 e. RR
10 9 rexri 
 |-  3 e. RR*
11 xnn0xr 
 |-  ( ( # ` V ) e. NN0* -> ( # ` V ) e. RR* )
12 6 11 ax-mp 
 |-  ( # ` V ) e. RR*
13 xrlenlt 
 |-  ( ( 3 e. RR* /\ ( # ` V ) e. RR* ) -> ( 3 <_ ( # ` V ) <-> -. ( # ` V ) < 3 ) )
14 10 12 13 mp2an 
 |-  ( 3 <_ ( # ` V ) <-> -. ( # ` V ) < 3 )
15 3m1e2 
 |-  ( 3 - 1 ) = 2
16 15 breq1i 
 |-  ( ( 3 - 1 ) < ( # ` V ) <-> 2 < ( # ` V ) )
17 8 14 16 3bitr3i 
 |-  ( -. ( # ` V ) < 3 <-> 2 < ( # ` V ) )
18 1 cusgr3cyclex 
 |-  ( ( G e. ComplUSGraph /\ 2 < ( # ` V ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) )
19 3ne0 
 |-  3 =/= 0
20 neeq1 
 |-  ( ( # ` f ) = 3 -> ( ( # ` f ) =/= 0 <-> 3 =/= 0 ) )
21 19 20 mpbiri 
 |-  ( ( # ` f ) = 3 -> ( # ` f ) =/= 0 )
22 hasheq0 
 |-  ( f e. _V -> ( ( # ` f ) = 0 <-> f = (/) ) )
23 22 elv 
 |-  ( ( # ` f ) = 0 <-> f = (/) )
24 23 necon3bii 
 |-  ( ( # ` f ) =/= 0 <-> f =/= (/) )
25 21 24 sylib 
 |-  ( ( # ` f ) = 3 -> f =/= (/) )
26 25 anim2i 
 |-  ( ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) -> ( f ( Cycles ` G ) p /\ f =/= (/) ) )
27 26 2eximi 
 |-  ( E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 3 ) -> E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) )
28 18 27 syl 
 |-  ( ( G e. ComplUSGraph /\ 2 < ( # ` V ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) )
29 28 ex 
 |-  ( G e. ComplUSGraph -> ( 2 < ( # ` V ) -> E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) ) )
30 17 29 syl5bi 
 |-  ( G e. ComplUSGraph -> ( -. ( # ` V ) < 3 -> E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) ) )
31 30 con1d 
 |-  ( G e. ComplUSGraph -> ( -. E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) -> ( # ` V ) < 3 ) )
32 2 31 sylbid 
 |-  ( G e. ComplUSGraph -> ( G e. AcyclicGraph -> ( # ` V ) < 3 ) )
33 cusgrusgr 
 |-  ( G e. ComplUSGraph -> G e. USGraph )
34 1 usgrcyclgt2v 
 |-  ( ( G e. USGraph /\ f ( Cycles ` G ) p /\ f =/= (/) ) -> 2 < ( # ` V ) )
35 34 3expib 
 |-  ( G e. USGraph -> ( ( f ( Cycles ` G ) p /\ f =/= (/) ) -> 2 < ( # ` V ) ) )
36 33 35 syl 
 |-  ( G e. ComplUSGraph -> ( ( f ( Cycles ` G ) p /\ f =/= (/) ) -> 2 < ( # ` V ) ) )
37 36 17 syl6ibr 
 |-  ( G e. ComplUSGraph -> ( ( f ( Cycles ` G ) p /\ f =/= (/) ) -> -. ( # ` V ) < 3 ) )
38 37 exlimdvv 
 |-  ( G e. ComplUSGraph -> ( E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) -> -. ( # ` V ) < 3 ) )
39 38 con2d 
 |-  ( G e. ComplUSGraph -> ( ( # ` V ) < 3 -> -. E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) ) )
40 39 2 sylibrd 
 |-  ( G e. ComplUSGraph -> ( ( # ` V ) < 3 -> G e. AcyclicGraph ) )
41 32 40 impbid 
 |-  ( G e. ComplUSGraph -> ( G e. AcyclicGraph <-> ( # ` V ) < 3 ) )