Definition df-acycgr 32409

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

Assertion

Ref	Expression
df-acycgr	⊢ AcyclicGraph = {𝑔 ∣ ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅)}

Distinct variable group:   𝑓,𝑔,𝑝

Detailed syntax breakdown of Definition df-acycgr

Step	Hyp	Ref	Expression
1		cacycgr 32408	. 2 class AcyclicGraph
2		vf	. . . . . . . . 9 setvar 𝑓
3	2	cv 1535	. . . . . . . 8 class 𝑓
4		vp	. . . . . . . . 9 setvar 𝑝
5	4	cv 1535	. . . . . . . 8 class 𝑝
6		vg	. . . . . . . . . 10 setvar 𝑔
7	6	cv 1535	. . . . . . . . 9 class 𝑔
8		ccycls 27562	. . . . . . . . 9 class Cycles
9	7, 8	cfv 6348	. . . . . . . 8 class (Cycles‘𝑔)
10	3, 5, 9	wbr 5059	. . . . . . 7 wff 𝑓(Cycles‘𝑔)𝑝
11		c0 4284	. . . . . . . 8 class ∅
12	3, 11	wne 3015	. . . . . . 7 wff 𝑓 ≠ ∅
13	10, 12	wa 398	. . . . . 6 wff (𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅)
14	13, 4	wex 1779	. . . . 5 wff ∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅)
15	14, 2	wex 1779	. . . 4 wff ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅)
16	15	wn 3	. . 3 wff ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅)
17	16, 6	cab 2798	. 2 class {𝑔 ∣ ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅)}
18	1, 17	wceq 1536	1 wff AcyclicGraph = {𝑔 ∣ ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅)}

This definition is referenced by:  dfacycgr1  32410  isacycgr  32411