Definition df-acycgr

Description: Define the class of all acyclic graphs. A graph is calledacyclic if it has no (non-trivial) cycles. (Contributed by BTernaryTau, 11-Oct-2023)

	Ref	Expression
Assertion	df-acycgr	$$⊢\mathrm{AcyclicGraph}=\left\{g|\neg \exists f\exists p\left(f\mathrm{Cycles}\left(g\right)p\wedge f\ne \varnothing \right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cacycgr	$$class\mathrm{AcyclicGraph}$$
1		vg	$$setvarg$$
2		vf	$$setvarf$$
3		vp	$$setvarp$$
4	2	cv	$$setvarf$$
5		ccycls	$$class\mathrm{Cycles}$$
6	1	cv	$$setvarg$$
7	6 5	cfv	$$class\mathrm{Cycles}\left(g\right)$$
8	3	cv	$$setvarp$$
9	4 8 7	wbr	$$wfff\mathrm{Cycles}\left(g\right)p$$
10		c0	$$class\varnothing$$
11	4 10	wne	$$wfff\ne \varnothing$$
12	9 11	wa	$$wff\left(f\mathrm{Cycles}\left(g\right)p\wedge f\ne \varnothing \right)$$
13	12 3	wex	$$wff\exists p\left(f\mathrm{Cycles}\left(g\right)p\wedge f\ne \varnothing \right)$$
14	13 2	wex	$$wff\exists f\exists p\left(f\mathrm{Cycles}\left(g\right)p\wedge f\ne \varnothing \right)$$
15	14	wn	$$wff\neg \exists f\exists p\left(f\mathrm{Cycles}\left(g\right)p\wedge f\ne \varnothing \right)$$
16	15 1	cab	$$class\left\{g|\neg \exists f\exists p\left(f\mathrm{Cycles}\left(g\right)p\wedge f\ne \varnothing \right)\right\}$$
17	0 16	wceq	$$wff\mathrm{AcyclicGraph}=\left\{g|\neg \exists f\exists p\left(f\mathrm{Cycles}\left(g\right)p\wedge f\ne \varnothing \right)\right\}$$