Step | Hyp | Ref
| Expression |
1 | | cuvtx 28642 |
. 2
class
UnivVtx |
2 | | vg |
. . 3
setvar ð |
3 | | cvv 3475 |
. . 3
class
V |
4 | | vn |
. . . . . . 7
setvar ð |
5 | 4 | cv 1541 |
. . . . . 6
class ð |
6 | 2 | cv 1541 |
. . . . . . 7
class ð |
7 | | vv |
. . . . . . . 8
setvar ð£ |
8 | 7 | cv 1541 |
. . . . . . 7
class ð£ |
9 | | cnbgr 28589 |
. . . . . . 7
class
NeighbVtx |
10 | 6, 8, 9 | co 7409 |
. . . . . 6
class (ð NeighbVtx ð£) |
11 | 5, 10 | wcel 2107 |
. . . . 5
wff ð â (ð NeighbVtx ð£) |
12 | | cvtx 28256 |
. . . . . . 7
class
Vtx |
13 | 6, 12 | cfv 6544 |
. . . . . 6
class
(Vtxâð) |
14 | 8 | csn 4629 |
. . . . . 6
class {ð£} |
15 | 13, 14 | cdif 3946 |
. . . . 5
class
((Vtxâð)
â {ð£}) |
16 | 11, 4, 15 | wral 3062 |
. . . 4
wff
âð â
((Vtxâð) â
{ð£})ð â (ð NeighbVtx ð£) |
17 | 16, 7, 13 | crab 3433 |
. . 3
class {ð£ â (Vtxâð) ⣠âð â ((Vtxâð) â {ð£})ð â (ð NeighbVtx ð£)} |
18 | 2, 3, 17 | cmpt 5232 |
. 2
class (ð â V ⊠{ð£ â (Vtxâð) ⣠âð â ((Vtxâð) â {ð£})ð â (ð NeighbVtx ð£)}) |
19 | 1, 18 | wceq 1542 |
1
wff UnivVtx =
(ð â V ⊠{ð£ â (Vtxâð) ⣠âð â ((Vtxâð) â {ð£})ð â (ð NeighbVtx ð£)}) |