Metamath Proof Explorer

Theorem acycgrsubgr

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

Ref Expression
Assertion acycgrsubgr ⊢ G ∈ AcyclicGraph ∧ S SubGraph G → S ∈ AcyclicGraph

Proof

Step Hyp Ref Expression
1 subgrcycl ⊢ S SubGraph G → f Cycles ⁡ S p → f Cycles ⁡ G p
2 1 anim1d ⊢ S SubGraph G → f Cycles ⁡ S p ∧ f ≠ ∅ → f Cycles ⁡ G p ∧ f ≠ ∅
3 2 2eximdv ⊢ S SubGraph G → ∃ f ∃ p f Cycles ⁡ S p ∧ f ≠ ∅ → ∃ f ∃ p f Cycles ⁡ G p ∧ f ≠ ∅
4 3 con3d ⊢ S SubGraph G → ¬ ∃ f ∃ p f Cycles ⁡ G p ∧ f ≠ ∅ → ¬ ∃ f ∃ p f Cycles ⁡ S p ∧ f ≠ ∅
5 subgrv ⊢ S SubGraph G → S ∈ V ∧ G ∈ V
6 isacycgr ⊢ G ∈ V → G ∈ AcyclicGraph ↔ ¬ ∃ f ∃ p f Cycles ⁡ G p ∧ f ≠ ∅
7 5 6 simpl2im ⊢ S SubGraph G → G ∈ AcyclicGraph ↔ ¬ ∃ f ∃ p f Cycles ⁡ G p ∧ f ≠ ∅
8 5 simpld ⊢ S SubGraph G → S ∈ V
9 isacycgr ⊢ S ∈ V → S ∈ AcyclicGraph ↔ ¬ ∃ f ∃ p f Cycles ⁡ S p ∧ f ≠ ∅
10 8 9 syl ⊢ S SubGraph G → S ∈ AcyclicGraph ↔ ¬ ∃ f ∃ p f Cycles ⁡ S p ∧ f ≠ ∅
11 4 7 10 3imtr4d ⊢ S SubGraph G → G ∈ AcyclicGraph → S ∈ AcyclicGraph
12 11 impcom ⊢ G ∈ AcyclicGraph ∧ S SubGraph G → S ∈ AcyclicGraph