Metamath Proof Explorer

Theorem acycgr1v

Description: A multigraph with one vertex is an acyclic graph. (Contributed by BTernaryTau, 12-Oct-2023)

Ref Expression
Hypothesis acycgrv.1 ⊢ V = Vtx ⁡ G
Assertion acycgr1v ⊢ G ∈ UMGraph ∧ V = 1 → G ∈ AcyclicGraph

Proof

Step Hyp Ref Expression
1 acycgrv.1 ⊢ V = Vtx ⁡ G
2 cyclispth ⊢ f Cycles ⁡ G p → f Paths ⁡ G p
3 1 pthhashvtx ⊢ f Paths ⁡ G p → f ≤ V
4 2 3 syl ⊢ f Cycles ⁡ G p → f ≤ V
5 4 adantr ⊢ f Cycles ⁡ G p ∧ V = 1 → f ≤ V
6 breq2 ⊢ V = 1 → f ≤ V ↔ f ≤ 1
7 6 adantl ⊢ f Cycles ⁡ G p ∧ V = 1 → f ≤ V ↔ f ≤ 1
8 5 7 mpbid ⊢ f Cycles ⁡ G p ∧ V = 1 → f ≤ 1
9 8 3adant1 ⊢ G ∈ UMGraph ∧ f Cycles ⁡ G p ∧ V = 1 → f ≤ 1
10 umgrn1cycl ⊢ G ∈ UMGraph ∧ f Cycles ⁡ G p → f ≠ 1
11 10 3adant3 ⊢ G ∈ UMGraph ∧ f Cycles ⁡ G p ∧ V = 1 → f ≠ 1
12 11 necomd ⊢ G ∈ UMGraph ∧ f Cycles ⁡ G p ∧ V = 1 → 1 ≠ f
13 cycliswlk ⊢ f Cycles ⁡ G p → f Walks ⁡ G p
14 wlkcl ⊢ f Walks ⁡ G p → f ∈ ℕ 0
15 14 nn0red ⊢ f Walks ⁡ G p → f ∈ ℝ
16 1red ⊢ f Walks ⁡ G p → 1 ∈ ℝ
17 15 16 ltlend ⊢ f Walks ⁡ G p → f < 1 ↔ f ≤ 1 ∧ 1 ≠ f
18 13 17 syl ⊢ f Cycles ⁡ G p → f < 1 ↔ f ≤ 1 ∧ 1 ≠ f
19 18 3ad2ant2 ⊢ G ∈ UMGraph ∧ f Cycles ⁡ G p ∧ V = 1 → f < 1 ↔ f ≤ 1 ∧ 1 ≠ f
20 9 12 19 mpbir2and ⊢ G ∈ UMGraph ∧ f Cycles ⁡ G p ∧ V = 1 → f < 1
21 nn0lt10b ⊢ f ∈ ℕ 0 → f < 1 ↔ f = 0
22 13 14 21 3syl ⊢ f Cycles ⁡ G p → f < 1 ↔ f = 0
23 22 3ad2ant2 ⊢ G ∈ UMGraph ∧ f Cycles ⁡ G p ∧ V = 1 → f < 1 ↔ f = 0
24 20 23 mpbid ⊢ G ∈ UMGraph ∧ f Cycles ⁡ G p ∧ V = 1 → f = 0
25 hasheq0 ⊢ f ∈ V → f = 0 ↔ f = ∅
26 25 elv ⊢ f = 0 ↔ f = ∅
27 24 26 sylib ⊢ G ∈ UMGraph ∧ f Cycles ⁡ G p ∧ V = 1 → f = ∅
28 27 3com23 ⊢ G ∈ UMGraph ∧ V = 1 ∧ f Cycles ⁡ G p → f = ∅
29 28 3expia ⊢ G ∈ UMGraph ∧ V = 1 → f Cycles ⁡ G p → f = ∅
30 29 alrimivv ⊢ G ∈ UMGraph ∧ V = 1 → ∀ f ∀ p f Cycles ⁡ G p → f = ∅
31 isacycgr1 ⊢ G ∈ UMGraph → G ∈ AcyclicGraph ↔ ∀ f ∀ p f Cycles ⁡ G p → f = ∅
32 31 adantr ⊢ G ∈ UMGraph ∧ V = 1 → G ∈ AcyclicGraph ↔ ∀ f ∀ p f Cycles ⁡ G p → f = ∅
33 30 32 mpbird ⊢ G ∈ UMGraph ∧ V = 1 → G ∈ AcyclicGraph