This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. USGraph /\ U e. V ) -> ( ( G ClNeighbVtx U ) e. Fin <-> { e e. E | U e. e } e. Fin ) )

Proof

Step Hyp Ref Expression
1 clnbusgrf1o.v 
 |-  V = ( Vtx ` G )
2 clnbusgrf1o.e 
 |-  E = ( Edg ` G )
3 1 dfclnbgr4 
 |-  ( U e. V -> ( G ClNeighbVtx U ) = ( { U } u. ( G NeighbVtx U ) ) )
4 3 eleq1d 
 |-  ( U e. V -> ( ( G ClNeighbVtx U ) e. Fin <-> ( { U } u. ( G NeighbVtx U ) ) e. Fin ) )
5 4 adantl 
 |-  ( ( G e. USGraph /\ U e. V ) -> ( ( G ClNeighbVtx U ) e. Fin <-> ( { U } u. ( G NeighbVtx U ) ) e. Fin ) )
6 1 2 edgusgrnbfin 
 |-  ( ( G e. USGraph /\ U e. V ) -> ( ( G NeighbVtx U ) e. Fin <-> { e e. E | U e. e } e. Fin ) )
7 6 anbi2d 
 |-  ( ( G e. USGraph /\ U e. V ) -> ( ( { U } e. Fin /\ ( G NeighbVtx U ) e. Fin ) <-> ( { U } e. Fin /\ { e e. E | U e. e } e. Fin ) ) )
8 unfib 
 |-  ( ( { U } u. ( G NeighbVtx U ) ) e. Fin <-> ( { U } e. Fin /\ ( G NeighbVtx U ) e. Fin ) )
9 snfi 
 |-  { U } e. Fin
10 9 biantrur 
 |-  ( { e e. E | U e. e } e. Fin <-> ( { U } e. Fin /\ { e e. E | U e. e } e. Fin ) )
11 7 8 10 3bitr4g 
 |-  ( ( G e. USGraph /\ U e. V ) -> ( ( { U } u. ( G NeighbVtx U ) ) e. Fin <-> { e e. E | U e. e } e. Fin ) )
12 5 11 bitrd 
 |-  ( ( G e. USGraph /\ U e. V ) -> ( ( G ClNeighbVtx U ) e. Fin <-> { e e. E | U e. e } e. Fin ) )