Metamath Proof Explorer

Theorem isacycgr1

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

Ref Expression
Assertion isacycgr1 ⊢ 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 imbi1d ⊢ g = G → f Cycles ⁡ g p → f = ∅ ↔ f Cycles ⁡ G p → f = ∅
4 3 2albidv ⊢ g = G → ∀ f ∀ p f Cycles ⁡ g p → f = ∅ ↔ ∀ f ∀ p f Cycles ⁡ G p → f = ∅
5 dfacycgr1 ⊢ AcyclicGraph = g | ∀ f ∀ p f Cycles ⁡ g p → f = ∅
6 4 5 elab2g ⊢ G ∈ W → G ∈ AcyclicGraph ↔ ∀ f ∀ p f Cycles ⁡ G p → f = ∅