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

Metamath Proof Explorer

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 )