This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-uvtx

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 ) } )