Users' Mathboxes 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 33404
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 33403 . 2 class AcyclicGraph
2 vf . . . . . . . . 9 setvar 𝑓
32cv 1539 . . . . . . . 8 class 𝑓
4 vp . . . . . . . . 9 setvar 𝑝
54cv 1539 . . . . . . . 8 class 𝑝
6 vg . . . . . . . . . 10 setvar 𝑔
76cv 1539 . . . . . . . . 9 class 𝑔
8 ccycls 28441 . . . . . . . . 9 class Cycles
97, 8cfv 6479 . . . . . . . 8 class (Cyclesβ€˜π‘”)
103, 5, 9wbr 5092 . . . . . . 7 wff 𝑓(Cyclesβ€˜π‘”)𝑝
11 c0 4269 . . . . . . . 8 class βˆ…
123, 11wne 2940 . . . . . . 7 wff 𝑓 β‰  βˆ…
1310, 12wa 396 . . . . . 6 wff (𝑓(Cyclesβ€˜π‘”)𝑝 ∧ 𝑓 β‰  βˆ…)
1413, 4wex 1780 . . . . 5 wff βˆƒπ‘(𝑓(Cyclesβ€˜π‘”)𝑝 ∧ 𝑓 β‰  βˆ…)
1514, 2wex 1780 . . . 4 wff βˆƒπ‘“βˆƒπ‘(𝑓(Cyclesβ€˜π‘”)𝑝 ∧ 𝑓 β‰  βˆ…)
1615wn 3 . . 3 wff Β¬ βˆƒπ‘“βˆƒπ‘(𝑓(Cyclesβ€˜π‘”)𝑝 ∧ 𝑓 β‰  βˆ…)
1716, 6cab 2713 . 2 class {𝑔 ∣ Β¬ βˆƒπ‘“βˆƒπ‘(𝑓(Cyclesβ€˜π‘”)𝑝 ∧ 𝑓 β‰  βˆ…)}
181, 17wceq 1540 1 wff AcyclicGraph = {𝑔 ∣ Β¬ βˆƒπ‘“βˆƒπ‘(𝑓(Cyclesβ€˜π‘”)𝑝 ∧ 𝑓 β‰  βˆ…)}
Colors of variables: wff setvar class
This definition is referenced by:  dfacycgr1  33405  isacycgr  33406
  Copyright terms: Public domain W3C validator