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 ) )