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 biimtrid ⊢ 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 imbitrrdi ⊢ 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