Theorem dfacycgr1 35114

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 35113	. 2 ⊢ AcyclicGraph = {𝑔 ∣ ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅)}
2		2exanali 1859	. . . 4 ⊢ (¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ ¬ 𝑓 = ∅) ↔ ∀𝑓∀𝑝(𝑓(Cycles‘𝑔)𝑝 → 𝑓 = ∅))
3		df-ne 2947	. . . . . 6 ⊢ (𝑓 ≠ ∅ ↔ ¬ 𝑓 = ∅)
4	3	anbi2i 622	. . . . 5 ⊢ ((𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅) ↔ (𝑓(Cycles‘𝑔)𝑝 ∧ ¬ 𝑓 = ∅))
5	4	2exbii 1847	. . . 4 ⊢ (∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅) ↔ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ ¬ 𝑓 = ∅))
6	2, 5	xchnxbir 333	. . 3 ⊢ (¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅) ↔ ∀𝑓∀𝑝(𝑓(Cycles‘𝑔)𝑝 → 𝑓 = ∅))
7	6	abbii 2812	. 2 ⊢ {𝑔 ∣ ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅)} = {𝑔 ∣ ∀𝑓∀𝑝(𝑓(Cycles‘𝑔)𝑝 → 𝑓 = ∅)}
8	1, 7	eqtri 2768	1 ⊢ AcyclicGraph = {𝑔 ∣ ∀𝑓∀𝑝(𝑓(Cycles‘𝑔)𝑝 → 𝑓 = ∅)}

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395  ∀wal 1535   = wceq 1537  ∃wex 1777  {cab 2717   ≠ wne 2946  ∅c0 4352   class class class wbr 5166  ‘cfv 6575  Cyclesccycls 29823  AcyclicGraphcacycgr 35112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-ne 2947  df-acycgr 35113

This theorem is referenced by:  isacycgr1  35116