Metamath Proof Explorer

Theorem acycgr2v

Description: A simple graph with two vertices is an acyclic graph. (Contributed by BTernaryTau, 12-Oct-2023)

Ref Expression
Hypothesis acycgrv.1 ⊢ V = Vtx ⁡ G
Assertion acycgr2v ⊢ G ∈ USGraph ∧ V = 2 → G ∈ AcyclicGraph

Proof

Step Hyp Ref Expression
1 acycgrv.1 ⊢ V = Vtx ⁡ G
2 1 usgrcyclgt2v ⊢ G ∈ USGraph ∧ f Cycles ⁡ G p ∧ f ≠ ∅ → 2 < V
3 2re ⊢ 2 ∈ ℝ
4 3 rexri ⊢ 2 ∈ ℝ *
5 1 fvexi ⊢ V ∈ V
6 hashxrcl ⊢ V ∈ V → V ∈ ℝ *
7 5 6 ax-mp ⊢ V ∈ ℝ *
8 xrltne ⊢ 2 ∈ ℝ * ∧ V ∈ ℝ * ∧ 2 < V → V ≠ 2
9 4 7 8 mp3an12 ⊢ 2 < V → V ≠ 2
10 9 neneqd ⊢ 2 < V → ¬ V = 2
11 2 10 syl ⊢ G ∈ USGraph ∧ f Cycles ⁡ G p ∧ f ≠ ∅ → ¬ V = 2
12 11 3expib ⊢ G ∈ USGraph → f Cycles ⁡ G p ∧ f ≠ ∅ → ¬ V = 2
13 12 con2d ⊢ G ∈ USGraph → V = 2 → ¬ f Cycles ⁡ G p ∧ f ≠ ∅
14 13 imp ⊢ G ∈ USGraph ∧ V = 2 → ¬ f Cycles ⁡ G p ∧ f ≠ ∅
15 14 nexdv ⊢ G ∈ USGraph ∧ V = 2 → ¬ ∃ p f Cycles ⁡ G p ∧ f ≠ ∅
16 15 nexdv ⊢ G ∈ USGraph ∧ V = 2 → ¬ ∃ f ∃ p f Cycles ⁡ G p ∧ f ≠ ∅
17 isacycgr ⊢ G ∈ USGraph → G ∈ AcyclicGraph ↔ ¬ ∃ f ∃ p f Cycles ⁡ G p ∧ f ≠ ∅
18 17 adantr ⊢ G ∈ USGraph ∧ V = 2 → G ∈ AcyclicGraph ↔ ¬ ∃ f ∃ p f Cycles ⁡ G p ∧ f ≠ ∅
19 16 18 mpbird ⊢ G ∈ USGraph ∧ V = 2 → G ∈ AcyclicGraph