Proof of Theorem nbusgrvtxm1
Step | Hyp | Ref
| Expression |
1 | | ax-1 6 |
. . 3
⊢ (𝑀 ∈ (𝐺 NeighbVtx 𝑈) → ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈))) |
2 | 1 | 2a1d 26 |
. 2
⊢ (𝑀 ∈ (𝐺 NeighbVtx 𝑈) → ((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) → ((#‘(𝐺 NeighbVtx 𝑈)) = ((#‘𝑉) − 1) → ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈))))) |
3 | | simpr 477 |
. . . . . . . 8
⊢ ((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) → (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) |
4 | 3 | adantr 481 |
. . . . . . 7
⊢ (((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈)) → (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) |
5 | | simprl 794 |
. . . . . . 7
⊢ (((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈)) → 𝑀 ∈ 𝑉) |
6 | | simpr 477 |
. . . . . . . 8
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈) → 𝑀 ≠ 𝑈) |
7 | 6 | adantl 482 |
. . . . . . 7
⊢ (((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈)) → 𝑀 ≠ 𝑈) |
8 | | df-nel 2898 |
. . . . . . . . . 10
⊢ (𝑀 ∉ (𝐺 NeighbVtx 𝑈) ↔ ¬ 𝑀 ∈ (𝐺 NeighbVtx 𝑈)) |
9 | 8 | biimpri 218 |
. . . . . . . . 9
⊢ (¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) → 𝑀 ∉ (𝐺 NeighbVtx 𝑈)) |
10 | 9 | adantr 481 |
. . . . . . . 8
⊢ ((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) → 𝑀 ∉ (𝐺 NeighbVtx 𝑈)) |
11 | 10 | adantr 481 |
. . . . . . 7
⊢ (((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈)) → 𝑀 ∉ (𝐺 NeighbVtx 𝑈)) |
12 | | hashnbusgrnn0.v |
. . . . . . . 8
⊢ 𝑉 = (Vtx‘𝐺) |
13 | 12 | nbfusgrlevtxm2 26280 |
. . . . . . 7
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈 ∧ 𝑀 ∉ (𝐺 NeighbVtx 𝑈))) → (#‘(𝐺 NeighbVtx 𝑈)) ≤ ((#‘𝑉) − 2)) |
14 | 4, 5, 7, 11, 13 | syl13anc 1328 |
. . . . . 6
⊢ (((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈)) → (#‘(𝐺 NeighbVtx 𝑈)) ≤ ((#‘𝑉) − 2)) |
15 | | breq1 4656 |
. . . . . . . . 9
⊢
((#‘(𝐺
NeighbVtx 𝑈)) =
((#‘𝑉) − 1)
→ ((#‘(𝐺
NeighbVtx 𝑈)) ≤
((#‘𝑉) − 2)
↔ ((#‘𝑉) −
1) ≤ ((#‘𝑉)
− 2))) |
16 | 15 | adantl 482 |
. . . . . . . 8
⊢ ((((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈)) ∧ (#‘(𝐺 NeighbVtx 𝑈)) = ((#‘𝑉) − 1)) → ((#‘(𝐺 NeighbVtx 𝑈)) ≤ ((#‘𝑉) − 2) ↔ ((#‘𝑉) − 1) ≤
((#‘𝑉) −
2))) |
17 | 12 | fusgrvtxfi 26211 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ FinUSGraph → 𝑉 ∈ Fin) |
18 | | hashcl 13147 |
. . . . . . . . . . . 12
⊢ (𝑉 ∈ Fin →
(#‘𝑉) ∈
ℕ0) |
19 | | nn0re 11301 |
. . . . . . . . . . . . 13
⊢
((#‘𝑉) ∈
ℕ0 → (#‘𝑉) ∈ ℝ) |
20 | | 1red 10055 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑉) ∈
ℝ → 1 ∈ ℝ) |
21 | | 2re 11090 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ |
22 | 21 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑉) ∈
ℝ → 2 ∈ ℝ) |
23 | | id 22 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑉) ∈
ℝ → (#‘𝑉)
∈ ℝ) |
24 | | 1lt2 11194 |
. . . . . . . . . . . . . . . 16
⊢ 1 <
2 |
25 | 24 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑉) ∈
ℝ → 1 < 2) |
26 | 20, 22, 23, 25 | ltsub2dd 10640 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑉) ∈
ℝ → ((#‘𝑉)
− 2) < ((#‘𝑉) − 1)) |
27 | 23, 22 | resubcld 10458 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑉) ∈
ℝ → ((#‘𝑉)
− 2) ∈ ℝ) |
28 | | peano2rem 10348 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑉) ∈
ℝ → ((#‘𝑉)
− 1) ∈ ℝ) |
29 | 27, 28 | ltnled 10184 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑉) ∈
ℝ → (((#‘𝑉) − 2) < ((#‘𝑉) − 1) ↔ ¬
((#‘𝑉) − 1)
≤ ((#‘𝑉) −
2))) |
30 | 26, 29 | mpbid 222 |
. . . . . . . . . . . . 13
⊢
((#‘𝑉) ∈
ℝ → ¬ ((#‘𝑉) − 1) ≤ ((#‘𝑉) − 2)) |
31 | 19, 30 | syl 17 |
. . . . . . . . . . . 12
⊢
((#‘𝑉) ∈
ℕ0 → ¬ ((#‘𝑉) − 1) ≤ ((#‘𝑉) − 2)) |
32 | 17, 18, 31 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ FinUSGraph → ¬
((#‘𝑉) − 1)
≤ ((#‘𝑉) −
2)) |
33 | 32 | pm2.21d 118 |
. . . . . . . . . 10
⊢ (𝐺 ∈ FinUSGraph →
(((#‘𝑉) − 1)
≤ ((#‘𝑉) −
2) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈))) |
34 | 33 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) → (((#‘𝑉) − 1) ≤ ((#‘𝑉) − 2) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈))) |
35 | 34 | ad3antlr 767 |
. . . . . . . 8
⊢ ((((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈)) ∧ (#‘(𝐺 NeighbVtx 𝑈)) = ((#‘𝑉) − 1)) → (((#‘𝑉) − 1) ≤
((#‘𝑉) − 2)
→ 𝑀 ∈ (𝐺 NeighbVtx 𝑈))) |
36 | 16, 35 | sylbid 230 |
. . . . . . 7
⊢ ((((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈)) ∧ (#‘(𝐺 NeighbVtx 𝑈)) = ((#‘𝑉) − 1)) → ((#‘(𝐺 NeighbVtx 𝑈)) ≤ ((#‘𝑉) − 2) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈))) |
37 | 36 | ex 450 |
. . . . . 6
⊢ (((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈)) → ((#‘(𝐺 NeighbVtx 𝑈)) = ((#‘𝑉) − 1) → ((#‘(𝐺 NeighbVtx 𝑈)) ≤ ((#‘𝑉) − 2) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈)))) |
38 | 14, 37 | mpid 44 |
. . . . 5
⊢ (((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈)) → ((#‘(𝐺 NeighbVtx 𝑈)) = ((#‘𝑉) − 1) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈))) |
39 | 38 | ex 450 |
. . . 4
⊢ ((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) → ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈) → ((#‘(𝐺 NeighbVtx 𝑈)) = ((#‘𝑉) − 1) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈)))) |
40 | 39 | com23 86 |
. . 3
⊢ ((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) → ((#‘(𝐺 NeighbVtx 𝑈)) = ((#‘𝑉) − 1) → ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈)))) |
41 | 40 | ex 450 |
. 2
⊢ (¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) → ((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) → ((#‘(𝐺 NeighbVtx 𝑈)) = ((#‘𝑉) − 1) → ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈))))) |
42 | 2, 41 | pm2.61i 176 |
1
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) → ((#‘(𝐺 NeighbVtx 𝑈)) = ((#‘𝑉) − 1) → ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈)))) |