Metamath Proof Explorer

Theorem wlklnwwlkln1

Description: The sequence of vertices in a walk of length N is a walk as word of length N in a pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018) (Revised by AV, 12-Apr-2021)

Ref Expression
Assertion wlklnwwlkln1 ( 𝐺 ∈ UPGraph → ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 𝑁 ) → 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 wlkcl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
2 1 adantr ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 𝑁 ) → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
3 wlkiswwlks1 ⊢ ( 𝐺 ∈ UPGraph → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 ∈ ( WWalks ‘ 𝐺 ) ) )
4 3 com12 ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ UPGraph → 𝑃 ∈ ( WWalks ‘ 𝐺 ) ) )
5 4 ad2antrl ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 𝑁 ) ) → ( 𝐺 ∈ UPGraph → 𝑃 ∈ ( WWalks ‘ 𝐺 ) ) )
6 5 imp ⊢ ( ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 𝑁 ) ) ∧ 𝐺 ∈ UPGraph ) → 𝑃 ∈ ( WWalks ‘ 𝐺 ) )
7 wlklenvp1 ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
8 7 ad2antrl ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 𝑁 ) ) → ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
9 oveq1 ⊢ ( ( ♯ ‘ 𝐹 ) = 𝑁 → ( ( ♯ ‘ 𝐹 ) + 1 ) = ( 𝑁 + 1 ) )
10 9 adantl ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 𝑁 ) → ( ( ♯ ‘ 𝐹 ) + 1 ) = ( 𝑁 + 1 ) )
11 10 adantl ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 𝑁 ) ) → ( ( ♯ ‘ 𝐹 ) + 1 ) = ( 𝑁 + 1 ) )
12 8 11 eqtrd ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 𝑁 ) ) → ( ♯ ‘ 𝑃 ) = ( 𝑁 + 1 ) )
13 12 adantr ⊢ ( ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 𝑁 ) ) ∧ 𝐺 ∈ UPGraph ) → ( ♯ ‘ 𝑃 ) = ( 𝑁 + 1 ) )
14 eleq1 ⊢ ( ( ♯ ‘ 𝐹 ) = 𝑁 → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ↔ 𝑁 ∈ ℕ0 ) )
15 iswwlksn ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = ( 𝑁 + 1 ) ) ) )
16 14 15 syl6bi ⊢ ( ( ♯ ‘ 𝐹 ) = 𝑁 → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = ( 𝑁 + 1 ) ) ) ) )
17 16 adantl ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 𝑁 ) → ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = ( 𝑁 + 1 ) ) ) ) )
18 17 impcom ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 𝑁 ) ) → ( 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = ( 𝑁 + 1 ) ) ) )
19 18 adantr ⊢ ( ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 𝑁 ) ) ∧ 𝐺 ∈ UPGraph ) → ( 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = ( 𝑁 + 1 ) ) ) )
20 6 13 19 mpbir2and ⊢ ( ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 𝑁 ) ) ∧ 𝐺 ∈ UPGraph ) → 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) )
21 20 ex ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 𝑁 ) ) → ( 𝐺 ∈ UPGraph → 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) ) )
22 2 21 mpancom ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 𝑁 ) → ( 𝐺 ∈ UPGraph → 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) ) )
23 22 com12 ⊢ ( 𝐺 ∈ UPGraph → ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 𝑁 ) → 𝑃 ∈ ( 𝑁 WWalksN 𝐺 ) ) )