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