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 484 |
. . . . . . . 8
⊢ ((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) → (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) |
| 4 | 3 | adantr 480 |
. . . . . . 7
⊢ (((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈)) → (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) |
| 5 | | simprl 771 |
. . . . . . 7
⊢ (((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈)) → 𝑀 ∈ 𝑉) |
| 6 | | simpr 484 |
. . . . . . . 8
⊢ ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈) → 𝑀 ≠ 𝑈) |
| 7 | 6 | adantl 481 |
. . . . . . 7
⊢ (((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈)) → 𝑀 ≠ 𝑈) |
| 8 | | df-nel 3047 |
. . . . . . . . . 10
⊢ (𝑀 ∉ (𝐺 NeighbVtx 𝑈) ↔ ¬ 𝑀 ∈ (𝐺 NeighbVtx 𝑈)) |
| 9 | 8 | biimpri 228 |
. . . . . . . . 9
⊢ (¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) → 𝑀 ∉ (𝐺 NeighbVtx 𝑈)) |
| 10 | 9 | adantr 480 |
. . . . . . . 8
⊢ ((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) → 𝑀 ∉ (𝐺 NeighbVtx 𝑈)) |
| 11 | 10 | adantr 480 |
. . . . . . 7
⊢ (((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈)) → 𝑀 ∉ (𝐺 NeighbVtx 𝑈)) |
| 12 | | hashnbusgrnn0.v |
. . . . . . . 8
⊢ 𝑉 = (Vtx‘𝐺) |
| 13 | 12 | nbfusgrlevtxm2 29395 |
. . . . . . 7
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈 ∧ 𝑀 ∉ (𝐺 NeighbVtx 𝑈))) → (♯‘(𝐺 NeighbVtx 𝑈)) ≤ ((♯‘𝑉) − 2)) |
| 14 | 4, 5, 7, 11, 13 | syl13anc 1374 |
. . . . . 6
⊢ (((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈)) → (♯‘(𝐺 NeighbVtx 𝑈)) ≤ ((♯‘𝑉) − 2)) |
| 15 | | breq1 5146 |
. . . . . . . . 9
⊢
((♯‘(𝐺
NeighbVtx 𝑈)) =
((♯‘𝑉) −
1) → ((♯‘(𝐺 NeighbVtx 𝑈)) ≤ ((♯‘𝑉) − 2) ↔ ((♯‘𝑉) − 1) ≤
((♯‘𝑉) −
2))) |
| 16 | 15 | adantl 481 |
. . . . . . . 8
⊢ ((((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈)) ∧ (♯‘(𝐺 NeighbVtx 𝑈)) = ((♯‘𝑉) − 1)) → ((♯‘(𝐺 NeighbVtx 𝑈)) ≤ ((♯‘𝑉) − 2) ↔ ((♯‘𝑉) − 1) ≤
((♯‘𝑉) −
2))) |
| 17 | 12 | fusgrvtxfi 29336 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ FinUSGraph → 𝑉 ∈ Fin) |
| 18 | | hashcl 14395 |
. . . . . . . . . . . 12
⊢ (𝑉 ∈ Fin →
(♯‘𝑉) ∈
ℕ0) |
| 19 | | nn0re 12535 |
. . . . . . . . . . . 12
⊢
((♯‘𝑉)
∈ ℕ0 → (♯‘𝑉) ∈ ℝ) |
| 20 | | 1red 11262 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝑉)
∈ ℝ → 1 ∈ ℝ) |
| 21 | | 2re 12340 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℝ |
| 22 | 21 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝑉)
∈ ℝ → 2 ∈ ℝ) |
| 23 | | id 22 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝑉)
∈ ℝ → (♯‘𝑉) ∈ ℝ) |
| 24 | | 1lt2 12437 |
. . . . . . . . . . . . . . 15
⊢ 1 <
2 |
| 25 | 24 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝑉)
∈ ℝ → 1 < 2) |
| 26 | 20, 22, 23, 25 | ltsub2dd 11876 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑉)
∈ ℝ → ((♯‘𝑉) − 2) < ((♯‘𝑉) − 1)) |
| 27 | 23, 22 | resubcld 11691 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝑉)
∈ ℝ → ((♯‘𝑉) − 2) ∈
ℝ) |
| 28 | | peano2rem 11576 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝑉)
∈ ℝ → ((♯‘𝑉) − 1) ∈
ℝ) |
| 29 | 27, 28 | ltnled 11408 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑉)
∈ ℝ → (((♯‘𝑉) − 2) < ((♯‘𝑉) − 1) ↔ ¬
((♯‘𝑉) −
1) ≤ ((♯‘𝑉)
− 2))) |
| 30 | 26, 29 | mpbid 232 |
. . . . . . . . . . . 12
⊢
((♯‘𝑉)
∈ ℝ → ¬ ((♯‘𝑉) − 1) ≤ ((♯‘𝑉) − 2)) |
| 31 | 17, 18, 19, 30 | 4syl 19 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ FinUSGraph → ¬
((♯‘𝑉) −
1) ≤ ((♯‘𝑉)
− 2)) |
| 32 | 31 | pm2.21d 121 |
. . . . . . . . . 10
⊢ (𝐺 ∈ FinUSGraph →
(((♯‘𝑉) −
1) ≤ ((♯‘𝑉)
− 2) → 𝑀 ∈
(𝐺 NeighbVtx 𝑈))) |
| 33 | 32 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) → (((♯‘𝑉) − 1) ≤ ((♯‘𝑉) − 2) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈))) |
| 34 | 33 | ad3antlr 731 |
. . . . . . . 8
⊢ ((((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈)) ∧ (♯‘(𝐺 NeighbVtx 𝑈)) = ((♯‘𝑉) − 1)) → (((♯‘𝑉) − 1) ≤
((♯‘𝑉) −
2) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈))) |
| 35 | 16, 34 | sylbid 240 |
. . . . . . 7
⊢ ((((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈)) ∧ (♯‘(𝐺 NeighbVtx 𝑈)) = ((♯‘𝑉) − 1)) → ((♯‘(𝐺 NeighbVtx 𝑈)) ≤ ((♯‘𝑉) − 2) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈))) |
| 36 | 35 | ex 412 |
. . . . . 6
⊢ (((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈)) → ((♯‘(𝐺 NeighbVtx 𝑈)) = ((♯‘𝑉) − 1) → ((♯‘(𝐺 NeighbVtx 𝑈)) ≤ ((♯‘𝑉) − 2) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈)))) |
| 37 | 14, 36 | mpid 44 |
. . . . 5
⊢ (((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈)) → ((♯‘(𝐺 NeighbVtx 𝑈)) = ((♯‘𝑉) − 1) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈))) |
| 38 | 37 | ex 412 |
. . . 4
⊢ ((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) → ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈) → ((♯‘(𝐺 NeighbVtx 𝑈)) = ((♯‘𝑉) − 1) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈)))) |
| 39 | 38 | com23 86 |
. . 3
⊢ ((¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉)) → ((♯‘(𝐺 NeighbVtx 𝑈)) = ((♯‘𝑉) − 1) → ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈)))) |
| 40 | 39 | ex 412 |
. 2
⊢ (¬
𝑀 ∈ (𝐺 NeighbVtx 𝑈) → ((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) → ((♯‘(𝐺 NeighbVtx 𝑈)) = ((♯‘𝑉) − 1) → ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈))))) |
| 41 | 2, 40 | pm2.61i 182 |
1
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) → ((♯‘(𝐺 NeighbVtx 𝑈)) = ((♯‘𝑉) − 1) → ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈)))) |