Metamath Proof Explorer


Theorem isacycgr1

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

Ref Expression
Assertion isacycgr1 ( 𝐺𝑊 → ( 𝐺 ∈ AcyclicGraph ↔ ∀ 𝑓𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝𝑓 = ∅ ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 ( 𝑔 = 𝐺 → ( Cycles ‘ 𝑔 ) = ( Cycles ‘ 𝐺 ) )
2 1 breqd ( 𝑔 = 𝐺 → ( 𝑓 ( Cycles ‘ 𝑔 ) 𝑝𝑓 ( Cycles ‘ 𝐺 ) 𝑝 ) )
3 2 imbi1d ( 𝑔 = 𝐺 → ( ( 𝑓 ( Cycles ‘ 𝑔 ) 𝑝𝑓 = ∅ ) ↔ ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝𝑓 = ∅ ) ) )
4 3 2albidv ( 𝑔 = 𝐺 → ( ∀ 𝑓𝑝 ( 𝑓 ( Cycles ‘ 𝑔 ) 𝑝𝑓 = ∅ ) ↔ ∀ 𝑓𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝𝑓 = ∅ ) ) )
5 dfacycgr1 AcyclicGraph = { 𝑔 ∣ ∀ 𝑓𝑝 ( 𝑓 ( Cycles ‘ 𝑔 ) 𝑝𝑓 = ∅ ) }
6 4 5 elab2g ( 𝐺𝑊 → ( 𝐺 ∈ AcyclicGraph ↔ ∀ 𝑓𝑝 ( 𝑓 ( Cycles ‘ 𝐺 ) 𝑝𝑓 = ∅ ) ) )