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