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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion nbusgrvtxm1 ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) → ( ( 𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈 ) → 𝑀 ∈ ( 𝐺 NeighbVtx 𝑈 ) ) ) )

Proof

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