Step |
Hyp |
Ref |
Expression |
0 |
|
cacycgr |
⊢ AcyclicGraph |
1 |
|
vg |
⊢ 𝑔 |
2 |
|
vf |
⊢ 𝑓 |
3 |
|
vp |
⊢ 𝑝 |
4 |
2
|
cv |
⊢ 𝑓 |
5 |
|
ccycls |
⊢ Cycles |
6 |
1
|
cv |
⊢ 𝑔 |
7 |
6 5
|
cfv |
⊢ ( Cycles ‘ 𝑔 ) |
8 |
3
|
cv |
⊢ 𝑝 |
9 |
4 8 7
|
wbr |
⊢ 𝑓 ( Cycles ‘ 𝑔 ) 𝑝 |
10 |
|
c0 |
⊢ ∅ |
11 |
4 10
|
wne |
⊢ 𝑓 ≠ ∅ |
12 |
9 11
|
wa |
⊢ ( 𝑓 ( Cycles ‘ 𝑔 ) 𝑝 ∧ 𝑓 ≠ ∅ ) |
13 |
12 3
|
wex |
⊢ ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝑔 ) 𝑝 ∧ 𝑓 ≠ ∅ ) |
14 |
13 2
|
wex |
⊢ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝑔 ) 𝑝 ∧ 𝑓 ≠ ∅ ) |
15 |
14
|
wn |
⊢ ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝑔 ) 𝑝 ∧ 𝑓 ≠ ∅ ) |
16 |
15 1
|
cab |
⊢ { 𝑔 ∣ ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝑔 ) 𝑝 ∧ 𝑓 ≠ ∅ ) } |
17 |
0 16
|
wceq |
⊢ AcyclicGraph = { 𝑔 ∣ ¬ ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( Cycles ‘ 𝑔 ) 𝑝 ∧ 𝑓 ≠ ∅ ) } |