MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-uvtx Structured version   Visualization version   GIF version

Definition df-uvtx 25717
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). (Contributed by Alexander van der Vekens, 12-Oct-2017.)
Assertion
Ref Expression
df-uvtx UnivVertex = (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑛𝑣 ∣ ∀𝑘 ∈ (𝑣 ∖ {𝑛}){𝑘, 𝑛} ∈ ran 𝑒})
Distinct variable group:   𝑣,𝑒,𝑘,𝑛

Detailed syntax breakdown of Definition df-uvtx
StepHypRef Expression
1 cuvtx 25714 . 2 class UnivVertex
2 vv . . 3 setvar 𝑣
3 ve . . 3 setvar 𝑒
4 cvv 3172 . . 3 class V
5 vk . . . . . . . 8 setvar 𝑘
65cv 1473 . . . . . . 7 class 𝑘
7 vn . . . . . . . 8 setvar 𝑛
87cv 1473 . . . . . . 7 class 𝑛
96, 8cpr 4126 . . . . . 6 class {𝑘, 𝑛}
103cv 1473 . . . . . . 7 class 𝑒
1110crn 5029 . . . . . 6 class ran 𝑒
129, 11wcel 1976 . . . . 5 wff {𝑘, 𝑛} ∈ ran 𝑒
132cv 1473 . . . . . 6 class 𝑣
148csn 4124 . . . . . 6 class {𝑛}
1513, 14cdif 3536 . . . . 5 class (𝑣 ∖ {𝑛})
1612, 5, 15wral 2895 . . . 4 wff 𝑘 ∈ (𝑣 ∖ {𝑛}){𝑘, 𝑛} ∈ ran 𝑒
1716, 7, 13crab 2899 . . 3 class {𝑛𝑣 ∣ ∀𝑘 ∈ (𝑣 ∖ {𝑛}){𝑘, 𝑛} ∈ ran 𝑒}
182, 3, 4, 4, 17cmpt2 6529 . 2 class (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑛𝑣 ∣ ∀𝑘 ∈ (𝑣 ∖ {𝑛}){𝑘, 𝑛} ∈ ran 𝑒})
191, 18wceq 1474 1 wff UnivVertex = (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑛𝑣 ∣ ∀𝑘 ∈ (𝑣 ∖ {𝑛}){𝑘, 𝑛} ∈ ran 𝑒})
Colors of variables: wff setvar class
This definition is referenced by:  isuvtx  25782  uvtxisvtx  25784  uvtx0  25785  uvtx01vtx  25786
  Copyright terms: Public domain W3C validator