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