Step |
Hyp |
Ref |
Expression |
1 |
|
wwlkbp.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
df-wwlksn |
⊢ WWalksN = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ { 𝑤 ∈ ( WWalks ‘ 𝑔 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑛 + 1 ) } ) |
3 |
2
|
elmpocl |
⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ) |
4 |
|
simpl |
⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ) → ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ) |
5 |
4
|
ancomd |
⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ) → ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ) ) |
6 |
|
iswwlksn |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ) |
7 |
6
|
adantr |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) ) ) |
8 |
1
|
wwlkbp |
⊢ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) → ( 𝐺 ∈ V ∧ 𝑊 ∈ Word 𝑉 ) ) |
9 |
8
|
simprd |
⊢ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) → 𝑊 ∈ Word 𝑉 ) |
10 |
9
|
adantr |
⊢ ( ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → 𝑊 ∈ Word 𝑉 ) |
11 |
7 10
|
syl6bi |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → 𝑊 ∈ Word 𝑉 ) ) |
12 |
11
|
imp |
⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ) → 𝑊 ∈ Word 𝑉 ) |
13 |
|
df-3an |
⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉 ) ↔ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑊 ∈ Word 𝑉 ) ) |
14 |
5 12 13
|
sylanbrc |
⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ) → ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉 ) ) |
15 |
3 14
|
mpancom |
⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉 ) ) |