Metamath Proof Explorer

Theorem nbusgrvtxm1

Description: If the number of neighbors of a vertex in a finite simple graph is the number of vertices of the graph minus 1, each vertex except the first mentioned vertex is a neighbor of this vertex. (Contributed by Alexander van der Vekens, 14-Jul-2018) (Revised by AV, 16-Dec-2020)

Ref Expression
Hypothesis hashnbusgrnn0.v ⊢ V = Vtx ⁡ G
Assertion nbusgrvtxm1 ⊢ G ∈ FinUSGraph ∧ U ∈ V → G NeighbVtx U = V − 1 → M ∈ V ∧ M ≠ U → M ∈ G NeighbVtx U

Proof

Step Hyp Ref Expression
1 hashnbusgrnn0.v ⊢ V = Vtx ⁡ G
2 ax-1 ⊢ M ∈ G NeighbVtx U → M ∈ V ∧ M ≠ U → M ∈ G NeighbVtx U
3 2 2a1d ⊢ M ∈ G NeighbVtx U → G ∈ FinUSGraph ∧ U ∈ V → G NeighbVtx U = V − 1 → M ∈ V ∧ M ≠ U → M ∈ G NeighbVtx U
4 simpr ⊢ ¬ M ∈ G NeighbVtx U ∧ G ∈ FinUSGraph ∧ U ∈ V → G ∈ FinUSGraph ∧ U ∈ V
5 4 adantr ⊢ ¬ M ∈ G NeighbVtx U ∧ G ∈ FinUSGraph ∧ U ∈ V ∧ M ∈ V ∧ M ≠ U → G ∈ FinUSGraph ∧ U ∈ V
6 simprl ⊢ ¬ M ∈ G NeighbVtx U ∧ G ∈ FinUSGraph ∧ U ∈ V ∧ M ∈ V ∧ M ≠ U → M ∈ V
7 simpr ⊢ M ∈ V ∧ M ≠ U → M ≠ U
8 7 adantl ⊢ ¬ M ∈ G NeighbVtx U ∧ G ∈ FinUSGraph ∧ U ∈ V ∧ M ∈ V ∧ M ≠ U → M ≠ U
9 df-nel ⊢ M ∉ G NeighbVtx U ↔ ¬ M ∈ G NeighbVtx U
10 9 biimpri ⊢ ¬ M ∈ G NeighbVtx U → M ∉ G NeighbVtx U
11 10 adantr ⊢ ¬ M ∈ G NeighbVtx U ∧ G ∈ FinUSGraph ∧ U ∈ V → M ∉ G NeighbVtx U
12 11 adantr ⊢ ¬ M ∈ G NeighbVtx U ∧ G ∈ FinUSGraph ∧ U ∈ V ∧ M ∈ V ∧ M ≠ U → M ∉ G NeighbVtx U
13 1 nbfusgrlevtxm2 ⊢ G ∈ FinUSGraph ∧ U ∈ V ∧ M ∈ V ∧ M ≠ U ∧ M ∉ G NeighbVtx U → G NeighbVtx U ≤ V − 2
14 5 6 8 12 13 syl13anc ⊢ ¬ M ∈ G NeighbVtx U ∧ G ∈ FinUSGraph ∧ U ∈ V ∧ M ∈ V ∧ M ≠ U → G NeighbVtx U ≤ V − 2
15 breq1 ⊢ G NeighbVtx U = V − 1 → G NeighbVtx U ≤ V − 2 ↔ V − 1 ≤ V − 2
16 15 adantl ⊢ ¬ M ∈ G NeighbVtx U ∧ G ∈ FinUSGraph ∧ U ∈ V ∧ M ∈ V ∧ M ≠ U ∧ G NeighbVtx U = V − 1 → G NeighbVtx U ≤ V − 2 ↔ V − 1 ≤ V − 2
17 1 fusgrvtxfi ⊢ G ∈ FinUSGraph → V ∈ Fin
18 hashcl ⊢ V ∈ Fin → V ∈ ℕ 0
19 nn0re ⊢ V ∈ ℕ 0 → V ∈ ℝ
20 1red ⊢ V ∈ ℝ → 1 ∈ ℝ
21 2re ⊢ 2 ∈ ℝ
22 21 a1i ⊢ V ∈ ℝ → 2 ∈ ℝ
23 id ⊢ V ∈ ℝ → V ∈ ℝ
24 1lt2 ⊢ 1 < 2
25 24 a1i ⊢ V ∈ ℝ → 1 < 2
26 20 22 23 25 ltsub2dd ⊢ V ∈ ℝ → V − 2 < V − 1
27 23 22 resubcld ⊢ V ∈ ℝ → V − 2 ∈ ℝ
28 peano2rem ⊢ V ∈ ℝ → V − 1 ∈ ℝ
29 27 28 ltnled ⊢ V ∈ ℝ → V − 2 < V − 1 ↔ ¬ V − 1 ≤ V − 2
30 26 29 mpbid ⊢ V ∈ ℝ → ¬ V − 1 ≤ V − 2
31 17 18 19 30 4syl ⊢ G ∈ FinUSGraph → ¬ V − 1 ≤ V − 2
32 31 pm2.21d ⊢ G ∈ FinUSGraph → V − 1 ≤ V − 2 → M ∈ G NeighbVtx U
33 32 adantr ⊢ G ∈ FinUSGraph ∧ U ∈ V → V − 1 ≤ V − 2 → M ∈ G NeighbVtx U
34 33 ad3antlr ⊢ ¬ M ∈ G NeighbVtx U ∧ G ∈ FinUSGraph ∧ U ∈ V ∧ M ∈ V ∧ M ≠ U ∧ G NeighbVtx U = V − 1 → V − 1 ≤ V − 2 → M ∈ G NeighbVtx U
35 16 34 sylbid ⊢ ¬ M ∈ G NeighbVtx U ∧ G ∈ FinUSGraph ∧ U ∈ V ∧ M ∈ V ∧ M ≠ U ∧ G NeighbVtx U = V − 1 → G NeighbVtx U ≤ V − 2 → M ∈ G NeighbVtx U
36 35 ex ⊢ ¬ M ∈ G NeighbVtx U ∧ G ∈ FinUSGraph ∧ U ∈ V ∧ M ∈ V ∧ M ≠ U → G NeighbVtx U = V − 1 → G NeighbVtx U ≤ V − 2 → M ∈ G NeighbVtx U
37 14 36 mpid ⊢ ¬ M ∈ G NeighbVtx U ∧ G ∈ FinUSGraph ∧ U ∈ V ∧ M ∈ V ∧ M ≠ U → G NeighbVtx U = V − 1 → M ∈ G NeighbVtx U
38 37 ex ⊢ ¬ M ∈ G NeighbVtx U ∧ G ∈ FinUSGraph ∧ U ∈ V → M ∈ V ∧ M ≠ U → G NeighbVtx U = V − 1 → M ∈ G NeighbVtx U
39 38 com23 ⊢ ¬ M ∈ G NeighbVtx U ∧ G ∈ FinUSGraph ∧ U ∈ V → G NeighbVtx U = V − 1 → M ∈ V ∧ M ≠ U → M ∈ G NeighbVtx U
40 39 ex ⊢ ¬ M ∈ G NeighbVtx U → G ∈ FinUSGraph ∧ U ∈ V → G NeighbVtx U = V − 1 → M ∈ V ∧ M ≠ U → M ∈ G NeighbVtx U
41 3 40 pm2.61i ⊢ G ∈ FinUSGraph ∧ U ∈ V → G NeighbVtx U = V − 1 → M ∈ V ∧ M ≠ U → M ∈ G NeighbVtx U