Users' Mathboxes Mathbox for BTernaryTau < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dfacycgr1 Structured version   Visualization version   GIF version

Theorem dfacycgr1 34433
Description: An alternate definition of the class of all acyclic graphs that requires all cycles to be trivial. (Contributed by BTernaryTau, 11-Oct-2023.)
Assertion
Ref Expression
dfacycgr1 AcyclicGraph = {𝑔 ∣ βˆ€π‘“βˆ€π‘(𝑓(Cyclesβ€˜π‘”)𝑝 β†’ 𝑓 = βˆ…)}
Distinct variable group:   𝑓,𝑔,𝑝

Proof of Theorem dfacycgr1
StepHypRef Expression
1 df-acycgr 34432 . 2 AcyclicGraph = {𝑔 ∣ Β¬ βˆƒπ‘“βˆƒπ‘(𝑓(Cyclesβ€˜π‘”)𝑝 ∧ 𝑓 β‰  βˆ…)}
2 2exanali 1861 . . . 4 (Β¬ βˆƒπ‘“βˆƒπ‘(𝑓(Cyclesβ€˜π‘”)𝑝 ∧ Β¬ 𝑓 = βˆ…) ↔ βˆ€π‘“βˆ€π‘(𝑓(Cyclesβ€˜π‘”)𝑝 β†’ 𝑓 = βˆ…))
3 df-ne 2939 . . . . . 6 (𝑓 β‰  βˆ… ↔ Β¬ 𝑓 = βˆ…)
43anbi2i 621 . . . . 5 ((𝑓(Cyclesβ€˜π‘”)𝑝 ∧ 𝑓 β‰  βˆ…) ↔ (𝑓(Cyclesβ€˜π‘”)𝑝 ∧ Β¬ 𝑓 = βˆ…))
542exbii 1849 . . . 4 (βˆƒπ‘“βˆƒπ‘(𝑓(Cyclesβ€˜π‘”)𝑝 ∧ 𝑓 β‰  βˆ…) ↔ βˆƒπ‘“βˆƒπ‘(𝑓(Cyclesβ€˜π‘”)𝑝 ∧ Β¬ 𝑓 = βˆ…))
62, 5xchnxbir 332 . . 3 (Β¬ βˆƒπ‘“βˆƒπ‘(𝑓(Cyclesβ€˜π‘”)𝑝 ∧ 𝑓 β‰  βˆ…) ↔ βˆ€π‘“βˆ€π‘(𝑓(Cyclesβ€˜π‘”)𝑝 β†’ 𝑓 = βˆ…))
76abbii 2800 . 2 {𝑔 ∣ Β¬ βˆƒπ‘“βˆƒπ‘(𝑓(Cyclesβ€˜π‘”)𝑝 ∧ 𝑓 β‰  βˆ…)} = {𝑔 ∣ βˆ€π‘“βˆ€π‘(𝑓(Cyclesβ€˜π‘”)𝑝 β†’ 𝑓 = βˆ…)}
81, 7eqtri 2758 1 AcyclicGraph = {𝑔 ∣ βˆ€π‘“βˆ€π‘(𝑓(Cyclesβ€˜π‘”)𝑝 β†’ 𝑓 = βˆ…)}
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 394  βˆ€wal 1537   = wceq 1539  βˆƒwex 1779  {cab 2707   β‰  wne 2938  βˆ…c0 4321   class class class wbr 5147  β€˜cfv 6542  Cyclesccycls 29309  AcyclicGraphcacycgr 34431
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-ne 2939  df-acycgr 34432
This theorem is referenced by:  isacycgr1  34435
  Copyright terms: Public domain W3C validator