Proof of Theorem wlkv0
Step | Hyp | Ref
| Expression |
1 | | wlkcpr 27996 |
. . 3
⊢ (𝑊 ∈ (Walks‘𝐺) ↔ (1st
‘𝑊)(Walks‘𝐺)(2nd ‘𝑊)) |
2 | | eqid 2738 |
. . . . . 6
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
3 | 2 | wlkf 27981 |
. . . . 5
⊢
((1st ‘𝑊)(Walks‘𝐺)(2nd ‘𝑊) → (1st ‘𝑊) ∈ Word dom
(iEdg‘𝐺)) |
4 | | eqid 2738 |
. . . . . 6
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
5 | 4 | wlkp 27983 |
. . . . 5
⊢
((1st ‘𝑊)(Walks‘𝐺)(2nd ‘𝑊) → (2nd ‘𝑊):(0...(♯‘(1st
‘𝑊)))⟶(Vtx‘𝐺)) |
6 | 3, 5 | jca 512 |
. . . 4
⊢
((1st ‘𝑊)(Walks‘𝐺)(2nd ‘𝑊) → ((1st ‘𝑊) ∈ Word dom
(iEdg‘𝐺) ∧
(2nd ‘𝑊):(0...(♯‘(1st
‘𝑊)))⟶(Vtx‘𝐺))) |
7 | | feq3 6583 |
. . . . . . 7
⊢
((Vtx‘𝐺) =
∅ → ((2nd ‘𝑊):(0...(♯‘(1st
‘𝑊)))⟶(Vtx‘𝐺) ↔ (2nd ‘𝑊):(0...(♯‘(1st
‘𝑊)))⟶∅)) |
8 | | f00 6656 |
. . . . . . 7
⊢
((2nd ‘𝑊):(0...(♯‘(1st
‘𝑊)))⟶∅
↔ ((2nd ‘𝑊) = ∅ ∧
(0...(♯‘(1st ‘𝑊))) = ∅)) |
9 | 7, 8 | bitrdi 287 |
. . . . . 6
⊢
((Vtx‘𝐺) =
∅ → ((2nd ‘𝑊):(0...(♯‘(1st
‘𝑊)))⟶(Vtx‘𝐺) ↔ ((2nd ‘𝑊) = ∅ ∧
(0...(♯‘(1st ‘𝑊))) = ∅))) |
10 | | 0z 12330 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℤ |
11 | | nn0z 12343 |
. . . . . . . . . . . . 13
⊢
((♯‘(1st ‘𝑊)) ∈ ℕ0 →
(♯‘(1st ‘𝑊)) ∈ ℤ) |
12 | | fzn 13272 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℤ ∧ (♯‘(1st ‘𝑊)) ∈ ℤ) →
((♯‘(1st ‘𝑊)) < 0 ↔
(0...(♯‘(1st ‘𝑊))) = ∅)) |
13 | 10, 11, 12 | sylancr 587 |
. . . . . . . . . . . 12
⊢
((♯‘(1st ‘𝑊)) ∈ ℕ0 →
((♯‘(1st ‘𝑊)) < 0 ↔
(0...(♯‘(1st ‘𝑊))) = ∅)) |
14 | | nn0nlt0 12259 |
. . . . . . . . . . . . 13
⊢
((♯‘(1st ‘𝑊)) ∈ ℕ0 → ¬
(♯‘(1st ‘𝑊)) < 0) |
15 | 14 | pm2.21d 121 |
. . . . . . . . . . . 12
⊢
((♯‘(1st ‘𝑊)) ∈ ℕ0 →
((♯‘(1st ‘𝑊)) < 0 → (1st
‘𝑊) =
∅)) |
16 | 13, 15 | sylbird 259 |
. . . . . . . . . . 11
⊢
((♯‘(1st ‘𝑊)) ∈ ℕ0 →
((0...(♯‘(1st ‘𝑊))) = ∅ → (1st
‘𝑊) =
∅)) |
17 | 16 | com12 32 |
. . . . . . . . . 10
⊢
((0...(♯‘(1st ‘𝑊))) = ∅ →
((♯‘(1st ‘𝑊)) ∈ ℕ0 →
(1st ‘𝑊) =
∅)) |
18 | 17 | adantl 482 |
. . . . . . . . 9
⊢
(((2nd ‘𝑊) = ∅ ∧
(0...(♯‘(1st ‘𝑊))) = ∅) →
((♯‘(1st ‘𝑊)) ∈ ℕ0 →
(1st ‘𝑊) =
∅)) |
19 | | lencl 14236 |
. . . . . . . . 9
⊢
((1st ‘𝑊) ∈ Word dom (iEdg‘𝐺) →
(♯‘(1st ‘𝑊)) ∈
ℕ0) |
20 | 18, 19 | impel 506 |
. . . . . . . 8
⊢
((((2nd ‘𝑊) = ∅ ∧
(0...(♯‘(1st ‘𝑊))) = ∅) ∧ (1st
‘𝑊) ∈ Word dom
(iEdg‘𝐺)) →
(1st ‘𝑊) =
∅) |
21 | | simpll 764 |
. . . . . . . 8
⊢
((((2nd ‘𝑊) = ∅ ∧
(0...(♯‘(1st ‘𝑊))) = ∅) ∧ (1st
‘𝑊) ∈ Word dom
(iEdg‘𝐺)) →
(2nd ‘𝑊) =
∅) |
22 | 20, 21 | jca 512 |
. . . . . . 7
⊢
((((2nd ‘𝑊) = ∅ ∧
(0...(♯‘(1st ‘𝑊))) = ∅) ∧ (1st
‘𝑊) ∈ Word dom
(iEdg‘𝐺)) →
((1st ‘𝑊)
= ∅ ∧ (2nd ‘𝑊) = ∅)) |
23 | 22 | ex 413 |
. . . . . 6
⊢
(((2nd ‘𝑊) = ∅ ∧
(0...(♯‘(1st ‘𝑊))) = ∅) → ((1st
‘𝑊) ∈ Word dom
(iEdg‘𝐺) →
((1st ‘𝑊)
= ∅ ∧ (2nd ‘𝑊) = ∅))) |
24 | 9, 23 | syl6bi 252 |
. . . . 5
⊢
((Vtx‘𝐺) =
∅ → ((2nd ‘𝑊):(0...(♯‘(1st
‘𝑊)))⟶(Vtx‘𝐺) → ((1st ‘𝑊) ∈ Word dom
(iEdg‘𝐺) →
((1st ‘𝑊)
= ∅ ∧ (2nd ‘𝑊) = ∅)))) |
25 | 24 | impcomd 412 |
. . . 4
⊢
((Vtx‘𝐺) =
∅ → (((1st ‘𝑊) ∈ Word dom (iEdg‘𝐺) ∧ (2nd
‘𝑊):(0...(♯‘(1st
‘𝑊)))⟶(Vtx‘𝐺)) → ((1st ‘𝑊) = ∅ ∧
(2nd ‘𝑊) =
∅))) |
26 | 6, 25 | syl5 34 |
. . 3
⊢
((Vtx‘𝐺) =
∅ → ((1st ‘𝑊)(Walks‘𝐺)(2nd ‘𝑊) → ((1st ‘𝑊) = ∅ ∧
(2nd ‘𝑊) =
∅))) |
27 | 1, 26 | syl5bi 241 |
. 2
⊢
((Vtx‘𝐺) =
∅ → (𝑊 ∈
(Walks‘𝐺) →
((1st ‘𝑊)
= ∅ ∧ (2nd ‘𝑊) = ∅))) |
28 | 27 | imp 407 |
1
⊢
(((Vtx‘𝐺) =
∅ ∧ 𝑊 ∈
(Walks‘𝐺)) →
((1st ‘𝑊)
= ∅ ∧ (2nd ‘𝑊) = ∅)) |