Theorem nbfusgrlevtxm1

Description: The number of neighbors of a vertex is at most the number of vertices of the graph minus 1 in a finite simple graph. (Contributed by AV, 16-Dec-2020) (Proof shortened by AV, 13-Feb-2022)

	Ref	Expression
Hypothesis	hashnbusgrnn0.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	nbfusgrlevtxm1	$$⊢\left(G\in \mathrm{FinUSGraph}\wedge U\in V\right)\to \left|G\mathrm{NeighbVtx}U\right|\le \left|V\right|-1$$

Proof

Step	Hyp	Ref	Expression
1		hashnbusgrnn0.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2	1	fvexi	$$⊢V\in \mathrm{V}$$
3	2	difexi	$$⊢V\setminus \left\{U\right\}\in \mathrm{V}$$
4	1	nbgrssovtx	$$⊢G\mathrm{NeighbVtx}U\subseteq V\setminus \left\{U\right\}$$
5	4	a1i	$$⊢\left(G\in \mathrm{FinUSGraph}\wedge U\in V\right)\to G\mathrm{NeighbVtx}U\subseteq V\setminus \left\{U\right\}$$
6		hashss	$$⊢\left(V\setminus \left\{U\right\}\in \mathrm{V}\wedge G\mathrm{NeighbVtx}U\subseteq V\setminus \left\{U\right\}\right)\to \left|G\mathrm{NeighbVtx}U\right|\le \left|V\setminus \left\{U\right\}\right|$$
7	3 5 6	sylancr	$$⊢\left(G\in \mathrm{FinUSGraph}\wedge U\in V\right)\to \left|G\mathrm{NeighbVtx}U\right|\le \left|V\setminus \left\{U\right\}\right|$$
8	1	fusgrvtxfi	$$⊢G\in \mathrm{FinUSGraph}\to V\in \mathrm{Fin}$$
9		hashdifsn	$$⊢\left(V\in \mathrm{Fin}\wedge U\in V\right)\to \left|V\setminus \left\{U\right\}\right|=\left|V\right|-1$$
10	9	eqcomd	$$⊢\left(V\in \mathrm{Fin}\wedge U\in V\right)\to \left|V\right|-1=\left|V\setminus \left\{U\right\}\right|$$
11	8 10	sylan	$$⊢\left(G\in \mathrm{FinUSGraph}\wedge U\in V\right)\to \left|V\right|-1=\left|V\setminus \left\{U\right\}\right|$$
12	7 11	breqtrrd	$$⊢\left(G\in \mathrm{FinUSGraph}\wedge U\in V\right)\to \left|G\mathrm{NeighbVtx}U\right|\le \left|V\right|-1$$