Metamath Proof Explorer

Theorem nbusgrfi

Description: The class of neighbors of a vertex in a simple graph with a finite number of edges is a finite set. (Contributed by Alexander van der Vekens, 19-Dec-2017) (Revised by AV, 28-Oct-2020)

Ref Expression
Hypotheses nbusgrf1o.v ⊢V=Vtx⁡G
nbusgrf1o.e ⊢E=Edg⁡G
Assertion nbusgrfi ⊢G∈USGraph∧E∈Fin∧U∈V→GNeighbVtxU∈Fin

Proof

Step Hyp Ref Expression
1 nbusgrf1o.v ⊢V=Vtx⁡G
2 nbusgrf1o.e ⊢E=Edg⁡G
3 rabfi ⊢E∈Fin→e∈E|U∈e∈Fin
4 3 3ad2ant2 ⊢G∈USGraph∧E∈Fin∧U∈V→e∈E|U∈e∈Fin
5 1 2 edgusgrnbfin ⊢G∈USGraph∧U∈V→GNeighbVtxU∈Fin↔e∈E|U∈e∈Fin
6 5 3adant2 ⊢G∈USGraph∧E∈Fin∧U∈V→GNeighbVtxU∈Fin↔e∈E|U∈e∈Fin
7 4 6 mpbird ⊢G∈USGraph∧E∈Fin∧U∈V→GNeighbVtxU∈Fin