Database
GRAPH THEORY
Undirected graphs
Neighbors, complete graphs and universal vertices
Universal vertices
vtxnbuvtx
Metamath Proof Explorer
Description: A universal vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens , 14-Oct-2017) (Revised by AV , 30-Oct-2020)
(Proof shortened by AV , 14-Feb-2022)
Ref
Expression
Hypothesis
uvtxel.v
⊢ V = Vtx ⁡ G
Assertion
vtxnbuvtx
⊢ N ∈ UnivVtx ⁡ G → ∀ n ∈ V ∖ N n ∈ G NeighbVtx N
Proof
Step
Hyp
Ref
Expression
1
uvtxel.v
⊢ V = Vtx ⁡ G
2
1
uvtxel
⊢ N ∈ UnivVtx ⁡ G ↔ N ∈ V ∧ ∀ n ∈ V ∖ N n ∈ G NeighbVtx N
3
2
simprbi
⊢ N ∈ UnivVtx ⁡ G → ∀ n ∈ V ∖ N n ∈ G NeighbVtx N