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 biranri ⊢ ¬ M ∈ G NeighbVtx U ∧ G ∈ FinUSGraph ∧ U ∈ V → M ∉ G NeighbVtx U
11 10 adantr ⊢ ¬ M ∈ G NeighbVtx U ∧ G ∈ FinUSGraph ∧ U ∈ V ∧ M ∈ V ∧ M ≠ U → M ∉ G NeighbVtx U
12 1 nbfusgrlevtxm2 ⊢ G ∈ FinUSGraph ∧ U ∈ V ∧ M ∈ V ∧ M ≠ U ∧ M ∉ G NeighbVtx U → G NeighbVtx U ≤ V − 2
13 5 6 8 11 12 syl13anc ⊢ ¬ M ∈ G NeighbVtx U ∧ G ∈ FinUSGraph ∧ U ∈ V ∧ M ∈ V ∧ M ≠ U → G NeighbVtx U ≤ V − 2
14 breq1 ⊢ G NeighbVtx U = V − 1 → G NeighbVtx U ≤ V − 2 ↔ V − 1 ≤ V − 2
15 14 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
16 1 fusgrvtxfi ⊢ G ∈ FinUSGraph → V ∈ Fin
17 hashcl ⊢ V ∈ Fin → V ∈ ℕ 0
18 nn0re ⊢ V ∈ ℕ 0 → V ∈ ℝ
19 1red ⊢ V ∈ ℝ → 1 ∈ ℝ
20 2re ⊢ 2 ∈ ℝ
21 20 a1i ⊢ V ∈ ℝ → 2 ∈ ℝ
22 id ⊢ V ∈ ℝ → V ∈ ℝ
23 1lt2 ⊢ 1 < 2
24 23 a1i ⊢ V ∈ ℝ → 1 < 2
25 19 21 22 24 ltsub2dd ⊢ V ∈ ℝ → V − 2 < V − 1
26 22 21 resubcld ⊢ V ∈ ℝ → V − 2 ∈ ℝ
27 peano2rem ⊢ V ∈ ℝ → V − 1 ∈ ℝ
28 26 27 ltnled ⊢ V ∈ ℝ → V − 2 < V − 1 ↔ ¬ V − 1 ≤ V − 2
29 25 28 mpbid ⊢ V ∈ ℝ → ¬ V − 1 ≤ V − 2
30 16 17 18 29 4syl ⊢ G ∈ FinUSGraph → ¬ V − 1 ≤ V − 2
31 30 pm2.21d ⊢ G ∈ FinUSGraph → V − 1 ≤ V − 2 → M ∈ G NeighbVtx U
32 31 adantr ⊢ G ∈ FinUSGraph ∧ U ∈ V → V − 1 ≤ V − 2 → M ∈ G NeighbVtx U
33 32 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
34 15 33 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
35 34 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
36 13 35 mpid ⊢ ¬ M ∈ G NeighbVtx U ∧ G ∈ FinUSGraph ∧ U ∈ V ∧ M ∈ V ∧ M ≠ U → G NeighbVtx U = V − 1 → M ∈ G NeighbVtx U
37 36 ex ⊢ ¬ M ∈ G NeighbVtx U ∧ G ∈ FinUSGraph ∧ U ∈ V → M ∈ V ∧ M ≠ U → G NeighbVtx U = V − 1 → M ∈ G NeighbVtx U
38 37 com23 ⊢ ¬ M ∈ G NeighbVtx U ∧ G ∈ FinUSGraph ∧ U ∈ V → G NeighbVtx U = V − 1 → M ∈ V ∧ M ≠ U → M ∈ G NeighbVtx U
39 38 ex ⊢ ¬ M ∈ G NeighbVtx U → G ∈ FinUSGraph ∧ U ∈ V → G NeighbVtx U = V − 1 → M ∈ V ∧ M ≠ U → M ∈ G NeighbVtx U
40 3 39 pm2.61i ⊢ G ∈ FinUSGraph ∧ U ∈ V → G NeighbVtx U = V − 1 → M ∈ V ∧ M ≠ U → M ∈ G NeighbVtx U