Step | Hyp | Ref
| Expression |
1 | | cacycgr 33403 |
. 2
class
AcyclicGraph |
2 | | vf |
. . . . . . . . 9
setvar π |
3 | 2 | cv 1539 |
. . . . . . . 8
class π |
4 | | vp |
. . . . . . . . 9
setvar π |
5 | 4 | cv 1539 |
. . . . . . . 8
class π |
6 | | vg |
. . . . . . . . . 10
setvar π |
7 | 6 | cv 1539 |
. . . . . . . . 9
class π |
8 | | ccycls 28441 |
. . . . . . . . 9
class
Cycles |
9 | 7, 8 | cfv 6479 |
. . . . . . . 8
class
(Cyclesβπ) |
10 | 3, 5, 9 | wbr 5092 |
. . . . . . 7
wff π(Cyclesβπ)π |
11 | | c0 4269 |
. . . . . . . 8
class
β
|
12 | 3, 11 | wne 2940 |
. . . . . . 7
wff π β β
|
13 | 10, 12 | wa 396 |
. . . . . 6
wff (π(Cyclesβπ)π β§ π β β
) |
14 | 13, 4 | wex 1780 |
. . . . 5
wff
βπ(π(Cyclesβπ)π β§ π β β
) |
15 | 14, 2 | wex 1780 |
. . . 4
wff
βπβπ(π(Cyclesβπ)π β§ π β β
) |
16 | 15 | wn 3 |
. . 3
wff Β¬
βπβπ(π(Cyclesβπ)π β§ π β β
) |
17 | 16, 6 | cab 2713 |
. 2
class {π β£ Β¬ βπβπ(π(Cyclesβπ)π β§ π β β
)} |
18 | 1, 17 | wceq 1540 |
1
wff
AcyclicGraph = {π
β£ Β¬ βπβπ(π(Cyclesβπ)π β§ π β β
)} |