Theorem dfacycgr1 35507

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 35506	. 2 ⊢ AcyclicGraph = {𝑔 ∣ ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅)}
2		2exanali 1883	. . . 4 ⊢ (¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ ¬ 𝑓 = ∅) ↔ ∀𝑓∀𝑝(𝑓(Cycles‘𝑔)𝑝 → 𝑓 = ∅))
3		df-ne 2961	. . . . . 6 ⊢ (𝑓 ≠ ∅ ↔ ¬ 𝑓 = ∅)
4	3	anbi2i 634	. . . . 5 ⊢ ((𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅) ↔ (𝑓(Cycles‘𝑔)𝑝 ∧ ¬ 𝑓 = ∅))
5	4	2exbii 1872	. . . 4 ⊢ (∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅) ↔ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ ¬ 𝑓 = ∅))
6	2, 5	xchnxbir 336	. . 3 ⊢ (¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅) ↔ ∀𝑓∀𝑝(𝑓(Cycles‘𝑔)𝑝 → 𝑓 = ∅))
7	6	abbii 2832	. 2 ⊢ {𝑔 ∣ ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅)} = {𝑔 ∣ ∀𝑓∀𝑝(𝑓(Cycles‘𝑔)𝑝 → 𝑓 = ∅)}
8	1, 7	eqtri 2788	1 ⊢ AcyclicGraph = {𝑔 ∣ ∀𝑓∀𝑝(𝑓(Cycles‘𝑔)𝑝 → 𝑓 = ∅)}

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400  ∀wal 1561   = wceq 1563  ∃wex 1802  {cab 2743   ≠ wne 2960  ∅c0 4288   class class class wbr 5105  ‘cfv 6525  Cyclesccycls 30043  AcyclicGraphcacycgr 35505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-ne 2961  df-acycgr 35506

This theorem is referenced by:  isacycgr1  35509