Metamath Proof Explorer

Theorem acycgrcycl

Description: Any cycle in an acyclic graph is trivial (i.e. has one vertex and no edges). (Contributed by BTernaryTau, 12-Oct-2023)

Ref Expression
Assertion acycgrcycl ⊢ G ∈ AcyclicGraph ∧ F Cycles ⁡ G P → F = ∅

Proof

Step Hyp Ref Expression
1 cycliswlk ⊢ F Cycles ⁡ G P → F Walks ⁡ G P
2 wlkv ⊢ F Walks ⁡ G P → G ∈ V ∧ F ∈ V ∧ P ∈ V
3 1 2 syl ⊢ F Cycles ⁡ G P → G ∈ V ∧ F ∈ V ∧ P ∈ V
4 3 simp2d ⊢ F Cycles ⁡ G P → F ∈ V
5 4 adantl ⊢ G ∈ AcyclicGraph ∧ F Cycles ⁡ G P → F ∈ V
6 3 simp3d ⊢ F Cycles ⁡ G P → P ∈ V
7 6 adantl ⊢ G ∈ AcyclicGraph ∧ F Cycles ⁡ G P → P ∈ V
8 breq1 ⊢ f = F → f Cycles ⁡ G p ↔ F Cycles ⁡ G p
9 eqeq1 ⊢ f = F → f = ∅ ↔ F = ∅
10 8 9 imbi12d ⊢ f = F → f Cycles ⁡ G p → f = ∅ ↔ F Cycles ⁡ G p → F = ∅
11 breq2 ⊢ p = P → F Cycles ⁡ G p ↔ F Cycles ⁡ G P
12 11 imbi1d ⊢ p = P → F Cycles ⁡ G p → F = ∅ ↔ F Cycles ⁡ G P → F = ∅
13 10 12 sylan9bb ⊢ f = F ∧ p = P → f Cycles ⁡ G p → f = ∅ ↔ F Cycles ⁡ G P → F = ∅
14 isacycgr1 ⊢ G ∈ AcyclicGraph → G ∈ AcyclicGraph ↔ ∀ f ∀ p f Cycles ⁡ G p → f = ∅
15 14 ibi ⊢ G ∈ AcyclicGraph → ∀ f ∀ p f Cycles ⁡ G p → f = ∅
16 15 19.21bbi ⊢ G ∈ AcyclicGraph → f Cycles ⁡ G p → f = ∅
17 16 adantr ⊢ G ∈ AcyclicGraph ∧ F Cycles ⁡ G P → f Cycles ⁡ G p → f = ∅
18 5 7 13 17 vtocl2d ⊢ G ∈ AcyclicGraph ∧ F Cycles ⁡ G P → F Cycles ⁡ G P → F = ∅
19 18 ex ⊢ G ∈ AcyclicGraph → F Cycles ⁡ G P → F Cycles ⁡ G P → F = ∅
20 19 pm2.43d ⊢ G ∈ AcyclicGraph → F Cycles ⁡ G P → F = ∅
21 20 imp ⊢ G ∈ AcyclicGraph ∧ F Cycles ⁡ G P → F = ∅