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 ∉ G NeighbVtx U → G NeighbVtx U ≤ V − 2

Proof

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