Database
GRAPH THEORY
Undirected graphs
Neighbors, complete graphs and universal vertices
Universal vertices
df-uvtx
Metamath Proof Explorer
Description: Define the class of all universal vertices (in graphs). A vertex is
calleduniversal if it is adjacent, i.e. connected by an edge, to all
other vertices (of the graph), or equivalently, if all other vertices
are its neighbors. (Contributed by Alexander van der Vekens , 12-Oct-2017) (Revised by AV , 24-Oct-2020)
Ref
Expression
Assertion
df-uvtx
|- UnivVtx = ( g e. _V |-> { v e. ( Vtx ` g ) | A. n e. ( ( Vtx ` g ) \ { v } ) n e. ( g NeighbVtx v ) } )
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cuvtx
|- UnivVtx
1
vg
|- g
2
cvv
|- _V
3
vv
|- v
4
cvtx
|- Vtx
5
1
cv
|- g
6
5 4
cfv
|- ( Vtx ` g )
7
vn
|- n
8
3
cv
|- v
9
8
csn
|- { v }
10
6 9
cdif
|- ( ( Vtx ` g ) \ { v } )
11
7
cv
|- n
12
cnbgr
|- NeighbVtx
13
5 8 12
co
|- ( g NeighbVtx v )
14
11 13
wcel
|- n e. ( g NeighbVtx v )
15
14 7 10
wral
|- A. n e. ( ( Vtx ` g ) \ { v } ) n e. ( g NeighbVtx v )
16
15 3 6
crab
|- { v e. ( Vtx ` g ) | A. n e. ( ( Vtx ` g ) \ { v } ) n e. ( g NeighbVtx v ) }
17
1 2 16
cmpt
|- ( g e. _V |-> { v e. ( Vtx ` g ) | A. n e. ( ( Vtx ` g ) \ { v } ) n e. ( g NeighbVtx v ) } )
18
0 17
wceq
|- UnivVtx = ( g e. _V |-> { v e. ( Vtx ` g ) | A. n e. ( ( Vtx ` g ) \ { v } ) n e. ( g NeighbVtx v ) } )