Metamath Proof Explorer


Theorem nbfiusgrfi

Description: The class of neighbors of a vertex in a finite simple graph is a finite set. (Contributed by Alexander van der Vekens, 7-Mar-2018) (Revised by AV, 28-Oct-2020)

Ref Expression
Assertion nbfiusgrfi
|- ( ( G e. FinUSGraph /\ N e. ( Vtx ` G ) ) -> ( G NeighbVtx N ) e. Fin )

Proof

Step Hyp Ref Expression
1 fusgrusgr
 |-  ( G e. FinUSGraph -> G e. USGraph )
2 1 adantr
 |-  ( ( G e. FinUSGraph /\ N e. ( Vtx ` G ) ) -> G e. USGraph )
3 fusgrfis
 |-  ( G e. FinUSGraph -> ( Edg ` G ) e. Fin )
4 3 adantr
 |-  ( ( G e. FinUSGraph /\ N e. ( Vtx ` G ) ) -> ( Edg ` G ) e. Fin )
5 simpr
 |-  ( ( G e. FinUSGraph /\ N e. ( Vtx ` G ) ) -> N e. ( Vtx ` G ) )
6 eqid
 |-  ( Vtx ` G ) = ( Vtx ` G )
7 eqid
 |-  ( Edg ` G ) = ( Edg ` G )
8 6 7 nbusgrfi
 |-  ( ( G e. USGraph /\ ( Edg ` G ) e. Fin /\ N e. ( Vtx ` G ) ) -> ( G NeighbVtx N ) e. Fin )
9 2 4 5 8 syl3anc
 |-  ( ( G e. FinUSGraph /\ N e. ( Vtx ` G ) ) -> ( G NeighbVtx N ) e. Fin )