| Step |
Hyp |
Ref |
Expression |
| 1 |
|
peano2nn0 |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 ) |
| 2 |
|
iswwlksn |
⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ↔ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ) ) |
| 3 |
1 2
|
syl |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ↔ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ) ) |
| 4 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
| 5 |
|
eqid |
⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 ) |
| 6 |
4 5
|
iswwlks |
⊢ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ↔ ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
| 7 |
|
simp1 |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ) |
| 8 |
|
nn0p1nn |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ ) |
| 9 |
8
|
3ad2ant3 |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ∈ ℕ ) |
| 10 |
1
|
nn0red |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℝ ) |
| 11 |
10
|
lep1d |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 1 ) + 1 ) ) |
| 12 |
11
|
3ad2ant3 |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 1 ) + 1 ) ) |
| 13 |
|
breq2 |
⊢ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝑊 ) ↔ ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 1 ) + 1 ) ) ) |
| 14 |
13
|
3ad2ant2 |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝑊 ) ↔ ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 1 ) + 1 ) ) ) |
| 15 |
12 14
|
mpbird |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝑊 ) ) |
| 16 |
|
pfxn0 |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ℕ ∧ ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ≠ ∅ ) |
| 17 |
7 9 15 16
|
syl3anc |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ≠ ∅ ) |
| 18 |
17
|
3exp |
⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 𝑁 ∈ ℕ0 → ( 𝑊 prefix ( 𝑁 + 1 ) ) ≠ ∅ ) ) ) |
| 19 |
18
|
3ad2ant2 |
⊢ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 𝑁 ∈ ℕ0 → ( 𝑊 prefix ( 𝑁 + 1 ) ) ≠ ∅ ) ) ) |
| 20 |
19
|
imp |
⊢ ( ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( 𝑁 ∈ ℕ0 → ( 𝑊 prefix ( 𝑁 + 1 ) ) ≠ ∅ ) ) |
| 21 |
20
|
impcom |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ≠ ∅ ) |
| 22 |
|
pfxcl |
⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ Word ( Vtx ‘ 𝐺 ) ) |
| 23 |
22
|
3ad2ant2 |
⊢ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ Word ( Vtx ‘ 𝐺 ) ) |
| 24 |
23
|
adantr |
⊢ ( ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ Word ( Vtx ‘ 𝐺 ) ) |
| 25 |
24
|
adantl |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ Word ( Vtx ‘ 𝐺 ) ) |
| 26 |
|
oveq1 |
⊢ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) ) |
| 27 |
1
|
nn0cnd |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℂ ) |
| 28 |
|
1cnd |
⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℂ ) |
| 29 |
27 28
|
pncand |
⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 + 1 ) + 1 ) − 1 ) = ( 𝑁 + 1 ) ) |
| 30 |
26 29
|
sylan9eq |
⊢ ( ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = ( 𝑁 + 1 ) ) |
| 31 |
30
|
oveq2d |
⊢ ( ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 0 ..^ ( 𝑁 + 1 ) ) ) |
| 32 |
31
|
raleqdv |
⊢ ( ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
| 33 |
32
|
adantl |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
| 34 |
|
nn0z |
⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ ) |
| 35 |
|
nn0z |
⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℤ ) |
| 36 |
1 35
|
syl |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℤ ) |
| 37 |
|
nn0re |
⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ ) |
| 38 |
37
|
lep1d |
⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ≤ ( 𝑁 + 1 ) ) |
| 39 |
34 36 38
|
3jca |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ∈ ℤ ∧ ( 𝑁 + 1 ) ∈ ℤ ∧ 𝑁 ≤ ( 𝑁 + 1 ) ) ) |
| 40 |
39
|
ad2antll |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑁 ∈ ℤ ∧ ( 𝑁 + 1 ) ∈ ℤ ∧ 𝑁 ≤ ( 𝑁 + 1 ) ) ) |
| 41 |
|
eluz2 |
⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ ( 𝑁 + 1 ) ∈ ℤ ∧ 𝑁 ≤ ( 𝑁 + 1 ) ) ) |
| 42 |
40 41
|
sylibr |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) |
| 43 |
|
fzoss2 |
⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( 𝑁 + 1 ) ) ) |
| 44 |
42 43
|
syl |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( 𝑁 + 1 ) ) ) |
| 45 |
|
ssralv |
⊢ ( ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( 𝑁 + 1 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
| 46 |
44 45
|
syl |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
| 47 |
|
simpll |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ) |
| 48 |
|
nn0fz0 |
⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 ↔ ( 𝑁 + 1 ) ∈ ( 0 ... ( 𝑁 + 1 ) ) ) |
| 49 |
1 48
|
sylib |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ( 0 ... ( 𝑁 + 1 ) ) ) |
| 50 |
49
|
ad2antll |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑁 + 1 ) ∈ ( 0 ... ( 𝑁 + 1 ) ) ) |
| 51 |
|
fzelp1 |
⊢ ( ( 𝑁 + 1 ) ∈ ( 0 ... ( 𝑁 + 1 ) ) → ( 𝑁 + 1 ) ∈ ( 0 ... ( ( 𝑁 + 1 ) + 1 ) ) ) |
| 52 |
50 51
|
syl |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑁 + 1 ) ∈ ( 0 ... ( ( 𝑁 + 1 ) + 1 ) ) ) |
| 53 |
|
oveq2 |
⊢ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 0 ... ( ♯ ‘ 𝑊 ) ) = ( 0 ... ( ( 𝑁 + 1 ) + 1 ) ) ) |
| 54 |
53
|
eleq2d |
⊢ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑁 + 1 ) ∈ ( 0 ... ( ( 𝑁 + 1 ) + 1 ) ) ) ) |
| 55 |
54
|
adantr |
⊢ ( ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑁 + 1 ) ∈ ( 0 ... ( ( 𝑁 + 1 ) + 1 ) ) ) ) |
| 56 |
55
|
adantl |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑁 + 1 ) ∈ ( 0 ... ( ( 𝑁 + 1 ) + 1 ) ) ) ) |
| 57 |
52 56
|
mpbird |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) |
| 58 |
57
|
adantr |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) |
| 59 |
|
fzossfzop1 |
⊢ ( 𝑁 ∈ ℕ0 → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( 𝑁 + 1 ) ) ) |
| 60 |
59
|
sseld |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) |
| 61 |
60
|
ad2antll |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) |
| 62 |
61
|
imp |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) |
| 63 |
|
pfxfv |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) = ( 𝑊 ‘ 𝑖 ) ) |
| 64 |
47 58 62 63
|
syl3anc |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) = ( 𝑊 ‘ 𝑖 ) ) |
| 65 |
64
|
eqcomd |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑊 ‘ 𝑖 ) = ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) ) |
| 66 |
|
fzofzp1 |
⊢ ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑁 ) ) |
| 67 |
66
|
adantl |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑁 ) ) |
| 68 |
|
fzval3 |
⊢ ( 𝑁 ∈ ℤ → ( 0 ... 𝑁 ) = ( 0 ..^ ( 𝑁 + 1 ) ) ) |
| 69 |
68
|
eqcomd |
⊢ ( 𝑁 ∈ ℤ → ( 0 ..^ ( 𝑁 + 1 ) ) = ( 0 ... 𝑁 ) ) |
| 70 |
34 69
|
syl |
⊢ ( 𝑁 ∈ ℕ0 → ( 0 ..^ ( 𝑁 + 1 ) ) = ( 0 ... 𝑁 ) ) |
| 71 |
70
|
eleq2d |
⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑖 + 1 ) ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ↔ ( 𝑖 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) |
| 72 |
71
|
ad2antll |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( ( 𝑖 + 1 ) ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ↔ ( 𝑖 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) |
| 73 |
72
|
adantr |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑖 + 1 ) ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ↔ ( 𝑖 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) |
| 74 |
67 73
|
mpbird |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) |
| 75 |
|
pfxfv |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑖 + 1 ) ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) = ( 𝑊 ‘ ( 𝑖 + 1 ) ) ) |
| 76 |
47 58 74 75
|
syl3anc |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) = ( 𝑊 ‘ ( 𝑖 + 1 ) ) ) |
| 77 |
76
|
eqcomd |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑊 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) ) |
| 78 |
65 77
|
preq12d |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } = { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ) |
| 79 |
78
|
eleq1d |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
| 80 |
79
|
biimpd |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
| 81 |
80
|
ralimdva |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
| 82 |
46 81
|
syld |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
| 83 |
33 82
|
sylbid |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
| 84 |
83
|
imp |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) |
| 85 |
|
nn0cn |
⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ ) |
| 86 |
85 28
|
pncand |
⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 ) |
| 87 |
86
|
oveq2d |
⊢ ( 𝑁 ∈ ℕ0 → ( 0 ..^ ( ( 𝑁 + 1 ) − 1 ) ) = ( 0 ..^ 𝑁 ) ) |
| 88 |
87
|
ad2antll |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( 0 ..^ ( ( 𝑁 + 1 ) − 1 ) ) = ( 0 ..^ 𝑁 ) ) |
| 89 |
88
|
adantr |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( 0 ..^ ( ( 𝑁 + 1 ) − 1 ) ) = ( 0 ..^ 𝑁 ) ) |
| 90 |
89
|
raleqdv |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( 𝑁 + 1 ) − 1 ) ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
| 91 |
84 90
|
mpbird |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( 𝑁 + 1 ) − 1 ) ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) |
| 92 |
|
pfxlen |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) ) |
| 93 |
57 92
|
syldan |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) ) |
| 94 |
93
|
oveq1d |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) − 1 ) = ( ( 𝑁 + 1 ) − 1 ) ) |
| 95 |
94
|
oveq2d |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) − 1 ) ) = ( 0 ..^ ( ( 𝑁 + 1 ) − 1 ) ) ) |
| 96 |
95
|
raleqdv |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) − 1 ) ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ( 𝑁 + 1 ) − 1 ) ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
| 97 |
96
|
adantr |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) − 1 ) ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ( 𝑁 + 1 ) − 1 ) ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
| 98 |
91 97
|
mpbird |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) − 1 ) ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) |
| 99 |
98
|
exp31 |
⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) − 1 ) ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) |
| 100 |
99
|
com23 |
⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) − 1 ) ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) |
| 101 |
100
|
imp |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) − 1 ) ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
| 102 |
101
|
3adant1 |
⊢ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) − 1 ) ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
| 103 |
102
|
expdimp |
⊢ ( ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( 𝑁 ∈ ℕ0 → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) − 1 ) ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
| 104 |
103
|
impcom |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) − 1 ) ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) |
| 105 |
4 5
|
iswwlks |
⊢ ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( WWalks ‘ 𝐺 ) ↔ ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ≠ ∅ ∧ ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) − 1 ) ) { ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ 𝑖 ) , ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
| 106 |
21 25 104 105
|
syl3anbrc |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( WWalks ‘ 𝐺 ) ) |
| 107 |
|
peano2nn0 |
⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( ( 𝑁 + 1 ) + 1 ) ∈ ℕ0 ) |
| 108 |
1 107
|
syl |
⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) + 1 ) ∈ ℕ0 ) |
| 109 |
|
elfz2nn0 |
⊢ ( ( 𝑁 + 1 ) ∈ ( 0 ... ( ( 𝑁 + 1 ) + 1 ) ) ↔ ( ( 𝑁 + 1 ) ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) + 1 ) ∈ ℕ0 ∧ ( 𝑁 + 1 ) ≤ ( ( 𝑁 + 1 ) + 1 ) ) ) |
| 110 |
1 108 11 109
|
syl3anbrc |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ( 0 ... ( ( 𝑁 + 1 ) + 1 ) ) ) |
| 111 |
110
|
adantl |
⊢ ( ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ∈ ( 0 ... ( ( 𝑁 + 1 ) + 1 ) ) ) |
| 112 |
111 55
|
mpbird |
⊢ ( ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) |
| 113 |
112
|
anim2i |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ) |
| 114 |
113
|
exp32 |
⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ) ) ) |
| 115 |
114
|
3ad2ant2 |
⊢ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) → ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ) ) ) |
| 116 |
115
|
imp |
⊢ ( ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ) ) |
| 117 |
116
|
impcom |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ) |
| 118 |
117 92
|
syl |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ) → ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) ) |
| 119 |
|
iswwlksn |
⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) ) ) ) |
| 120 |
119
|
adantr |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ) → ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ ( 𝑊 prefix ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) ) ) ) |
| 121 |
106 118 120
|
mpbir2and |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ) |
| 122 |
121
|
expcom |
⊢ ( ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( 𝑁 ∈ ℕ0 → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ) ) |
| 123 |
6 122
|
sylanb |
⊢ ( ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( 𝑁 ∈ ℕ0 → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ) ) |
| 124 |
123
|
com12 |
⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( ( 𝑁 + 1 ) + 1 ) ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ) ) |
| 125 |
3 124
|
sylbid |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( 𝑊 prefix ( 𝑁 + 1 ) ) ∈ ( 𝑁 WWalksN 𝐺 ) ) ) |