Metamath Proof Explorer

Theorem isacycgr

Description: The property of being an acyclic graph. (Contributed by BTernaryTau, 11-Oct-2023)

Ref Expression
Assertion isacycgr ⊢ G ∈ W → G ∈ AcyclicGraph ↔ ¬ ∃ f ∃ p f Cycles ⁡ G p ∧ f ≠ ∅

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ g = G → Cycles ⁡ g = Cycles ⁡ G
2 1 breqd ⊢ g = G → f Cycles ⁡ g p ↔ f Cycles ⁡ G p
3 2 anbi1d ⊢ g = G → f Cycles ⁡ g p ∧ f ≠ ∅ ↔ f Cycles ⁡ G p ∧ f ≠ ∅
4 3 2exbidv ⊢ g = G → ∃ f ∃ p f Cycles ⁡ g p ∧ f ≠ ∅ ↔ ∃ f ∃ p f Cycles ⁡ G p ∧ f ≠ ∅
5 4 notbid ⊢ g = G → ¬ ∃ f ∃ p f Cycles ⁡ g p ∧ f ≠ ∅ ↔ ¬ ∃ f ∃ p f Cycles ⁡ G p ∧ f ≠ ∅
6 df-acycgr ⊢ AcyclicGraph = g | ¬ ∃ f ∃ p f Cycles ⁡ g p ∧ f ≠ ∅
7 5 6 elab2g ⊢ G ∈ W → G ∈ AcyclicGraph ↔ ¬ ∃ f ∃ p f Cycles ⁡ G p ∧ f ≠ ∅