Mathbox for BTernaryTau < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-acycgr Structured version   Visualization version   GIF version

Definition df-acycgr 32394
 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
StepHypRef Expression
1 cacycgr 32393 . 2 class AcyclicGraph
2 vf . . . . . . . . 9 setvar 𝑓
32cv 1536 . . . . . . . 8 class 𝑓
4 vp . . . . . . . . 9 setvar 𝑝
54cv 1536 . . . . . . . 8 class 𝑝
6 vg . . . . . . . . . 10 setvar 𝑔
76cv 1536 . . . . . . . . 9 class 𝑔
8 ccycls 27549 . . . . . . . . 9 class Cycles
97, 8cfv 6327 . . . . . . . 8 class (Cycles‘𝑔)
103, 5, 9wbr 5038 . . . . . . 7 wff 𝑓(Cycles‘𝑔)𝑝
11 c0 4265 . . . . . . . 8 class
123, 11wne 3006 . . . . . . 7 wff 𝑓 ≠ ∅
1310, 12wa 398 . . . . . 6 wff (𝑓(Cycles‘𝑔)𝑝𝑓 ≠ ∅)
1413, 4wex 1780 . . . . 5 wff 𝑝(𝑓(Cycles‘𝑔)𝑝𝑓 ≠ ∅)
1514, 2wex 1780 . . . 4 wff 𝑓𝑝(𝑓(Cycles‘𝑔)𝑝𝑓 ≠ ∅)
1615wn 3 . . 3 wff ¬ ∃𝑓𝑝(𝑓(Cycles‘𝑔)𝑝𝑓 ≠ ∅)
1716, 6cab 2798 . 2 class {𝑔 ∣ ¬ ∃𝑓𝑝(𝑓(Cycles‘𝑔)𝑝𝑓 ≠ ∅)}
181, 17wceq 1537 1 wff AcyclicGraph = {𝑔 ∣ ¬ ∃𝑓𝑝(𝑓(Cycles‘𝑔)𝑝𝑓 ≠ ∅)}
 Colors of variables: wff setvar class This definition is referenced by:  dfacycgr1  32395  isacycgr  32396
 Copyright terms: Public domain W3C validator