Theorem dfacycgr1

Description: An alternate definition of the class of all acyclic graphs that requires all cycles to be trivial. (Contributed by BTernaryTau, 11-Oct-2023)

	Ref	Expression
Assertion	dfacycgr1	⊢ AcyclicGraph = { 𝑔 ∣ ∀ 𝑓 ∀ 𝑝 ( 𝑓 ( Cycles ‘ 𝑔 ) 𝑝 → 𝑓 = ∅ ) }

Proof

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