Proof of Theorem wwlksnwwlksnon
Step | Hyp | Ref
| Expression |
1 | | wwlknbp2 26752 |
. . . . . 6
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1))) |
2 | 1 | adantl 482 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1))) |
3 | | wwlksnwwlksnon.v |
. . . . . . . . . . . 12
⊢ 𝑉 = (Vtx‘𝐺) |
4 | 3 | eqcomi 2631 |
. . . . . . . . . . 11
⊢
(Vtx‘𝐺) =
𝑉 |
5 | 4 | wrdeqi 13328 |
. . . . . . . . . 10
⊢ Word
(Vtx‘𝐺) = Word 𝑉 |
6 | 5 | eleq2i 2693 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word (Vtx‘𝐺) ↔ 𝑊 ∈ Word 𝑉) |
7 | 6 | biimpi 206 |
. . . . . . . 8
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → 𝑊 ∈ Word 𝑉) |
8 | 7 | adantr 481 |
. . . . . . 7
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) → 𝑊 ∈ Word 𝑉) |
9 | | nn0p1nn 11332 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ) |
10 | | lbfzo0 12507 |
. . . . . . . . . 10
⊢ (0 ∈
(0..^(𝑁 + 1)) ↔ (𝑁 + 1) ∈
ℕ) |
11 | 9, 10 | sylibr 224 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ 0 ∈ (0..^(𝑁 +
1))) |
12 | 11 | ad3antrrr 766 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1))) → 0 ∈ (0..^(𝑁 + 1))) |
13 | | oveq2 6658 |
. . . . . . . . . 10
⊢
((#‘𝑊) =
(𝑁 + 1) →
(0..^(#‘𝑊)) =
(0..^(𝑁 +
1))) |
14 | 13 | eleq2d 2687 |
. . . . . . . . 9
⊢
((#‘𝑊) =
(𝑁 + 1) → (0 ∈
(0..^(#‘𝑊)) ↔ 0
∈ (0..^(𝑁 +
1)))) |
15 | 14 | ad2antll 765 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1))) → (0 ∈ (0..^(#‘𝑊)) ↔ 0 ∈ (0..^(𝑁 + 1)))) |
16 | 12, 15 | mpbird 247 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1))) → 0 ∈ (0..^(#‘𝑊))) |
17 | | wrdsymbcl 13318 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 0 ∈ (0..^(#‘𝑊))) → (𝑊‘0) ∈ 𝑉) |
18 | 8, 16, 17 | syl2an2 875 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1))) → (𝑊‘0) ∈ 𝑉) |
19 | | fzonn0p1 12544 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈ (0..^(𝑁 + 1))) |
20 | 19 | ad3antrrr 766 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1))) → 𝑁 ∈ (0..^(𝑁 + 1))) |
21 | 13 | eleq2d 2687 |
. . . . . . . . 9
⊢
((#‘𝑊) =
(𝑁 + 1) → (𝑁 ∈ (0..^(#‘𝑊)) ↔ 𝑁 ∈ (0..^(𝑁 + 1)))) |
22 | 21 | ad2antll 765 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1))) → (𝑁 ∈ (0..^(#‘𝑊)) ↔ 𝑁 ∈ (0..^(𝑁 + 1)))) |
23 | 20, 22 | mpbird 247 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1))) → 𝑁 ∈ (0..^(#‘𝑊))) |
24 | | wrdsymbcl 13318 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(#‘𝑊))) → (𝑊‘𝑁) ∈ 𝑉) |
25 | 8, 23, 24 | syl2an2 875 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1))) → (𝑊‘𝑁) ∈ 𝑉) |
26 | | simplr 792 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1))) → 𝑊 ∈ (𝑁 WWalksN 𝐺)) |
27 | | eqidd 2623 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1))) → (𝑊‘0) = (𝑊‘0)) |
28 | | eqidd 2623 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1))) → (𝑊‘𝑁) = (𝑊‘𝑁)) |
29 | | eqeq2 2633 |
. . . . . . . 8
⊢ (𝑎 = (𝑊‘0) → ((𝑊‘0) = 𝑎 ↔ (𝑊‘0) = (𝑊‘0))) |
30 | 29 | 3anbi2d 1404 |
. . . . . . 7
⊢ (𝑎 = (𝑊‘0) → ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) ↔ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = (𝑊‘0) ∧ (𝑊‘𝑁) = 𝑏))) |
31 | | eqeq2 2633 |
. . . . . . . 8
⊢ (𝑏 = (𝑊‘𝑁) → ((𝑊‘𝑁) = 𝑏 ↔ (𝑊‘𝑁) = (𝑊‘𝑁))) |
32 | 31 | 3anbi3d 1405 |
. . . . . . 7
⊢ (𝑏 = (𝑊‘𝑁) → ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = (𝑊‘0) ∧ (𝑊‘𝑁) = 𝑏) ↔ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = (𝑊‘0) ∧ (𝑊‘𝑁) = (𝑊‘𝑁)))) |
33 | 30, 32 | rspc2ev 3324 |
. . . . . 6
⊢ (((𝑊‘0) ∈ 𝑉 ∧ (𝑊‘𝑁) ∈ 𝑉 ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = (𝑊‘0) ∧ (𝑊‘𝑁) = (𝑊‘𝑁))) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏)) |
34 | 18, 25, 26, 27, 28, 33 | syl113anc 1338 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1))) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏)) |
35 | 2, 34 | mpdan 702 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏)) |
36 | 35 | ex 450 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) → (𝑊 ∈ (𝑁 WWalksN 𝐺) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏))) |
37 | | simp1 1061 |
. . . . 5
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) → 𝑊 ∈ (𝑁 WWalksN 𝐺)) |
38 | 37 | a1i 11 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) → 𝑊 ∈ (𝑁 WWalksN 𝐺))) |
39 | 38 | rexlimdvva 3038 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) → (∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) → 𝑊 ∈ (𝑁 WWalksN 𝐺))) |
40 | 36, 39 | impbid 202 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) → (𝑊 ∈ (𝑁 WWalksN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏))) |
41 | 3 | wwlknon 26742 |
. . . . 5
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ↔ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏))) |
42 | 41 | bicomd 213 |
. . . 4
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) ↔ 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏))) |
43 | 42 | adantl 482 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) ↔ 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏))) |
44 | 43 | 2rexbidva 3056 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) → (∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏))) |
45 | 40, 44 | bitrd 268 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) → (𝑊 ∈ (𝑁 WWalksN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏))) |