Theorem clnbusgrfi

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

	Ref	Expression
Hypotheses	clnbusgrf1o.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	clnbusgrf1o.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	clnbusgrfi	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐸 ∈ Fin ∧ 𝑈 ∈ 𝑉 ) → ( 𝐺 ClNeighbVtx 𝑈 ) ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		clnbusgrf1o.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		clnbusgrf1o.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		rabfi	⊢ ( 𝐸 ∈ Fin → { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin )
4	3	3ad2ant2	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐸 ∈ Fin ∧ 𝑈 ∈ 𝑉 ) → { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin )
5	1 2	edgusgrclnbfin	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( 𝐺 ClNeighbVtx 𝑈 ) ∈ Fin ↔ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin ) )
6	5	3adant2	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐸 ∈ Fin ∧ 𝑈 ∈ 𝑉 ) → ( ( 𝐺 ClNeighbVtx 𝑈 ) ∈ Fin ↔ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin ) )
7	4 6	mpbird	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐸 ∈ Fin ∧ 𝑈 ∈ 𝑉 ) → ( 𝐺 ClNeighbVtx 𝑈 ) ∈ Fin )