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 ‘ 𝐺 ) 𝑝 → 𝑓 = ∅ ) ) ) |