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	|- AcyclicGraph = { g | -. E. f E. p ( f ( Cycles ` g ) p /\ f =/= (/) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cacycgr	|- AcyclicGraph
1		vg	|- g
2		vf	|- f
3		vp	|- p
4	2	cv	|- f
5		ccycls	|- Cycles
6	1	cv	|- g
7	6 5	cfv	|- ( Cycles ` g )
8	3	cv	|- p
9	4 8 7	wbr	|- f ( Cycles ` g ) p
10		c0	|- (/)
11	4 10	wne	|- f =/= (/)
12	9 11	wa	|- ( f ( Cycles ` g ) p /\ f =/= (/) )
13	12 3	wex	|- E. p ( f ( Cycles ` g ) p /\ f =/= (/) )
14	13 2	wex	|- E. f E. p ( f ( Cycles ` g ) p /\ f =/= (/) )
15	14	wn	|- -. E. f E. p ( f ( Cycles ` g ) p /\ f =/= (/) )
16	15 1	cab	|- { g | -. E. f E. p ( f ( Cycles ` g ) p /\ f =/= (/) ) }
17	0 16	wceq	|- AcyclicGraph = { g | -. E. f E. p ( f ( Cycles ` g ) p /\ f =/= (/) ) }