Metamath Proof Explorer

Theorem nbfusgrlevtxm2

Description: If there is a vertex which is not a neighbor of another vertex, the number of neighbors of the other vertex is at most the number of vertices of the graph minus 2 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 nbfusgrlevtxm2 ⊢G∈FinUSGraph∧U∈V∧M∈V∧M≠U∧M∉GNeighbVtxU→GNeighbVtxU≤V−2

Proof

Step Hyp Ref Expression
1 hashnbusgrnn0.v ⊢V=Vtx⁡G
2 1 fvexi ⊢V∈V
3 difexg ⊢V∈V→V∖MU∈V
4 2 3 mp1i ⊢G∈FinUSGraph∧U∈V∧M∈V∧M≠U∧M∉GNeighbVtxU→V∖MU∈V
5 simpr3 ⊢G∈FinUSGraph∧U∈V∧M∈V∧M≠U∧M∉GNeighbVtxU→M∉GNeighbVtxU
6 1 nbgrssvwo2 ⊢M∉GNeighbVtxU→GNeighbVtxU⊆V∖MU
7 5 6 syl ⊢G∈FinUSGraph∧U∈V∧M∈V∧M≠U∧M∉GNeighbVtxU→GNeighbVtxU⊆V∖MU
8 hashss ⊢V∖MU∈V∧GNeighbVtxU⊆V∖MU→GNeighbVtxU≤V∖MU
9 4 7 8 syl2anc ⊢G∈FinUSGraph∧U∈V∧M∈V∧M≠U∧M∉GNeighbVtxU→GNeighbVtxU≤V∖MU
10 1 fusgrvtxfi ⊢G∈FinUSGraph→V∈Fin
11 10 ad2antrr ⊢G∈FinUSGraph∧U∈V∧M∈V∧M≠U∧M∉GNeighbVtxU→V∈Fin
12 simpr1 ⊢G∈FinUSGraph∧U∈V∧M∈V∧M≠U∧M∉GNeighbVtxU→M∈V
13 simplr ⊢G∈FinUSGraph∧U∈V∧M∈V∧M≠U∧M∉GNeighbVtxU→U∈V
14 simpr2 ⊢G∈FinUSGraph∧U∈V∧M∈V∧M≠U∧M∉GNeighbVtxU→M≠U
15 hashdifpr ⊢V∈Fin∧M∈V∧U∈V∧M≠U→V∖MU=V−2
16 11 12 13 14 15 syl13anc ⊢G∈FinUSGraph∧U∈V∧M∈V∧M≠U∧M∉GNeighbVtxU→V∖MU=V−2
17 9 16 breqtrd ⊢G∈FinUSGraph∧U∈V∧M∈V∧M≠U∧M∉GNeighbVtxU→GNeighbVtxU≤V−2