Metamath Proof Explorer

Theorem 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 ⊢ V = Vtx ⁡ G
nbusgrf1o.e ⊢ E = Edg ⁡ G
Assertion nbedgusgr ⊢ G ∈ USGraph ∧ U ∈ V → G NeighbVtx U = e ∈ E | U ∈ e

Proof

Step Hyp Ref Expression
1 nbusgrf1o.v ⊢ V = Vtx ⁡ G
2 nbusgrf1o.e ⊢ E = Edg ⁡ G
3 ovex ⊢ G NeighbVtx U ∈ V
4 1 2 nbusgrf1o ⊢ G ∈ USGraph ∧ U ∈ V → ∃ f f : G NeighbVtx U ⟶ 1-1 onto e ∈ E | U ∈ e
5 hasheqf1oi ⊢ G NeighbVtx U ∈ V → ∃ f f : G NeighbVtx U ⟶ 1-1 onto e ∈ E | U ∈ e → G NeighbVtx U = e ∈ E | U ∈ e
6 3 4 5 mpsyl ⊢ G ∈ USGraph ∧ U ∈ V → G NeighbVtx U = e ∈ E | U ∈ e