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=\mathrm{Vtx}\left(G\right)$$
	clnbusgrf1o.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
Assertion	edgusgrclnbfin	Could not format assertion : No typesetting found for |- ( ( G e. USGraph /\ U e. V ) -> ( ( G ClNeighbVtx U ) e. Fin <-> { e e. E | U e. e } e. Fin ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		clnbusgrf1o.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		clnbusgrf1o.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
3	1	dfclnbgr4	Could not format ( U e. V -> ( G ClNeighbVtx U ) = ( { U } u. ( G NeighbVtx U ) ) ) : No typesetting found for |- ( U e. V -> ( G ClNeighbVtx U ) = ( { U } u. ( G NeighbVtx U ) ) ) with typecode |-
4	3	eleq1d	Could not format ( U e. V -> ( ( G ClNeighbVtx U ) e. Fin <-> ( { U } u. ( G NeighbVtx U ) ) e. Fin ) ) : No typesetting found for |- ( U e. V -> ( ( G ClNeighbVtx U ) e. Fin <-> ( { U } u. ( G NeighbVtx U ) ) e. Fin ) ) with typecode |-
5	4	adantl	Could not format ( ( G e. USGraph /\ U e. V ) -> ( ( G ClNeighbVtx U ) e. Fin <-> ( { U } u. ( G NeighbVtx U ) ) e. Fin ) ) : No typesetting found for |- ( ( G e. USGraph /\ U e. V ) -> ( ( G ClNeighbVtx U ) e. Fin <-> ( { U } u. ( G NeighbVtx U ) ) e. Fin ) ) with typecode |-
6	1 2	edgusgrnbfin	$$⊢\left(G\in \mathrm{USGraph}\wedge U\in V\right)\to \left(G\mathrm{NeighbVtx}U\in \mathrm{Fin}\leftrightarrow \left\{e\in E|U\in e\right\}\in \mathrm{Fin}\right)$$
7	6	anbi2d	$$⊢\left(G\in \mathrm{USGraph}\wedge U\in V\right)\to \left(\left(\left\{U\right\}\in \mathrm{Fin}\wedge G\mathrm{NeighbVtx}U\in \mathrm{Fin}\right)\leftrightarrow \left(\left\{U\right\}\in \mathrm{Fin}\wedge \left\{e\in E|U\in e\right\}\in \mathrm{Fin}\right)\right)$$
8		unfib	$$⊢\left\{U\right\}\cup \left(G\mathrm{NeighbVtx}U\right)\in \mathrm{Fin}\leftrightarrow \left(\left\{U\right\}\in \mathrm{Fin}\wedge G\mathrm{NeighbVtx}U\in \mathrm{Fin}\right)$$
9		snfi	$$⊢\left\{U\right\}\in \mathrm{Fin}$$
10	9	biantrur	$$⊢\left\{e\in E|U\in e\right\}\in \mathrm{Fin}\leftrightarrow \left(\left\{U\right\}\in \mathrm{Fin}\wedge \left\{e\in E|U\in e\right\}\in \mathrm{Fin}\right)$$
11	7 8 10	3bitr4g	$$⊢\left(G\in \mathrm{USGraph}\wedge U\in V\right)\to \left(\left\{U\right\}\cup \left(G\mathrm{NeighbVtx}U\right)\in \mathrm{Fin}\leftrightarrow \left\{e\in E|U\in e\right\}\in \mathrm{Fin}\right)$$
12	5 11	bitrd	Could not format ( ( G e. USGraph /\ U e. V ) -> ( ( G ClNeighbVtx U ) e. Fin <-> { e e. E | U e. e } e. Fin ) ) : No typesetting found for |- ( ( G e. USGraph /\ U e. V ) -> ( ( G ClNeighbVtx U ) e. Fin <-> { e e. E | U e. e } e. Fin ) ) with typecode |-