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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion acycgr1v ( ( 𝐺 ∈ UMGraph ∧ ( ♯ ‘ 𝑉 ) = 1 ) → 𝐺 ∈ AcyclicGraph )

Proof

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