Theorem nbusgrfi

Description: The class of neighbors of a vertex in a simple graph with a finite number of edges is a finite set. (Contributed by Alexander van der Vekens, 19-Dec-2017) (Revised by AV, 28-Oct-2020)

	Ref	Expression
Hypotheses	nbusgrf1o.v	|- V = ( Vtx ` G )
	nbusgrf1o.e	|- E = ( Edg ` G )
Assertion	nbusgrfi	|- ( ( G e. USGraph /\ E e. Fin /\ U e. V ) -> ( G NeighbVtx U ) e. Fin )

Proof

Step	Hyp	Ref	Expression
1		nbusgrf1o.v	|- V = ( Vtx ` G )
2		nbusgrf1o.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	edgusgrnbfin	|- ( ( G e. USGraph /\ U e. V ) -> ( ( G NeighbVtx U ) e. Fin <-> { e e. E | U e. e } e. Fin ) )
6	5	3adant2	|- ( ( G e. USGraph /\ E e. Fin /\ U e. V ) -> ( ( G NeighbVtx 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 NeighbVtx U ) e. Fin )