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 → G NeighbVtx U ∈ 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 → G NeighbVtx U ∈ Fin ↔ e ∈ E | U ∈ e ∈ Fin
6 5 3adant2 ⊢ G ∈ USGraph ∧ E ∈ Fin ∧ U ∈ V → G NeighbVtx U ∈ Fin ↔ e ∈ E | U ∈ e ∈ Fin
7 4 6 mpbird ⊢ G ∈ USGraph ∧ E ∈ Fin ∧ U ∈ V → G NeighbVtx U ∈ Fin