This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )