Theorem dfacycgr1 34135

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

Step	Hyp	Ref	Expression
1		df-acycgr 34134	. 2 ⊢ AcyclicGraph = {𝑔 ∣ ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅)}
2		2exanali 1864	. . . 4 ⊢ (¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ ¬ 𝑓 = ∅) ↔ ∀𝑓∀𝑝(𝑓(Cycles‘𝑔)𝑝 → 𝑓 = ∅))
3		df-ne 2942	. . . . . 6 ⊢ (𝑓 ≠ ∅ ↔ ¬ 𝑓 = ∅)
4	3	anbi2i 624	. . . . 5 ⊢ ((𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅) ↔ (𝑓(Cycles‘𝑔)𝑝 ∧ ¬ 𝑓 = ∅))
5	4	2exbii 1852	. . . 4 ⊢ (∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅) ↔ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ ¬ 𝑓 = ∅))
6	2, 5	xchnxbir 333	. . 3 ⊢ (¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅) ↔ ∀𝑓∀𝑝(𝑓(Cycles‘𝑔)𝑝 → 𝑓 = ∅))
7	6	abbii 2803	. 2 ⊢ {𝑔 ∣ ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅)} = {𝑔 ∣ ∀𝑓∀𝑝(𝑓(Cycles‘𝑔)𝑝 → 𝑓 = ∅)}
8	1, 7	eqtri 2761	1 ⊢ AcyclicGraph = {𝑔 ∣ ∀𝑓∀𝑝(𝑓(Cycles‘𝑔)𝑝 → 𝑓 = ∅)}

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397  ∀wal 1540   = wceq 1542  ∃wex 1782  {cab 2710   ≠ wne 2941  ∅c0 4323   class class class wbr 5149  ‘cfv 6544  Cyclesccycls 29042  AcyclicGraphcacycgr 34133

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-ne 2942  df-acycgr 34134

This theorem is referenced by:  isacycgr1  34137