isacycgr

Description: The property of being an acyclic graph. (Contributed by BTernaryTau, 11-Oct-2023)

		Ref	Expression
	Assertion	isacycgr	$⊢ G \in W \to (G \in AcyclicGraph \leftrightarrow \neg \exists f \exists p (f Cycles (G) p \land f \neq \emptyset))$

Step	Hyp	Ref	Expression
1		fveq2	$⊢ g = G \to Cycles (g) = Cycles (G)$
2	1	breqd	$⊢ g = G \to (f Cycles (g) p \leftrightarrow f Cycles (G) p)$
3	2	anbi1d	$⊢ g = G \to ((f Cycles (g) p \land f \neq \emptyset) \leftrightarrow (f Cycles (G) p \land f \neq \emptyset))$
4	3	2exbidv	$⊢ g = G \to (\exists f \exists p (f Cycles (g) p \land f \neq \emptyset) \leftrightarrow \exists f \exists p (f Cycles (G) p \land f \neq \emptyset))$
5	4	notbid	$⊢ g = G \to (\neg \exists f \exists p (f Cycles (g) p \land f \neq \emptyset) \leftrightarrow \neg \exists f \exists p (f Cycles (G) p \land f \neq \emptyset))$
6		df-acycgr	$⊢ AcyclicGraph = \{g \| \neg \exists f \exists p (f Cycles (g) p \land f \neq \emptyset)\}$
7	5 6	elab2g	$⊢ G \in W \to (G \in AcyclicGraph \leftrightarrow \neg \exists f \exists p (f Cycles (G) p \land f \neq \emptyset))$

Metamath Proof Explorer