Metamath Proof Explorer


Theorem clnbusgrfi

Description: The closed neighborhood of a vertex in a simple graph with a finite number of edges is a finite set. (Contributed by AV, 10-May-2025)

Ref Expression
Hypotheses clnbusgrf1o.v V = Vtx G
clnbusgrf1o.e E = Edg G
Assertion clnbusgrfi G USGraph E Fin U V G ClNeighbVtx U Fin

Proof

Step Hyp Ref Expression
1 clnbusgrf1o.v V = Vtx G
2 clnbusgrf1o.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 edgusgrclnbfin G USGraph U V G ClNeighbVtx U Fin e E | U e Fin
6 5 3adant2 G USGraph E Fin U V G ClNeighbVtx U Fin e E | U e Fin
7 4 6 mpbird G USGraph E Fin U V G ClNeighbVtx U Fin