acycgrsubgr

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

		Ref	Expression
	Assertion	acycgrsubgr	$⊢ (G \in AcyclicGraph \land S SubGraph G) \to S \in AcyclicGraph$

Step	Hyp	Ref	Expression
1		subgrcycl	$⊢ S SubGraph G \to (f Cycles (S) p \to f Cycles (G) p)$
2	1	anim1d	$⊢ S SubGraph G \to ((f Cycles (S) p \land f \neq \emptyset) \to (f Cycles (G) p \land f \neq \emptyset))$
3	2	2eximdv	$⊢ S SubGraph G \to (\exists f \exists p (f Cycles (S) p \land f \neq \emptyset) \to \exists f \exists p (f Cycles (G) p \land f \neq \emptyset))$
4	3	con3d	$⊢ S SubGraph G \to (\neg \exists f \exists p (f Cycles (G) p \land f \neq \emptyset) \to \neg \exists f \exists p (f Cycles (S) p \land f \neq \emptyset))$
5		subgrv	$⊢ S SubGraph G \to (S \in V \land G \in V)$
6		isacycgr	$⊢ G \in V \to (G \in AcyclicGraph \leftrightarrow \neg \exists f \exists p (f Cycles (G) p \land f \neq \emptyset))$
7	5 6	simpl2im	$⊢ S SubGraph G \to (G \in AcyclicGraph \leftrightarrow \neg \exists f \exists p (f Cycles (G) p \land f \neq \emptyset))$
8	5	simpld	$⊢ S SubGraph G \to S \in V$
9		isacycgr	$⊢ S \in V \to (S \in AcyclicGraph \leftrightarrow \neg \exists f \exists p (f Cycles (S) p \land f \neq \emptyset))$
10	8 9	syl	$⊢ S SubGraph G \to (S \in AcyclicGraph \leftrightarrow \neg \exists f \exists p (f Cycles (S) p \land f \neq \emptyset))$
11	4 7 10	3imtr4d	$⊢ S SubGraph G \to (G \in AcyclicGraph \to S \in AcyclicGraph)$
12	11	impcom	$⊢ (G \in AcyclicGraph \land S SubGraph G) \to S \in AcyclicGraph$

Metamath Proof Explorer