Step | Hyp | Ref
| Expression |
1 | | crgr 28812 |
. 2
class
RegGraph |
2 | | vk |
. . . . . 6
setvar π |
3 | 2 | cv 1541 |
. . . . 5
class π |
4 | | cxnn0 12544 |
. . . . 5
class
β0* |
5 | 3, 4 | wcel 2107 |
. . . 4
wff π β
β0* |
6 | | vv |
. . . . . . . 8
setvar π£ |
7 | 6 | cv 1541 |
. . . . . . 7
class π£ |
8 | | vg |
. . . . . . . . 9
setvar π |
9 | 8 | cv 1541 |
. . . . . . . 8
class π |
10 | | cvtxdg 28722 |
. . . . . . . 8
class
VtxDeg |
11 | 9, 10 | cfv 6544 |
. . . . . . 7
class
(VtxDegβπ) |
12 | 7, 11 | cfv 6544 |
. . . . . 6
class
((VtxDegβπ)βπ£) |
13 | 12, 3 | wceq 1542 |
. . . . 5
wff
((VtxDegβπ)βπ£) = π |
14 | | cvtx 28256 |
. . . . . 6
class
Vtx |
15 | 9, 14 | cfv 6544 |
. . . . 5
class
(Vtxβπ) |
16 | 13, 6, 15 | wral 3062 |
. . . 4
wff
βπ£ β
(Vtxβπ)((VtxDegβπ)βπ£) = π |
17 | 5, 16 | wa 397 |
. . 3
wff (π β
β0* β§ βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = π) |
18 | 17, 8, 2 | copab 5211 |
. 2
class
{β¨π, πβ© β£ (π β
β0* β§ βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = π)} |
19 | 1, 18 | wceq 1542 |
1
wff RegGraph =
{β¨π, πβ© β£ (π β
β0* β§ βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = π)} |