This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ClNeighbVtx 𝑁 ) ∈ Fin )

Proof

Step Hyp Ref Expression
1 fusgrusgr ⊢ ( 𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph )
2 1 adantr ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) → 𝐺 ∈ USGraph )
3 fusgrfis ⊢ ( 𝐺 ∈ FinUSGraph → ( Edg ‘ 𝐺 ) ∈ Fin )
4 3 adantr ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) → ( Edg ‘ 𝐺 ) ∈ Fin )
5 simpr ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) → 𝑁 ∈ ( Vtx ‘ 𝐺 ) )
6 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
7 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
8 6 7 clnbusgrfi ⊢ ( ( 𝐺 ∈ USGraph ∧ ( Edg ‘ 𝐺 ) ∈ Fin ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ClNeighbVtx 𝑁 ) ∈ Fin )
9 2 4 5 8 syl3anc ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ClNeighbVtx 𝑁 ) ∈ Fin )