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

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 ⊢ 𝑉 = ( 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 ) )