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 uvtxnbgrss
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)
Ref
Expression
Hypothesis
uvtxel.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion
uvtxnbgrss ⊢ ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) → ( 𝑉 ∖ { 𝑁 } ) ⊆ ( 𝐺 NeighbVtx 𝑁 ) )
Proof
Step
Hyp
Ref
Expression
1
uvtxel.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2
1
vtxnbuvtx ⊢ ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) → ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑁 ) )
3
dfss3 ⊢ ( ( 𝑉 ∖ { 𝑁 } ) ⊆ ( 𝐺 NeighbVtx 𝑁 ) ↔ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑁 ) )
4
2 3
sylibr ⊢ ( 𝑁 ∈ ( UnivVtx ‘ 𝐺 ) → ( 𝑉 ∖ { 𝑁 } ) ⊆ ( 𝐺 NeighbVtx 𝑁 ) )