Step |
Hyp |
Ref |
Expression |
1 |
|
wwlksnwwlksnon.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
wwlknbp1 |
⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) |
3 |
1
|
eqcomi |
⊢ ( Vtx ‘ 𝐺 ) = 𝑉 |
4 |
3
|
wrdeqi |
⊢ Word ( Vtx ‘ 𝐺 ) = Word 𝑉 |
5 |
4
|
eleq2i |
⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ↔ 𝑊 ∈ Word 𝑉 ) |
6 |
5
|
biimpi |
⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → 𝑊 ∈ Word 𝑉 ) |
7 |
6
|
3ad2ant2 |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → 𝑊 ∈ Word 𝑉 ) |
8 |
|
nn0p1nn |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ ) |
9 |
|
lbfzo0 |
⊢ ( 0 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ↔ ( 𝑁 + 1 ) ∈ ℕ ) |
10 |
8 9
|
sylibr |
⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) |
11 |
10
|
3ad2ant1 |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → 0 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) |
12 |
|
oveq2 |
⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ..^ ( 𝑁 + 1 ) ) ) |
13 |
12
|
eleq2d |
⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ 0 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) |
14 |
13
|
3ad2ant3 |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ 0 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) |
15 |
11 14
|
mpbird |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) |
16 |
15
|
adantl |
⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) |
17 |
|
wrdsymbcl |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 ) |
18 |
7 16 17
|
syl2an2 |
⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 ) |
19 |
|
fzonn0p1 |
⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) |
20 |
19
|
3ad2ant1 |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) |
21 |
12
|
eleq2d |
⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) |
22 |
21
|
3ad2ant3 |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) |
23 |
20 22
|
mpbird |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) |
24 |
|
wrdsymbcl |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ 𝑁 ) ∈ 𝑉 ) |
25 |
7 23 24
|
syl2anc |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( 𝑊 ‘ 𝑁 ) ∈ 𝑉 ) |
26 |
25
|
adantl |
⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) → ( 𝑊 ‘ 𝑁 ) ∈ 𝑉 ) |
27 |
|
simpl |
⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) → 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ) |
28 |
|
eqidd |
⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) → ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ) |
29 |
|
eqidd |
⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) → ( 𝑊 ‘ 𝑁 ) = ( 𝑊 ‘ 𝑁 ) ) |
30 |
|
eqeq2 |
⊢ ( 𝑎 = ( 𝑊 ‘ 0 ) → ( ( 𝑊 ‘ 0 ) = 𝑎 ↔ ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ) ) |
31 |
30
|
3anbi2d |
⊢ ( 𝑎 = ( 𝑊 ‘ 0 ) → ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) ↔ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) ) ) |
32 |
|
eqeq2 |
⊢ ( 𝑏 = ( 𝑊 ‘ 𝑁 ) → ( ( 𝑊 ‘ 𝑁 ) = 𝑏 ↔ ( 𝑊 ‘ 𝑁 ) = ( 𝑊 ‘ 𝑁 ) ) ) |
33 |
32
|
3anbi3d |
⊢ ( 𝑏 = ( 𝑊 ‘ 𝑁 ) → ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) ↔ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( 𝑊 ‘ 𝑁 ) = ( 𝑊 ‘ 𝑁 ) ) ) ) |
34 |
31 33
|
rspc2ev |
⊢ ( ( ( 𝑊 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑊 ‘ 𝑁 ) ∈ 𝑉 ∧ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ∧ ( 𝑊 ‘ 𝑁 ) = ( 𝑊 ‘ 𝑁 ) ) ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) ) |
35 |
18 26 27 28 29 34
|
syl113anc |
⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) ) |
36 |
2 35
|
mpdan |
⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) ) |
37 |
|
simp1 |
⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) → 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ) |
38 |
37
|
a1i |
⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) → 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ) ) |
39 |
38
|
rexlimivv |
⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) → 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ) |
40 |
36 39
|
impbii |
⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) ) |
41 |
|
wwlknon |
⊢ ( 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ↔ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) ) |
42 |
41
|
bicomi |
⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) ↔ 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ) |
43 |
42
|
2rexbii |
⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ) |
44 |
40 43
|
bitri |
⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ) |