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 32384
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 32383 . 2 AcyclicGraph = {𝑔 ∣ ¬ ∃𝑓𝑝(𝑓(Cycles‘𝑔)𝑝𝑓 ≠ ∅)}
2 2exanali 1853 . . . 4 (¬ ∃𝑓𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ ¬ 𝑓 = ∅) ↔ ∀𝑓𝑝(𝑓(Cycles‘𝑔)𝑝𝑓 = ∅))
3 df-ne 3015 . . . . . 6 (𝑓 ≠ ∅ ↔ ¬ 𝑓 = ∅)
43anbi2i 624 . . . . 5 ((𝑓(Cycles‘𝑔)𝑝𝑓 ≠ ∅) ↔ (𝑓(Cycles‘𝑔)𝑝 ∧ ¬ 𝑓 = ∅))
542exbii 1842 . . . 4 (∃𝑓𝑝(𝑓(Cycles‘𝑔)𝑝𝑓 ≠ ∅) ↔ ∃𝑓𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ ¬ 𝑓 = ∅))
62, 5xchnxbir 335 . . 3 (¬ ∃𝑓𝑝(𝑓(Cycles‘𝑔)𝑝𝑓 ≠ ∅) ↔ ∀𝑓𝑝(𝑓(Cycles‘𝑔)𝑝𝑓 = ∅))
76abbii 2884 . 2 {𝑔 ∣ ¬ ∃𝑓𝑝(𝑓(Cycles‘𝑔)𝑝𝑓 ≠ ∅)} = {𝑔 ∣ ∀𝑓𝑝(𝑓(Cycles‘𝑔)𝑝𝑓 = ∅)}
81, 7eqtri 2842 1 AcyclicGraph = {𝑔 ∣ ∀𝑓𝑝(𝑓(Cycles‘𝑔)𝑝𝑓 = ∅)}
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 398  wal 1528   = wceq 1530  wex 1773  {cab 2797  wne 3014  c0 4289   class class class wbr 5057  cfv 6348  Cyclesccycls 27558  AcyclicGraphcacycgr 32382
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-9 2117  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1774  df-sb 2063  df-clab 2798  df-cleq 2812  df-ne 3015  df-acycgr 32383
This theorem is referenced by:  isacycgr1  32386
  Copyright terms: Public domain W3C validator