![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-uvtx | Structured version Visualization version GIF 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), 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 |
---|---|
df-uvtx | ⊢ UnivVtx = (𝑔 ∈ V ↦ {𝑣 ∈ (Vtx‘𝑔) ∣ ∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})𝑛 ∈ (𝑔 NeighbVtx 𝑣)}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cuvtx 27175 | . 2 class UnivVtx | |
2 | vg | . . 3 setvar 𝑔 | |
3 | cvv 3441 | . . 3 class V | |
4 | vn | . . . . . . 7 setvar 𝑛 | |
5 | 4 | cv 1537 | . . . . . 6 class 𝑛 |
6 | 2 | cv 1537 | . . . . . . 7 class 𝑔 |
7 | vv | . . . . . . . 8 setvar 𝑣 | |
8 | 7 | cv 1537 | . . . . . . 7 class 𝑣 |
9 | cnbgr 27122 | . . . . . . 7 class NeighbVtx | |
10 | 6, 8, 9 | co 7135 | . . . . . 6 class (𝑔 NeighbVtx 𝑣) |
11 | 5, 10 | wcel 2111 | . . . . 5 wff 𝑛 ∈ (𝑔 NeighbVtx 𝑣) |
12 | cvtx 26789 | . . . . . . 7 class Vtx | |
13 | 6, 12 | cfv 6324 | . . . . . 6 class (Vtx‘𝑔) |
14 | 8 | csn 4525 | . . . . . 6 class {𝑣} |
15 | 13, 14 | cdif 3878 | . . . . 5 class ((Vtx‘𝑔) ∖ {𝑣}) |
16 | 11, 4, 15 | wral 3106 | . . . 4 wff ∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})𝑛 ∈ (𝑔 NeighbVtx 𝑣) |
17 | 16, 7, 13 | crab 3110 | . . 3 class {𝑣 ∈ (Vtx‘𝑔) ∣ ∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})𝑛 ∈ (𝑔 NeighbVtx 𝑣)} |
18 | 2, 3, 17 | cmpt 5110 | . 2 class (𝑔 ∈ V ↦ {𝑣 ∈ (Vtx‘𝑔) ∣ ∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})𝑛 ∈ (𝑔 NeighbVtx 𝑣)}) |
19 | 1, 18 | wceq 1538 | 1 wff UnivVtx = (𝑔 ∈ V ↦ {𝑣 ∈ (Vtx‘𝑔) ∣ ∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})𝑛 ∈ (𝑔 NeighbVtx 𝑣)}) |
Colors of variables: wff setvar class |
This definition is referenced by: uvtxval 27177 |
Copyright terms: Public domain | W3C validator |