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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	nbfusgrlevtxm1	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) ≤ ( ( ♯ ‘ 𝑉 ) − 1 ) )

Proof

Step	Hyp	Ref	Expression
1		hashnbusgrnn0.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2	1	fvexi	⊢ 𝑉 ∈ V
3	2	difexi	⊢ ( 𝑉 ∖ { 𝑈 } ) ∈ V
4	1	nbgrssovtx	⊢ ( 𝐺 NeighbVtx 𝑈 ) ⊆ ( 𝑉 ∖ { 𝑈 } )
5	4	a1i	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝐺 NeighbVtx 𝑈 ) ⊆ ( 𝑉 ∖ { 𝑈 } ) )
6		hashss	⊢ ( ( ( 𝑉 ∖ { 𝑈 } ) ∈ V ∧ ( 𝐺 NeighbVtx 𝑈 ) ⊆ ( 𝑉 ∖ { 𝑈 } ) ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) ≤ ( ♯ ‘ ( 𝑉 ∖ { 𝑈 } ) ) )
7	3 5 6	sylancr	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) ≤ ( ♯ ‘ ( 𝑉 ∖ { 𝑈 } ) ) )
8	1	fusgrvtxfi	⊢ ( 𝐺 ∈ FinUSGraph → 𝑉 ∈ Fin )
9		hashdifsn	⊢ ( ( 𝑉 ∈ Fin ∧ 𝑈 ∈ 𝑉 ) → ( ♯ ‘ ( 𝑉 ∖ { 𝑈 } ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) )
10	9	eqcomd	⊢ ( ( 𝑉 ∈ Fin ∧ 𝑈 ∈ 𝑉 ) → ( ( ♯ ‘ 𝑉 ) − 1 ) = ( ♯ ‘ ( 𝑉 ∖ { 𝑈 } ) ) )
11	8 10	sylan	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( ♯ ‘ 𝑉 ) − 1 ) = ( ♯ ‘ ( 𝑉 ∖ { 𝑈 } ) ) )
12	7 11	breqtrrd	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) ≤ ( ( ♯ ‘ 𝑉 ) − 1 ) )