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 ‘ 𝐺 ) 𝑃 ) → 𝐹 = ∅ )