![]() |
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 26690 | . 2 class UnivVtx | |
2 | vg | . . 3 setvar 𝑔 | |
3 | cvv 3414 | . . 3 class V | |
4 | vn | . . . . . . 7 setvar 𝑛 | |
5 | 4 | cv 1655 | . . . . . 6 class 𝑛 |
6 | 2 | cv 1655 | . . . . . . 7 class 𝑔 |
7 | vv | . . . . . . . 8 setvar 𝑣 | |
8 | 7 | cv 1655 | . . . . . . 7 class 𝑣 |
9 | cnbgr 26636 | . . . . . . 7 class NeighbVtx | |
10 | 6, 8, 9 | co 6910 | . . . . . 6 class (𝑔 NeighbVtx 𝑣) |
11 | 5, 10 | wcel 2164 | . . . . 5 wff 𝑛 ∈ (𝑔 NeighbVtx 𝑣) |
12 | cvtx 26301 | . . . . . . 7 class Vtx | |
13 | 6, 12 | cfv 6127 | . . . . . 6 class (Vtx‘𝑔) |
14 | 8 | csn 4399 | . . . . . 6 class {𝑣} |
15 | 13, 14 | cdif 3795 | . . . . 5 class ((Vtx‘𝑔) ∖ {𝑣}) |
16 | 11, 4, 15 | wral 3117 | . . . 4 wff ∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})𝑛 ∈ (𝑔 NeighbVtx 𝑣) |
17 | 16, 7, 13 | crab 3121 | . . 3 class {𝑣 ∈ (Vtx‘𝑔) ∣ ∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})𝑛 ∈ (𝑔 NeighbVtx 𝑣)} |
18 | 2, 3, 17 | cmpt 4954 | . 2 class (𝑔 ∈ V ↦ {𝑣 ∈ (Vtx‘𝑔) ∣ ∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})𝑛 ∈ (𝑔 NeighbVtx 𝑣)}) |
19 | 1, 18 | wceq 1656 | 1 wff UnivVtx = (𝑔 ∈ V ↦ {𝑣 ∈ (Vtx‘𝑔) ∣ ∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})𝑛 ∈ (𝑔 NeighbVtx 𝑣)}) |
Colors of variables: wff setvar class |
This definition is referenced by: uvtxval 26692 |
Copyright terms: Public domain | W3C validator |