# 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}=\mathrm{Vtx}\left({G}\right)$
Assertion acycgr1v ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left|{V}\right|=1\right)\to {G}\in \mathrm{AcyclicGraph}$

### Proof

Step Hyp Ref Expression
1 acycgrv.1 ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 cyclispth ${⊢}{f}\mathrm{Cycles}\left({G}\right){p}\to {f}\mathrm{Paths}\left({G}\right){p}$
3 1 pthhashvtx ${⊢}{f}\mathrm{Paths}\left({G}\right){p}\to \left|{f}\right|\le \left|{V}\right|$
4 2 3 syl ${⊢}{f}\mathrm{Cycles}\left({G}\right){p}\to \left|{f}\right|\le \left|{V}\right|$
5 4 adantr ${⊢}\left({f}\mathrm{Cycles}\left({G}\right){p}\wedge \left|{V}\right|=1\right)\to \left|{f}\right|\le \left|{V}\right|$
6 breq2 ${⊢}\left|{V}\right|=1\to \left(\left|{f}\right|\le \left|{V}\right|↔\left|{f}\right|\le 1\right)$
7 6 adantl ${⊢}\left({f}\mathrm{Cycles}\left({G}\right){p}\wedge \left|{V}\right|=1\right)\to \left(\left|{f}\right|\le \left|{V}\right|↔\left|{f}\right|\le 1\right)$
8 5 7 mpbid ${⊢}\left({f}\mathrm{Cycles}\left({G}\right){p}\wedge \left|{V}\right|=1\right)\to \left|{f}\right|\le 1$
9 8 3adant1 ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {f}\mathrm{Cycles}\left({G}\right){p}\wedge \left|{V}\right|=1\right)\to \left|{f}\right|\le 1$
10 umgrn1cycl ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {f}\mathrm{Cycles}\left({G}\right){p}\right)\to \left|{f}\right|\ne 1$
11 10 3adant3 ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {f}\mathrm{Cycles}\left({G}\right){p}\wedge \left|{V}\right|=1\right)\to \left|{f}\right|\ne 1$
12 11 necomd ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {f}\mathrm{Cycles}\left({G}\right){p}\wedge \left|{V}\right|=1\right)\to 1\ne \left|{f}\right|$
13 cycliswlk ${⊢}{f}\mathrm{Cycles}\left({G}\right){p}\to {f}\mathrm{Walks}\left({G}\right){p}$
14 wlkcl ${⊢}{f}\mathrm{Walks}\left({G}\right){p}\to \left|{f}\right|\in {ℕ}_{0}$
15 14 nn0red ${⊢}{f}\mathrm{Walks}\left({G}\right){p}\to \left|{f}\right|\in ℝ$
16 1red ${⊢}{f}\mathrm{Walks}\left({G}\right){p}\to 1\in ℝ$
17 15 16 ltlend ${⊢}{f}\mathrm{Walks}\left({G}\right){p}\to \left(\left|{f}\right|<1↔\left(\left|{f}\right|\le 1\wedge 1\ne \left|{f}\right|\right)\right)$
18 13 17 syl ${⊢}{f}\mathrm{Cycles}\left({G}\right){p}\to \left(\left|{f}\right|<1↔\left(\left|{f}\right|\le 1\wedge 1\ne \left|{f}\right|\right)\right)$
19 18 3ad2ant2 ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {f}\mathrm{Cycles}\left({G}\right){p}\wedge \left|{V}\right|=1\right)\to \left(\left|{f}\right|<1↔\left(\left|{f}\right|\le 1\wedge 1\ne \left|{f}\right|\right)\right)$
20 9 12 19 mpbir2and ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {f}\mathrm{Cycles}\left({G}\right){p}\wedge \left|{V}\right|=1\right)\to \left|{f}\right|<1$
21 nn0lt10b ${⊢}\left|{f}\right|\in {ℕ}_{0}\to \left(\left|{f}\right|<1↔\left|{f}\right|=0\right)$
22 13 14 21 3syl ${⊢}{f}\mathrm{Cycles}\left({G}\right){p}\to \left(\left|{f}\right|<1↔\left|{f}\right|=0\right)$
23 22 3ad2ant2 ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {f}\mathrm{Cycles}\left({G}\right){p}\wedge \left|{V}\right|=1\right)\to \left(\left|{f}\right|<1↔\left|{f}\right|=0\right)$
24 20 23 mpbid ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {f}\mathrm{Cycles}\left({G}\right){p}\wedge \left|{V}\right|=1\right)\to \left|{f}\right|=0$
25 hasheq0 ${⊢}{f}\in \mathrm{V}\to \left(\left|{f}\right|=0↔{f}=\varnothing \right)$
26 25 elv ${⊢}\left|{f}\right|=0↔{f}=\varnothing$
27 24 26 sylib ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {f}\mathrm{Cycles}\left({G}\right){p}\wedge \left|{V}\right|=1\right)\to {f}=\varnothing$
28 27 3com23 ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left|{V}\right|=1\wedge {f}\mathrm{Cycles}\left({G}\right){p}\right)\to {f}=\varnothing$
29 28 3expia ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left|{V}\right|=1\right)\to \left({f}\mathrm{Cycles}\left({G}\right){p}\to {f}=\varnothing \right)$
30 29 alrimivv ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left|{V}\right|=1\right)\to \forall {f}\phantom{\rule{.4em}{0ex}}\forall {p}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{Cycles}\left({G}\right){p}\to {f}=\varnothing \right)$
31 isacycgr1 ${⊢}{G}\in \mathrm{UMGraph}\to \left({G}\in \mathrm{AcyclicGraph}↔\forall {f}\phantom{\rule{.4em}{0ex}}\forall {p}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{Cycles}\left({G}\right){p}\to {f}=\varnothing \right)\right)$
32 31 adantr ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left|{V}\right|=1\right)\to \left({G}\in \mathrm{AcyclicGraph}↔\forall {f}\phantom{\rule{.4em}{0ex}}\forall {p}\phantom{\rule{.4em}{0ex}}\left({f}\mathrm{Cycles}\left({G}\right){p}\to {f}=\varnothing \right)\right)$
33 30 32 mpbird ${⊢}\left({G}\in \mathrm{UMGraph}\wedge \left|{V}\right|=1\right)\to {G}\in \mathrm{AcyclicGraph}$