Detailed syntax breakdown of Definition df-acycgr
Step | Hyp | Ref
| Expression |
1 | | cacycgr 33092 |
. 2
class
AcyclicGraph |
2 | | vf |
. . . . . . . . 9
setvar 𝑓 |
3 | 2 | cv 1541 |
. . . . . . . 8
class 𝑓 |
4 | | vp |
. . . . . . . . 9
setvar 𝑝 |
5 | 4 | cv 1541 |
. . . . . . . 8
class 𝑝 |
6 | | vg |
. . . . . . . . . 10
setvar 𝑔 |
7 | 6 | cv 1541 |
. . . . . . . . 9
class 𝑔 |
8 | | ccycls 28141 |
. . . . . . . . 9
class
Cycles |
9 | 7, 8 | cfv 6431 |
. . . . . . . 8
class
(Cycles‘𝑔) |
10 | 3, 5, 9 | wbr 5079 |
. . . . . . 7
wff 𝑓(Cycles‘𝑔)𝑝 |
11 | | c0 4262 |
. . . . . . . 8
class
∅ |
12 | 3, 11 | wne 2945 |
. . . . . . 7
wff 𝑓 ≠ ∅ |
13 | 10, 12 | wa 396 |
. . . . . 6
wff (𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅) |
14 | 13, 4 | wex 1786 |
. . . . 5
wff
∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅) |
15 | 14, 2 | wex 1786 |
. . . 4
wff
∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅) |
16 | 15 | wn 3 |
. . 3
wff ¬
∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅) |
17 | 16, 6 | cab 2717 |
. 2
class {𝑔 ∣ ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅)} |
18 | 1, 17 | wceq 1542 |
1
wff
AcyclicGraph = {𝑔
∣ ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅)} |