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 ComplUSGraph G AcyclicGraph V < 3

Proof

Step Hyp Ref Expression
1 cusgracyclt3v.1 V = Vtx G
2 isacycgr G ComplUSGraph G AcyclicGraph ¬ f p f Cycles G p f
3 3nn0 3 0
4 1 fvexi V V
5 hashxnn0 V V V 0 *
6 4 5 ax-mp V 0 *
7 xnn0lem1lt 3 0 V 0 * 3 V 3 1 < V
8 3 6 7 mp2an 3 V 3 1 < V
9 3re 3
10 9 rexri 3 *
11 xnn0xr V 0 * V *
12 6 11 ax-mp V *
13 xrlenlt 3 * V * 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 ComplUSGraph 2 < V f 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 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 f p f Cycles G p f = 3 f p f Cycles G p f
28 18 27 syl G ComplUSGraph 2 < V f p f Cycles G p f
29 28 ex G ComplUSGraph 2 < V f p f Cycles G p f
30 17 29 syl5bi G ComplUSGraph ¬ V < 3 f p f Cycles G p f
31 30 con1d G ComplUSGraph ¬ f p f Cycles G p f V < 3
32 2 31 sylbid G ComplUSGraph G AcyclicGraph V < 3
33 cusgrusgr G ComplUSGraph G USGraph
34 1 usgrcyclgt2v G USGraph f Cycles G p f 2 < V
35 34 3expib G USGraph f Cycles G p f 2 < V
36 33 35 syl G ComplUSGraph f Cycles G p f 2 < V
37 36 17 syl6ibr G ComplUSGraph f Cycles G p f ¬ V < 3
38 37 exlimdvv G ComplUSGraph f p f Cycles G p f ¬ V < 3
39 38 con2d G ComplUSGraph V < 3 ¬ f p f Cycles G p f
40 39 2 sylibrd G ComplUSGraph V < 3 G AcyclicGraph
41 32 40 impbid G ComplUSGraph G AcyclicGraph V < 3