Metamath Proof Explorer

Definition df-clnbgr

Description: Define the closedneighborhood resp. the class of all neighbors of a vertex (in a graph) and the vertex itself, see definition in section I.1 of Bollobas p. 3. The closed neighborhood of a vertex are all vertices which are connected with this vertex by an edge and the vertex itself (in contrast to an open neighborhood, see df-nbgr ). Alternatively, a closed neighborhood of a vertex could have been defined as its open neighborhood enhanced by the vertex itself, see dfclnbgr4 . This definition is applicable even for arbitrary hypergraphs. (Contributed by AV, 7-May-2025)

Ref Expression
Assertion df-clnbgr Could not format assertion : No typesetting found for |- ClNeighbVtx = ( g e. _V , v e. ( Vtx ` g ) |-> ( { v } u. { n e. ( Vtx ` g ) | E. e e. ( Edg ` g ) { v , n } C_ e } ) ) with typecode |-

Detailed syntax breakdown

Step Hyp Ref Expression
0 cclnbgr Could not format ClNeighbVtx : No typesetting found for class ClNeighbVtx with typecode class
1 vg setvar g
2 cvv class V
3 vv setvar v
4 cvtx class Vtx
5 1 cv setvar g
6 5 4 cfv class Vtx ⁡ g
7 3 cv setvar v
8 7 csn class v
9 vn setvar n
10 ve setvar e
11 cedg class Edg
12 5 11 cfv class Edg ⁡ g
13 9 cv setvar n
14 7 13 cpr class v n
15 10 cv setvar e
16 14 15 wss wff v n ⊆ e
17 16 10 12 wrex wff ∃ e ∈ Edg ⁡ g v n ⊆ e
18 17 9 6 crab class n ∈ Vtx ⁡ g | ∃ e ∈ Edg ⁡ g v n ⊆ e
19 8 18 cun class v ∪ n ∈ Vtx ⁡ g | ∃ e ∈ Edg ⁡ g v n ⊆ e
20 1 3 2 6 19 cmpo class g ∈ V , v ∈ Vtx ⁡ g ⟼ v ∪ n ∈ Vtx ⁡ g | ∃ e ∈ Edg ⁡ g v n ⊆ e
21 0 20 wceq Could not format ClNeighbVtx = ( g e. _V , v e. ( Vtx ` g ) |-> ( { v } u. { n e. ( Vtx ` g ) | E. e e. ( Edg ` g ) { v , n } C_ e } ) ) : No typesetting found for wff ClNeighbVtx = ( g e. _V , v e. ( Vtx ` g ) |-> ( { v } u. { n e. ( Vtx ` g ) | E. e e. ( Edg ` g ) { v , n } C_ e } ) ) with typecode wff