Theorem clnbfiusgrfi

Description: The closed neighborhood of a vertex in a finite simple graph is a finite set. (Contributed by AV, 10-May-2025)

	Ref	Expression
Assertion	clnbfiusgrfi	Could not format assertion : No typesetting found for |- ( ( G e. FinUSGraph /\ N e. ( Vtx ` G ) ) -> ( G ClNeighbVtx N ) e. Fin ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		fusgrusgr	$$⊢G\in \mathrm{FinUSGraph}\to G\in \mathrm{USGraph}$$
2	1	adantr	$$⊢\left(G\in \mathrm{FinUSGraph}\wedge N\in \mathrm{Vtx}\left(G\right)\right)\to G\in \mathrm{USGraph}$$
3		fusgrfis	$$⊢G\in \mathrm{FinUSGraph}\to \mathrm{Edg}\left(G\right)\in \mathrm{Fin}$$
4	3	adantr	$$⊢\left(G\in \mathrm{FinUSGraph}\wedge N\in \mathrm{Vtx}\left(G\right)\right)\to \mathrm{Edg}\left(G\right)\in \mathrm{Fin}$$
5		simpr	$$⊢\left(G\in \mathrm{FinUSGraph}\wedge N\in \mathrm{Vtx}\left(G\right)\right)\to N\in \mathrm{Vtx}\left(G\right)$$
6		eqid	$$⊢\mathrm{Vtx}\left(G\right)=\mathrm{Vtx}\left(G\right)$$
7		eqid	$$⊢\mathrm{Edg}\left(G\right)=\mathrm{Edg}\left(G\right)$$
8	6 7	clnbusgrfi	Could not format ( ( G e. USGraph /\ ( Edg ` G ) e. Fin /\ N e. ( Vtx ` G ) ) -> ( G ClNeighbVtx N ) e. Fin ) : No typesetting found for |- ( ( G e. USGraph /\ ( Edg ` G ) e. Fin /\ N e. ( Vtx ` G ) ) -> ( G ClNeighbVtx N ) e. Fin ) with typecode |-
9	2 4 5 8	syl3anc	Could not format ( ( G e. FinUSGraph /\ N e. ( Vtx ` G ) ) -> ( G ClNeighbVtx N ) e. Fin ) : No typesetting found for |- ( ( G e. FinUSGraph /\ N e. ( Vtx ` G ) ) -> ( G ClNeighbVtx N ) e. Fin ) with typecode |-