Metamath Proof Explorer


Theorem edgusgrclnbfin

Description: The size of the closed neighborhood of a vertex in a simple graph is finite iff the number of edges having this vertex as endpoint is finite. (Contributed by AV, 10-May-2025)

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

Proof

Step Hyp Ref Expression
1 clnbusgrf1o.v V = Vtx G
2 clnbusgrf1o.e E = Edg G
3 1 dfclnbgr4 U V G ClNeighbVtx U = U G NeighbVtx U
4 3 eleq1d U V G ClNeighbVtx U Fin U G NeighbVtx U Fin
5 4 adantl G USGraph U V G ClNeighbVtx U Fin U G NeighbVtx U Fin
6 1 2 edgusgrnbfin G USGraph U V G NeighbVtx U Fin e E | U e Fin
7 6 anbi2d G USGraph U V U Fin G NeighbVtx U Fin U Fin e E | U e Fin
8 unfib U G NeighbVtx U Fin U Fin G NeighbVtx U Fin
9 snfi U Fin
10 9 biantrur e E | U e Fin U Fin e E | U e Fin
11 7 8 10 3bitr4g G USGraph U V U G NeighbVtx U Fin e E | U e Fin
12 5 11 bitrd G USGraph U V G ClNeighbVtx U Fin e E | U e Fin