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	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	clnbusgrf1o.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
Assertion	clnbusgrfi	Could not format assertion : No typesetting found for |- ( ( G e. USGraph /\ E e. Fin /\ U e. V ) -> ( G ClNeighbVtx U ) 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		rabfi	$$⊢E\in \mathrm{Fin}\to \left\{e\in E|U\in e\right\}\in \mathrm{Fin}$$
4	3	3ad2ant2	$$⊢\left(G\in \mathrm{USGraph}\wedge E\in \mathrm{Fin}\wedge U\in V\right)\to \left\{e\in E|U\in e\right\}\in \mathrm{Fin}$$
5	1 2	edgusgrclnbfin	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 |-
6	5	3adant2	Could not format ( ( G e. USGraph /\ E e. Fin /\ U e. V ) -> ( ( G ClNeighbVtx U ) e. Fin <-> { e e. E | U e. e } e. Fin ) ) : No typesetting found for |- ( ( G e. USGraph /\ E e. Fin /\ U e. V ) -> ( ( G ClNeighbVtx U ) e. Fin <-> { e e. E | U e. e } e. Fin ) ) with typecode |-
7	4 6	mpbird	Could not format ( ( G e. USGraph /\ E e. Fin /\ U e. V ) -> ( G ClNeighbVtx U ) e. Fin ) : No typesetting found for |- ( ( G e. USGraph /\ E e. Fin /\ U e. V ) -> ( G ClNeighbVtx U ) e. Fin ) with typecode |-