Theorem acycgrsubgr

Description: The subgraph of an acyclic graph is also acyclic. (Contributed by BTernaryTau, 23-Oct-2023)

	Ref	Expression
Assertion	acycgrsubgr	⊢ ( ( 𝐺 ∈ AcyclicGraph ∧ 𝑆 SubGraph 𝐺 ) → 𝑆 ∈ AcyclicGraph )

Proof

Step	Hyp	Ref	Expression
1		subgrcycl	⊢ ( 𝑆 SubGraph 𝐺 → ( 𝑓 ( Cycles ‘ 𝑆 ) 𝑝 → 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ) )
2	1	anim1d	⊢ ( 𝑆 SubGraph 𝐺 → ( ( 𝑓 ( Cycles ‘ 𝑆 ) 𝑝 ∧ 𝑓 ≠ ∅ ) → ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) ) )
3	2	2eximdv	⊢ ( 𝑆 SubGraph 𝐺 → ( ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝑆 ) 𝑝 ∧ 𝑓 ≠ ∅ ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) ) )
4	3	con3d	⊢ ( 𝑆 SubGraph 𝐺 → ( ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) → ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝑆 ) 𝑝 ∧ 𝑓 ≠ ∅ ) ) )
5		subgrv	⊢ ( 𝑆 SubGraph 𝐺 → ( 𝑆 ∈ V ∧ 𝐺 ∈ V ) )
6		isacycgr	⊢ ( 𝐺 ∈ V → ( 𝐺 ∈ AcyclicGraph ↔ ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) ) )
7	5 6	simpl2im	⊢ ( 𝑆 SubGraph 𝐺 → ( 𝐺 ∈ AcyclicGraph ↔ ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ∧ 𝑓 ≠ ∅ ) ) )
8	5	simpld	⊢ ( 𝑆 SubGraph 𝐺 → 𝑆 ∈ V )
9		isacycgr	⊢ ( 𝑆 ∈ V → ( 𝑆 ∈ AcyclicGraph ↔ ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝑆 ) 𝑝 ∧ 𝑓 ≠ ∅ ) ) )
10	8 9	syl	⊢ ( 𝑆 SubGraph 𝐺 → ( 𝑆 ∈ AcyclicGraph ↔ ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝑆 ) 𝑝 ∧ 𝑓 ≠ ∅ ) ) )
11	4 7 10	3imtr4d	⊢ ( 𝑆 SubGraph 𝐺 → ( 𝐺 ∈ AcyclicGraph → 𝑆 ∈ AcyclicGraph ) )
12	11	impcom	⊢ ( ( 𝐺 ∈ AcyclicGraph ∧ 𝑆 SubGraph 𝐺 ) → 𝑆 ∈ AcyclicGraph )