Proof of Theorem 1wlkv0
Step | Hyp | Ref
| Expression |
1 | | 1wlkcpr 40833 |
. . 3
⊢ (𝑊 ∈ (1Walks‘𝐺) ↔ (1st
‘𝑊)(1Walks‘𝐺)(2nd ‘𝑊)) |
2 | | eqid 2610 |
. . . . 5
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
3 | | eqid 2610 |
. . . . 5
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
4 | 2, 3 | 2m1wlk 40818 |
. . . 4
⊢
((1st ‘𝑊)(1Walks‘𝐺)(2nd ‘𝑊) → ((1st ‘𝑊) ∈ Word dom
(iEdg‘𝐺) ∧
(2nd ‘𝑊):(0...(#‘(1st ‘𝑊)))⟶(Vtx‘𝐺))) |
5 | | feq3 5941 |
. . . . . . . 8
⊢
((Vtx‘𝐺) =
∅ → ((2nd ‘𝑊):(0...(#‘(1st ‘𝑊)))⟶(Vtx‘𝐺) ↔ (2nd
‘𝑊):(0...(#‘(1st ‘𝑊)))⟶∅)) |
6 | | f00 6000 |
. . . . . . . 8
⊢
((2nd ‘𝑊):(0...(#‘(1st ‘𝑊)))⟶∅ ↔
((2nd ‘𝑊)
= ∅ ∧ (0...(#‘(1st ‘𝑊))) = ∅)) |
7 | 5, 6 | syl6bb 275 |
. . . . . . 7
⊢
((Vtx‘𝐺) =
∅ → ((2nd ‘𝑊):(0...(#‘(1st ‘𝑊)))⟶(Vtx‘𝐺) ↔ ((2nd
‘𝑊) = ∅ ∧
(0...(#‘(1st ‘𝑊))) = ∅))) |
8 | | 0z 11265 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℤ |
9 | | nn0z 11277 |
. . . . . . . . . . . . . 14
⊢
((#‘(1st ‘𝑊)) ∈ ℕ0 →
(#‘(1st ‘𝑊)) ∈ ℤ) |
10 | | fzn 12228 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℤ ∧ (#‘(1st ‘𝑊)) ∈ ℤ) →
((#‘(1st ‘𝑊)) < 0 ↔
(0...(#‘(1st ‘𝑊))) = ∅)) |
11 | 8, 9, 10 | sylancr 694 |
. . . . . . . . . . . . 13
⊢
((#‘(1st ‘𝑊)) ∈ ℕ0 →
((#‘(1st ‘𝑊)) < 0 ↔
(0...(#‘(1st ‘𝑊))) = ∅)) |
12 | | nn0nlt0 11196 |
. . . . . . . . . . . . . 14
⊢
((#‘(1st ‘𝑊)) ∈ ℕ0 → ¬
(#‘(1st ‘𝑊)) < 0) |
13 | 12 | pm2.21d 117 |
. . . . . . . . . . . . 13
⊢
((#‘(1st ‘𝑊)) ∈ ℕ0 →
((#‘(1st ‘𝑊)) < 0 → (1st
‘𝑊) =
∅)) |
14 | 11, 13 | sylbird 249 |
. . . . . . . . . . . 12
⊢
((#‘(1st ‘𝑊)) ∈ ℕ0 →
((0...(#‘(1st ‘𝑊))) = ∅ → (1st
‘𝑊) =
∅)) |
15 | 14 | com12 32 |
. . . . . . . . . . 11
⊢
((0...(#‘(1st ‘𝑊))) = ∅ →
((#‘(1st ‘𝑊)) ∈ ℕ0 →
(1st ‘𝑊) =
∅)) |
16 | 15 | adantl 481 |
. . . . . . . . . 10
⊢
(((2nd ‘𝑊) = ∅ ∧
(0...(#‘(1st ‘𝑊))) = ∅) →
((#‘(1st ‘𝑊)) ∈ ℕ0 →
(1st ‘𝑊) =
∅)) |
17 | | lencl 13179 |
. . . . . . . . . 10
⊢
((1st ‘𝑊) ∈ Word dom (iEdg‘𝐺) →
(#‘(1st ‘𝑊)) ∈
ℕ0) |
18 | 16, 17 | impel 484 |
. . . . . . . . 9
⊢
((((2nd ‘𝑊) = ∅ ∧
(0...(#‘(1st ‘𝑊))) = ∅) ∧ (1st
‘𝑊) ∈ Word dom
(iEdg‘𝐺)) →
(1st ‘𝑊) =
∅) |
19 | | simpll 786 |
. . . . . . . . 9
⊢
((((2nd ‘𝑊) = ∅ ∧
(0...(#‘(1st ‘𝑊))) = ∅) ∧ (1st
‘𝑊) ∈ Word dom
(iEdg‘𝐺)) →
(2nd ‘𝑊) =
∅) |
20 | 18, 19 | jca 553 |
. . . . . . . 8
⊢
((((2nd ‘𝑊) = ∅ ∧
(0...(#‘(1st ‘𝑊))) = ∅) ∧ (1st
‘𝑊) ∈ Word dom
(iEdg‘𝐺)) →
((1st ‘𝑊)
= ∅ ∧ (2nd ‘𝑊) = ∅)) |
21 | 20 | ex 449 |
. . . . . . 7
⊢
(((2nd ‘𝑊) = ∅ ∧
(0...(#‘(1st ‘𝑊))) = ∅) → ((1st
‘𝑊) ∈ Word dom
(iEdg‘𝐺) →
((1st ‘𝑊)
= ∅ ∧ (2nd ‘𝑊) = ∅))) |
22 | 7, 21 | syl6bi 242 |
. . . . . 6
⊢
((Vtx‘𝐺) =
∅ → ((2nd ‘𝑊):(0...(#‘(1st ‘𝑊)))⟶(Vtx‘𝐺) → ((1st
‘𝑊) ∈ Word dom
(iEdg‘𝐺) →
((1st ‘𝑊)
= ∅ ∧ (2nd ‘𝑊) = ∅)))) |
23 | 22 | com23 84 |
. . . . 5
⊢
((Vtx‘𝐺) =
∅ → ((1st ‘𝑊) ∈ Word dom (iEdg‘𝐺) → ((2nd
‘𝑊):(0...(#‘(1st ‘𝑊)))⟶(Vtx‘𝐺) → ((1st
‘𝑊) = ∅ ∧
(2nd ‘𝑊) =
∅)))) |
24 | 23 | impd 446 |
. . . 4
⊢
((Vtx‘𝐺) =
∅ → (((1st ‘𝑊) ∈ Word dom (iEdg‘𝐺) ∧ (2nd
‘𝑊):(0...(#‘(1st ‘𝑊)))⟶(Vtx‘𝐺)) → ((1st
‘𝑊) = ∅ ∧
(2nd ‘𝑊) =
∅))) |
25 | 4, 24 | syl5 33 |
. . 3
⊢
((Vtx‘𝐺) =
∅ → ((1st ‘𝑊)(1Walks‘𝐺)(2nd ‘𝑊) → ((1st ‘𝑊) = ∅ ∧
(2nd ‘𝑊) =
∅))) |
26 | 1, 25 | syl5bi 231 |
. 2
⊢
((Vtx‘𝐺) =
∅ → (𝑊 ∈
(1Walks‘𝐺) →
((1st ‘𝑊)
= ∅ ∧ (2nd ‘𝑊) = ∅))) |
27 | 26 | imp 444 |
1
⊢
(((Vtx‘𝐺) =
∅ ∧ 𝑊 ∈
(1Walks‘𝐺)) →
((1st ‘𝑊)
= ∅ ∧ (2nd ‘𝑊) = ∅)) |