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 ⊢fCycles⁡Gp→fPaths⁡Gp
3 1 pthhashvtx ⊢fPaths⁡Gp→f≤V
4 2 3 syl ⊢fCycles⁡Gp→f≤V
5 4 adantr ⊢fCycles⁡Gp∧V=1→f≤V
6 breq2 ⊢V=1→f≤V↔f≤1
7 6 adantl ⊢fCycles⁡Gp∧V=1→f≤V↔f≤1
8 5 7 mpbid ⊢fCycles⁡Gp∧V=1→f≤1
9 8 3adant1 ⊢G∈UMGraph∧fCycles⁡Gp∧V=1→f≤1
10 umgrn1cycl ⊢G∈UMGraph∧fCycles⁡Gp→f≠1
11 10 3adant3 ⊢G∈UMGraph∧fCycles⁡Gp∧V=1→f≠1
12 11 necomd ⊢G∈UMGraph∧fCycles⁡Gp∧V=1→1≠f
13 cycliswlk ⊢fCycles⁡Gp→fWalks⁡Gp
14 wlkcl ⊢fWalks⁡Gp→f∈ℕ0
15 14 nn0red ⊢fWalks⁡Gp→f∈ℝ
16 1red ⊢fWalks⁡Gp→1∈ℝ
17 15 16 ltlend ⊢fWalks⁡Gp→f<1↔f≤1∧1≠f
18 13 17 syl ⊢fCycles⁡Gp→f<1↔f≤1∧1≠f
19 18 3ad2ant2 ⊢G∈UMGraph∧fCycles⁡Gp∧V=1→f<1↔f≤1∧1≠f
20 9 12 19 mpbir2and ⊢G∈UMGraph∧fCycles⁡Gp∧V=1→f<1
21 nn0lt10b ⊢f∈ℕ0→f<1↔f=0
22 13 14 21 3syl ⊢fCycles⁡Gp→f<1↔f=0
23 22 3ad2ant2 ⊢G∈UMGraph∧fCycles⁡Gp∧V=1→f<1↔f=0
24 20 23 mpbid ⊢G∈UMGraph∧fCycles⁡Gp∧V=1→f=0
25 hasheq0 ⊢f∈V→f=0↔f=∅
26 25 elv ⊢f=0↔f=∅
27 24 26 sylib ⊢G∈UMGraph∧fCycles⁡Gp∧V=1→f=∅
28 27 3com23 ⊢G∈UMGraph∧V=1∧fCycles⁡Gp→f=∅
29 28 3expia ⊢G∈UMGraph∧V=1→fCycles⁡Gp→f=∅
30 29 alrimivv ⊢G∈UMGraph∧V=1→∀f∀pfCycles⁡Gp→f=∅
31 isacycgr1 ⊢G∈UMGraph→G∈AcyclicGraph↔∀f∀pfCycles⁡Gp→f=∅
32 31 adantr ⊢G∈UMGraph∧V=1→G∈AcyclicGraph↔∀f∀pfCycles⁡Gp→f=∅
33 30 32 mpbird ⊢G∈UMGraph∧V=1→G∈AcyclicGraph