Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-uvtxa | Structured version Visualization version Unicode version |
Description: Define the class of all universal vertices (in graphs). A vertex is called universal if it is adjacent, i.e. connected by an edge, to all other vertices (of the graph) resp. all other vertices are its neighbors. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 24-Oct-2020.) |
Ref | Expression |
---|---|
df-uvtxa | UnivVtx Vtx Vtx NeighbVtx |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cuvtxa 26225 | . 2 UnivVtx | |
2 | vg | . . 3 | |
3 | cvv 3200 | . . 3 | |
4 | vn | . . . . . . 7 | |
5 | 4 | cv 1482 | . . . . . 6 |
6 | 2 | cv 1482 | . . . . . . 7 |
7 | vv | . . . . . . . 8 | |
8 | 7 | cv 1482 | . . . . . . 7 |
9 | cnbgr 26224 | . . . . . . 7 NeighbVtx | |
10 | 6, 8, 9 | co 6650 | . . . . . 6 NeighbVtx |
11 | 5, 10 | wcel 1990 | . . . . 5 NeighbVtx |
12 | cvtx 25874 | . . . . . . 7 Vtx | |
13 | 6, 12 | cfv 5888 | . . . . . 6 Vtx |
14 | 8 | csn 4177 | . . . . . 6 |
15 | 13, 14 | cdif 3571 | . . . . 5 Vtx |
16 | 11, 4, 15 | wral 2912 | . . . 4 Vtx NeighbVtx |
17 | 16, 7, 13 | crab 2916 | . . 3 Vtx Vtx NeighbVtx |
18 | 2, 3, 17 | cmpt 4729 | . 2 Vtx Vtx NeighbVtx |
19 | 1, 18 | wceq 1483 | 1 UnivVtx Vtx Vtx NeighbVtx |
Colors of variables: wff setvar class |
This definition is referenced by: uvtxaval 26287 |
Copyright terms: Public domain | W3C validator |