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 485 |
. . . . . . . 8
⊢ ((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) → (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) |
4 | 3 | adantr 481 |
. . . . . . 7
⊢ (((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈)) → (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) |
5 | | simprl 768 |
. . . . . . 7
⊢ (((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈)) → 𝑀 ∈ 𝑉) |
6 | | simpr 485 |
. . . . . . . 8
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈) → 𝑀 ≠ 𝑈) |
7 | 6 | adantl 482 |
. . . . . . 7
⊢ (((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈)) → 𝑀 ≠ 𝑈) |
8 | | df-nel 3050 |
. . . . . . . . . 10
⊢ (𝑀 ∉ (𝐺 NeighbVtx 𝑈) ↔ ¬ 𝑀 ∈ (𝐺 NeighbVtx 𝑈)) |
9 | 8 | biimpri 227 |
. . . . . . . . 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 27745 |
. . . . . . 7
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈 ∧ 𝑀 ∉ (𝐺 NeighbVtx 𝑈))) → (♯‘(𝐺 NeighbVtx 𝑈)) ≤ ((♯‘𝑉) − 2)) |
14 | 4, 5, 7, 11, 13 | syl13anc 1371 |
. . . . . 6
⊢ (((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈)) → (♯‘(𝐺 NeighbVtx 𝑈)) ≤ ((♯‘𝑉) − 2)) |
15 | | breq1 5077 |
. . . . . . . . 9
⊢
((♯‘(𝐺
NeighbVtx 𝑈)) =
((♯‘𝑉) −
1) → ((♯‘(𝐺 NeighbVtx 𝑈)) ≤ ((♯‘𝑉) − 2) ↔ ((♯‘𝑉) − 1) ≤
((♯‘𝑉) −
2))) |
16 | 15 | adantl 482 |
. . . . . . . 8
⊢ ((((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈)) ∧ (♯‘(𝐺 NeighbVtx 𝑈)) = ((♯‘𝑉) − 1)) → ((♯‘(𝐺 NeighbVtx 𝑈)) ≤ ((♯‘𝑉) − 2) ↔ ((♯‘𝑉) − 1) ≤
((♯‘𝑉) −
2))) |
17 | 12 | fusgrvtxfi 27686 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ FinUSGraph → 𝑉 ∈ Fin) |
18 | | hashcl 14071 |
. . . . . . . . . . . 12
⊢ (𝑉 ∈ Fin →
(♯‘𝑉) ∈
ℕ0) |
19 | | nn0re 12242 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑉)
∈ ℕ0 → (♯‘𝑉) ∈ ℝ) |
20 | | 1red 10976 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝑉)
∈ ℝ → 1 ∈ ℝ) |
21 | | 2re 12047 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ |
22 | 21 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝑉)
∈ ℝ → 2 ∈ ℝ) |
23 | | id 22 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝑉)
∈ ℝ → (♯‘𝑉) ∈ ℝ) |
24 | | 1lt2 12144 |
. . . . . . . . . . . . . . . 16
⊢ 1 <
2 |
25 | 24 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝑉)
∈ ℝ → 1 < 2) |
26 | 20, 22, 23, 25 | ltsub2dd 11588 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝑉)
∈ ℝ → ((♯‘𝑉) − 2) < ((♯‘𝑉) − 1)) |
27 | 23, 22 | resubcld 11403 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝑉)
∈ ℝ → ((♯‘𝑉) − 2) ∈
ℝ) |
28 | | peano2rem 11288 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝑉)
∈ ℝ → ((♯‘𝑉) − 1) ∈
ℝ) |
29 | 27, 28 | ltnled 11122 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝑉)
∈ ℝ → (((♯‘𝑉) − 2) < ((♯‘𝑉) − 1) ↔ ¬
((♯‘𝑉) −
1) ≤ ((♯‘𝑉)
− 2))) |
30 | 26, 29 | mpbid 231 |
. . . . . . . . . . . . 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 121 |
. . . . . . . . . 10
⊢ (𝐺 ∈ FinUSGraph →
(((♯‘𝑉) −
1) ≤ ((♯‘𝑉)
− 2) → 𝑀 ∈
(𝐺 NeighbVtx 𝑈))) |
34 | 33 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) → (((♯‘𝑉) − 1) ≤ ((♯‘𝑉) − 2) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈))) |
35 | 34 | ad3antlr 728 |
. . . . . . . 8
⊢ ((((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈)) ∧ (♯‘(𝐺 NeighbVtx 𝑈)) = ((♯‘𝑉) − 1)) → (((♯‘𝑉) − 1) ≤
((♯‘𝑉) −
2) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈))) |
36 | 16, 35 | sylbid 239 |
. . . . . . 7
⊢ ((((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈)) ∧ (♯‘(𝐺 NeighbVtx 𝑈)) = ((♯‘𝑉) − 1)) → ((♯‘(𝐺 NeighbVtx 𝑈)) ≤ ((♯‘𝑉) − 2) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈))) |
37 | 36 | ex 413 |
. . . . . 6
⊢ (((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈)) → ((♯‘(𝐺 NeighbVtx 𝑈)) = ((♯‘𝑉) − 1) → ((♯‘(𝐺 NeighbVtx 𝑈)) ≤ ((♯‘𝑉) − 2) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈)))) |
38 | 14, 37 | mpid 44 |
. . . . 5
⊢ (((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈)) → ((♯‘(𝐺 NeighbVtx 𝑈)) = ((♯‘𝑉) − 1) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈))) |
39 | 38 | ex 413 |
. . . 4
⊢ ((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) → ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈) → ((♯‘(𝐺 NeighbVtx 𝑈)) = ((♯‘𝑉) − 1) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈)))) |
40 | 39 | com23 86 |
. . 3
⊢ ((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) → ((♯‘(𝐺 NeighbVtx 𝑈)) = ((♯‘𝑉) − 1) → ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈)))) |
41 | 40 | ex 413 |
. 2
⊢ (¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) → ((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) → ((♯‘(𝐺 NeighbVtx 𝑈)) = ((♯‘𝑉) − 1) → ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈))))) |
42 | 2, 41 | pm2.61i 182 |
1
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) → ((♯‘(𝐺 NeighbVtx 𝑈)) = ((♯‘𝑉) − 1) → ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈)))) |