Metamath Proof Explorer

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 ⊢ V = Vtx ⁡ G
clnbusgrf1o.e ⊢ E = Edg ⁡ G
Assertion edgusgrclnbfin ⊢ G ∈ USGraph ∧ U ∈ V → G ClNeighbVtx U ∈ Fin ↔ e ∈ E | U ∈ e ∈ Fin

Proof

Step Hyp Ref Expression
1 clnbusgrf1o.v ⊢ V = Vtx ⁡ G
2 clnbusgrf1o.e ⊢ E = Edg ⁡ G
3 1 dfclnbgr4 ⊢ U ∈ V → G ClNeighbVtx U = U ∪ G NeighbVtx U
4 3 eleq1d ⊢ U ∈ V → G ClNeighbVtx U ∈ Fin ↔ U ∪ G NeighbVtx U ∈ Fin
5 4 adantl ⊢ G ∈ USGraph ∧ U ∈ V → G ClNeighbVtx U ∈ Fin ↔ U ∪ G NeighbVtx U ∈ Fin
6 1 2 edgusgrnbfin ⊢ G ∈ USGraph ∧ U ∈ V → G NeighbVtx U ∈ Fin ↔ e ∈ E | U ∈ e ∈ Fin
7 6 anbi2d ⊢ G ∈ USGraph ∧ U ∈ V → U ∈ Fin ∧ G NeighbVtx U ∈ Fin ↔ U ∈ Fin ∧ e ∈ E | U ∈ e ∈ Fin
8 unfib ⊢ U ∪ G NeighbVtx U ∈ Fin ↔ U ∈ Fin ∧ G NeighbVtx U ∈ Fin
9 snfi ⊢ U ∈ Fin
10 9 biantrur ⊢ e ∈ E | U ∈ e ∈ Fin ↔ U ∈ Fin ∧ e ∈ E | U ∈ e ∈ Fin
11 7 8 10 3bitr4g ⊢ G ∈ USGraph ∧ U ∈ V → U ∪ G NeighbVtx U ∈ Fin ↔ e ∈ E | U ∈ e ∈ Fin
12 5 11 bitrd ⊢ G ∈ USGraph ∧ U ∈ V → G ClNeighbVtx U ∈ Fin ↔ e ∈ E | U ∈ e ∈ Fin