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 nbedgusgr
Description: The number of neighbors of a vertex is the number of edges at the vertex
in a simple graph. (Contributed by AV , 27-Dec-2020) (Proof shortened by AV , 5-May-2021)
Ref
Expression
Hypotheses
nbusgrf1o.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
nbusgrf1o.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion
nbedgusgr ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ) )
Proof
Step
Hyp
Ref
Expression
1
nbusgrf1o.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2
nbusgrf1o.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3
ovex ⊢ ( 𝐺 NeighbVtx 𝑈 ) ∈ V
4
1 2
nbusgrf1o ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ∃ 𝑓 𝑓 : ( 𝐺 NeighbVtx 𝑈 ) –1-1 -onto → { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } )
5
hasheqf1oi ⊢ ( ( 𝐺 NeighbVtx 𝑈 ) ∈ V → ( ∃ 𝑓 𝑓 : ( 𝐺 NeighbVtx 𝑈 ) –1-1 -onto → { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ) ) )
6
3 4 5
mpsyl ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ) )