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 ⊢ V = Vtx ⁡ G
Assertion nbfusgrlevtxm1 ⊢ G ∈ FinUSGraph ∧ U ∈ V → G NeighbVtx U ≤ V − 1

Proof

Step Hyp Ref Expression
1 hashnbusgrnn0.v ⊢ V = Vtx ⁡ G
2 1 fvexi ⊢ V ∈ V
3 2 difexi ⊢ V ∖ U ∈ V
4 1 nbgrssovtx ⊢ G NeighbVtx U ⊆ V ∖ U
5 4 a1i ⊢ G ∈ FinUSGraph ∧ U ∈ V → G NeighbVtx U ⊆ V ∖ U
6 hashss ⊢ V ∖ U ∈ V ∧ G NeighbVtx U ⊆ V ∖ U → G NeighbVtx U ≤ V ∖ U
7 3 5 6 sylancr ⊢ G ∈ FinUSGraph ∧ U ∈ V → G NeighbVtx U ≤ V ∖ U
8 1 fusgrvtxfi ⊢ G ∈ FinUSGraph → V ∈ Fin
9 hashdifsn ⊢ V ∈ Fin ∧ U ∈ V → V ∖ U = V − 1
10 9 eqcomd ⊢ V ∈ Fin ∧ U ∈ V → V − 1 = V ∖ U
11 8 10 sylan ⊢ G ∈ FinUSGraph ∧ U ∈ V → V − 1 = V ∖ U
12 7 11 breqtrrd ⊢ G ∈ FinUSGraph ∧ U ∈ V → G NeighbVtx U ≤ V − 1