Theorem edgusgrclnbfin

Description: The size of the closed neighborhood of a vertex in a simple graph is finite iff the number of edges having this vertex as endpoint is finite. (Contributed by AV, 10-May-2025)

	Ref	Expression
Hypotheses	clnbusgrf1o.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	clnbusgrf1o.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	edgusgrclnbfin	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( 𝐺 ClNeighbVtx 𝑈 ) ∈ Fin ↔ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin ) )

Proof

Step	Hyp	Ref	Expression
1		clnbusgrf1o.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		clnbusgrf1o.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3	1	dfclnbgr4	⊢ ( 𝑈 ∈ 𝑉 → ( 𝐺 ClNeighbVtx 𝑈 ) = ( { 𝑈 } ∪ ( 𝐺 NeighbVtx 𝑈 ) ) )
4	3	eleq1d	⊢ ( 𝑈 ∈ 𝑉 → ( ( 𝐺 ClNeighbVtx 𝑈 ) ∈ Fin ↔ ( { 𝑈 } ∪ ( 𝐺 NeighbVtx 𝑈 ) ) ∈ Fin ) )
5	4	adantl	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( 𝐺 ClNeighbVtx 𝑈 ) ∈ Fin ↔ ( { 𝑈 } ∪ ( 𝐺 NeighbVtx 𝑈 ) ) ∈ Fin ) )
6	1 2	edgusgrnbfin	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin ↔ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin ) )
7	6	anbi2d	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( { 𝑈 } ∈ Fin ∧ ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin ) ↔ ( { 𝑈 } ∈ Fin ∧ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin ) ) )
8		unfib	⊢ ( ( { 𝑈 } ∪ ( 𝐺 NeighbVtx 𝑈 ) ) ∈ Fin ↔ ( { 𝑈 } ∈ Fin ∧ ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin ) )
9		snfi	⊢ { 𝑈 } ∈ Fin
10	9	biantrur	⊢ ( { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin ↔ ( { 𝑈 } ∈ Fin ∧ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin ) )
11	7 8 10	3bitr4g	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( { 𝑈 } ∪ ( 𝐺 NeighbVtx 𝑈 ) ) ∈ Fin ↔ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin ) )
12	5 11	bitrd	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( 𝐺 ClNeighbVtx 𝑈 ) ∈ Fin ↔ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin ) )