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 ∈ FinUSGraph ∧ N ∈ Vtx ⁡ G → G ClNeighbVtx 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 clnbusgrfi ⊢ G ∈ USGraph ∧ Edg ⁡ G ∈ Fin ∧ N ∈ Vtx ⁡ G → G ClNeighbVtx N ∈ Fin
9 2 4 5 8 syl3anc ⊢ G ∈ FinUSGraph ∧ N ∈ Vtx ⁡ G → G ClNeighbVtx N ∈ Fin