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 FinUSGraph N Vtx G G NeighbVtx N Fin

Proof

Step Hyp Ref Expression
1 fusgrusgr G FinUSGraph G USGraph
2 1 adantr G FinUSGraph N Vtx G G USGraph
3 fusgrfis G FinUSGraph Edg G Fin
4 3 adantr G FinUSGraph N Vtx G Edg G Fin
5 simpr G FinUSGraph N Vtx G N Vtx G
6 eqid Vtx G = Vtx G
7 eqid Edg G = Edg G
8 6 7 nbusgrfi G USGraph Edg G Fin N Vtx G G NeighbVtx N Fin
9 2 4 5 8 syl3anc G FinUSGraph N Vtx G G NeighbVtx N Fin