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 = { 𝑔 ∣ ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝑔 ) 𝑝 ∧ 𝑓 ≠ ∅ ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cacycgr	⊢ AcyclicGraph
1		vg	⊢ 𝑔
2		vf	⊢ 𝑓
3		vp	⊢ 𝑝
4	2	cv	⊢ 𝑓
5		ccycls	⊢ Cycles
6	1	cv	⊢ 𝑔
7	6 5	cfv	⊢ ( Cycles ‘ 𝑔 )
8	3	cv	⊢ 𝑝
9	4 8 7	wbr	⊢ 𝑓 ( Cycles ‘ 𝑔 ) 𝑝
10		c0	⊢ ∅
11	4 10	wne	⊢ 𝑓 ≠ ∅
12	9 11	wa	⊢ ( 𝑓 ( Cycles ‘ 𝑔 ) 𝑝 ∧ 𝑓 ≠ ∅ )
13	12 3	wex	⊢ ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝑔 ) 𝑝 ∧ 𝑓 ≠ ∅ )
14	13 2	wex	⊢ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝑔 ) 𝑝 ∧ 𝑓 ≠ ∅ )
15	14	wn	⊢ ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝑔 ) 𝑝 ∧ 𝑓 ≠ ∅ )
16	15 1	cab	⊢ { 𝑔 ∣ ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝑔 ) 𝑝 ∧ 𝑓 ≠ ∅ ) }
17	0 16	wceq	⊢ AcyclicGraph = { 𝑔 ∣ ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝑔 ) 𝑝 ∧ 𝑓 ≠ ∅ ) }