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 Neighbors nbusgrvtx
Description: The set of neighbors of a vertex in a simple graph. (Contributed by Alexander van der Vekens , 9-Oct-2017) (Revised by AV , 26-Oct-2020)
(Proof shortened by AV , 27-Nov-2020)
Ref
Expression
Hypotheses
nbuhgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
nbuhgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion
nbusgrvtx ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } )
Proof
Step
Hyp
Ref
Expression
1
nbuhgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2
nbuhgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3
usgrumgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UMGraph )
4
1 2
nbumgrvtx ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } )
5
3 4
sylan ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } )