Metamath Proof Explorer


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 ‘ 𝑔 ) 𝑝𝑓 = ∅ ) }