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 ( ( 𝐺 ∈ AcyclicGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ) → 𝐹 = ∅ )

Proof

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