Definition df-acycgr 35148

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 35147	. 2 class AcyclicGraph
2		vf	. . . . . . . . 9 setvar 𝑓
3	2	cv 1539	. . . . . . . 8 class 𝑓
4		vp	. . . . . . . . 9 setvar 𝑝
5	4	cv 1539	. . . . . . . 8 class 𝑝
6		vg	. . . . . . . . . 10 setvar 𝑔
7	6	cv 1539	. . . . . . . . 9 class 𝑔
8		ccycls 29805	. . . . . . . . 9 class Cycles
9	7, 8	cfv 6561	. . . . . . . 8 class (Cycles‘𝑔)
10	3, 5, 9	wbr 5143	. . . . . . 7 wff 𝑓(Cycles‘𝑔)𝑝
11		c0 4333	. . . . . . . 8 class ∅
12	3, 11	wne 2940	. . . . . . 7 wff 𝑓 ≠ ∅
13	10, 12	wa 395	. . . . . 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 2714	. 2 class {𝑔 ∣ ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅)}
18	1, 17	wceq 1540	1 wff AcyclicGraph = {𝑔 ∣ ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅)}

This definition is referenced by:  dfacycgr1  35149  isacycgr  35150