This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database GRAPH THEORY Undirected graphs Neighbors, complete graphs and universal vertices Universal vertices uvtxisvtx
Description: A universal vertex is a vertex. (Contributed by Alexander van der
Vekens , 12-Oct-2017) (Revised by AV , 30-Oct-2020) (Proof shortened by AV , 14-Feb-2022)
Ref
Expression
Hypothesis
uvtxel.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion
uvtxisvtx ⊢ ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) → 𝑁 ∈ 𝑉 )
Proof
Step
Hyp
Ref
Expression
1
uvtxel.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2
1
uvtxel ⊢ ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ( 𝑁 ∈ 𝑉 ∧ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑁 ) ) )
3
2
simplbi ⊢ ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) → 𝑁 ∈ 𝑉 )