Theorem dfacycgr1 35142

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 35141	. 2 ⊢ AcyclicGraph = {𝑔 ∣ ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅)}
2		2exanali 1860	. . . 4 ⊢ (¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ ¬ 𝑓 = ∅) ↔ ∀𝑓∀𝑝(𝑓(Cycles‘𝑔)𝑝 → 𝑓 = ∅))
3		df-ne 2941	. . . . . 6 ⊢ (𝑓 ≠ ∅ ↔ ¬ 𝑓 = ∅)
4	3	anbi2i 623	. . . . 5 ⊢ ((𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅) ↔ (𝑓(Cycles‘𝑔)𝑝 ∧ ¬ 𝑓 = ∅))
5	4	2exbii 1848	. . . 4 ⊢ (∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅) ↔ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ ¬ 𝑓 = ∅))
6	2, 5	xchnxbir 333	. . 3 ⊢ (¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅) ↔ ∀𝑓∀𝑝(𝑓(Cycles‘𝑔)𝑝 → 𝑓 = ∅))
7	6	abbii 2809	. 2 ⊢ {𝑔 ∣ ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅)} = {𝑔 ∣ ∀𝑓∀𝑝(𝑓(Cycles‘𝑔)𝑝 → 𝑓 = ∅)}
8	1, 7	eqtri 2765	1 ⊢ AcyclicGraph = {𝑔 ∣ ∀𝑓∀𝑝(𝑓(Cycles‘𝑔)𝑝 → 𝑓 = ∅)}

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395  ∀wal 1537   = wceq 1539  ∃wex 1778  {cab 2714   ≠ wne 2940  ∅c0 4342   class class class wbr 5151  ‘cfv 6569  Cyclesccycls 29831  AcyclicGraphcacycgr 35140

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2065  df-clab 2715  df-cleq 2729  df-ne 2941  df-acycgr 35141

This theorem is referenced by:  isacycgr1  35144