Step | Hyp | Ref
| Expression |
1 | | cuvtx 28639 |
. 2
class
UnivVtx |
2 | | vg |
. . 3
setvar ð |
3 | | cvv 3474 |
. . 3
class
V |
4 | | vn |
. . . . . . 7
setvar ð |
5 | 4 | cv 1540 |
. . . . . 6
class ð |
6 | 2 | cv 1540 |
. . . . . . 7
class ð |
7 | | vv |
. . . . . . . 8
setvar ð£ |
8 | 7 | cv 1540 |
. . . . . . 7
class ð£ |
9 | | cnbgr 28586 |
. . . . . . 7
class
NeighbVtx |
10 | 6, 8, 9 | co 7408 |
. . . . . 6
class (ð NeighbVtx ð£) |
11 | 5, 10 | wcel 2106 |
. . . . 5
wff ð â (ð NeighbVtx ð£) |
12 | | cvtx 28253 |
. . . . . . 7
class
Vtx |
13 | 6, 12 | cfv 6543 |
. . . . . 6
class
(Vtxâð) |
14 | 8 | csn 4628 |
. . . . . 6
class {ð£} |
15 | 13, 14 | cdif 3945 |
. . . . 5
class
((Vtxâð)
â {ð£}) |
16 | 11, 4, 15 | wral 3061 |
. . . 4
wff
âð â
((Vtxâð) â
{ð£})ð â (ð NeighbVtx ð£) |
17 | 16, 7, 13 | crab 3432 |
. . 3
class {ð£ â (Vtxâð) ⣠âð â ((Vtxâð) â {ð£})ð â (ð NeighbVtx ð£)} |
18 | 2, 3, 17 | cmpt 5231 |
. 2
class (ð â V ⊠{ð£ â (Vtxâð) ⣠âð â ((Vtxâð) â {ð£})ð â (ð NeighbVtx ð£)}) |
19 | 1, 18 | wceq 1541 |
1
wff UnivVtx =
(ð â V ⊠{ð£ â (Vtxâð) ⣠âð â ((Vtxâð) â {ð£})ð â (ð NeighbVtx ð£)}) |