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

Proof

Step	Hyp	Ref	Expression
1		clnbusgrf1o.v	|- V = ( Vtx ` G )
2		clnbusgrf1o.e	|- E = ( Edg ` G )
3		rabfi	|- ( E e. Fin -> { e e. E | U e. e } e. Fin )
4	3	3ad2ant2	|- ( ( G e. USGraph /\ E e. Fin /\ U e. V ) -> { e e. E | U e. e } e. Fin )
5	1 2	edgusgrclnbfin	|- ( ( G e. USGraph /\ U e. V ) -> ( ( G ClNeighbVtx U ) e. Fin <-> { e e. E | U e. e } e. Fin ) )
6	5	3adant2	|- ( ( G e. USGraph /\ E e. Fin /\ U e. V ) -> ( ( G ClNeighbVtx U ) e. Fin <-> { e e. E | U e. e } e. Fin ) )
7	4 6	mpbird	|- ( ( G e. USGraph /\ E e. Fin /\ U e. V ) -> ( G ClNeighbVtx U ) e. Fin )