Metamath Proof Explorer


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 ‘ 𝑔 ) 𝑝𝑓 ≠ ∅ ) }