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 )