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 uvtxnbgr
Description: A universal vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens , 14-Oct-2017) (Revised by AV , 3-Nov-2020)
(Revised by AV , 23-Mar-2021)
Ref
Expression
Hypothesis
uvtxnbgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion
uvtxnbgr ⊢ ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) → ( 𝐺 NeighbVtx 𝑁 ) = ( 𝑉 ∖ { 𝑁 } ) )
Proof
Step
Hyp
Ref
Expression
1
uvtxnbgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2
1
nbgrssovtx ⊢ ( 𝐺 NeighbVtx 𝑁 ) ⊆ ( 𝑉 ∖ { 𝑁 } )
3
2
a1i ⊢ ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) → ( 𝐺 NeighbVtx 𝑁 ) ⊆ ( 𝑉 ∖ { 𝑁 } ) )
4
1
uvtxnbgrss ⊢ ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) → ( 𝑉 ∖ { 𝑁 } ) ⊆ ( 𝐺 NeighbVtx 𝑁 ) )
5
3 4
eqssd ⊢ ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) → ( 𝐺 NeighbVtx 𝑁 ) = ( 𝑉 ∖ { 𝑁 } ) )