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

Theorem dfacycgr1 32622
 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 32621 . 2 AcyclicGraph = {𝑔 ∣ ¬ ∃𝑓𝑝(𝑓(Cycles‘𝑔)𝑝𝑓 ≠ ∅)}
2 2exanali 1861 . . . 4 (¬ ∃𝑓𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ ¬ 𝑓 = ∅) ↔ ∀𝑓𝑝(𝑓(Cycles‘𝑔)𝑝𝑓 = ∅))
3 df-ne 2952 . . . . . 6 (𝑓 ≠ ∅ ↔ ¬ 𝑓 = ∅)
43anbi2i 625 . . . . 5 ((𝑓(Cycles‘𝑔)𝑝𝑓 ≠ ∅) ↔ (𝑓(Cycles‘𝑔)𝑝 ∧ ¬ 𝑓 = ∅))
542exbii 1850 . . . 4 (∃𝑓𝑝(𝑓(Cycles‘𝑔)𝑝𝑓 ≠ ∅) ↔ ∃𝑓𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ ¬ 𝑓 = ∅))
62, 5xchnxbir 336 . . 3 (¬ ∃𝑓𝑝(𝑓(Cycles‘𝑔)𝑝𝑓 ≠ ∅) ↔ ∀𝑓𝑝(𝑓(Cycles‘𝑔)𝑝𝑓 = ∅))
76abbii 2823 . 2 {𝑔 ∣ ¬ ∃𝑓𝑝(𝑓(Cycles‘𝑔)𝑝𝑓 ≠ ∅)} = {𝑔 ∣ ∀𝑓𝑝(𝑓(Cycles‘𝑔)𝑝𝑓 = ∅)}
81, 7eqtri 2781 1 AcyclicGraph = {𝑔 ∣ ∀𝑓𝑝(𝑓(Cycles‘𝑔)𝑝𝑓 = ∅)}
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399  ∀wal 1536   = wceq 1538  ∃wex 1781  {cab 2735   ≠ wne 2951  ∅c0 4225   class class class wbr 5032  ‘cfv 6335  Cyclesccycls 27673  AcyclicGraphcacycgr 32620 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-ne 2952  df-acycgr 32621 This theorem is referenced by:  isacycgr1  32624
 Copyright terms: Public domain W3C validator