Metamath Proof Explorer

Theorem clnbfiusgrfi

Description: The closed neighborhood of a vertex in a finite simple graph is a finite set. (Contributed by AV, 10-May-2025)

Ref Expression
Assertion clnbfiusgrfi 
|- ( ( G e. FinUSGraph /\ N e. ( Vtx ` G ) ) -> ( G ClNeighbVtx 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 clnbusgrfi 
 |-  ( ( G e. USGraph /\ ( Edg ` G ) e. Fin /\ N e. ( Vtx ` G ) ) -> ( G ClNeighbVtx N ) e. Fin )
9 2 4 5 8 syl3anc 
 |-  ( ( G e. FinUSGraph /\ N e. ( Vtx ` G ) ) -> ( G ClNeighbVtx N ) e. Fin )