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 ⊢ G ∈ UPGraph → F Walks ⁡ G P ∧ F = N → P ∈ N WWalksN G

Proof

Step Hyp Ref Expression
1 wlkcl ⊢ F Walks ⁡ G P → F ∈ ℕ 0
2 1 adantr ⊢ F Walks ⁡ G P ∧ F = N → F ∈ ℕ 0
3 wlkiswwlks1 ⊢ G ∈ UPGraph → F Walks ⁡ G P → P ∈ WWalks ⁡ G
4 3 com12 ⊢ F Walks ⁡ G P → G ∈ UPGraph → P ∈ WWalks ⁡ G
5 4 ad2antrl ⊢ F ∈ ℕ 0 ∧ F Walks ⁡ G P ∧ F = N → G ∈ UPGraph → P ∈ WWalks ⁡ G
6 5 imp ⊢ F ∈ ℕ 0 ∧ F Walks ⁡ G P ∧ F = N ∧ G ∈ UPGraph → P ∈ WWalks ⁡ G
7 wlklenvp1 ⊢ F Walks ⁡ G P → P = F + 1
8 7 ad2antrl ⊢ F ∈ ℕ 0 ∧ F Walks ⁡ G P ∧ F = N → P = F + 1
9 oveq1 ⊢ F = N → F + 1 = N + 1
10 9 adantl ⊢ F Walks ⁡ G P ∧ F = N → F + 1 = N + 1
11 10 adantl ⊢ F ∈ ℕ 0 ∧ F Walks ⁡ G P ∧ F = N → F + 1 = N + 1
12 8 11 eqtrd ⊢ F ∈ ℕ 0 ∧ F Walks ⁡ G P ∧ F = N → P = N + 1
13 12 adantr ⊢ F ∈ ℕ 0 ∧ F Walks ⁡ G P ∧ F = N ∧ G ∈ UPGraph → P = N + 1
14 eleq1 ⊢ F = N → F ∈ ℕ 0 ↔ N ∈ ℕ 0
15 iswwlksn ⊢ N ∈ ℕ 0 → P ∈ N WWalksN G ↔ P ∈ WWalks ⁡ G ∧ P = N + 1
16 14 15 biimtrdi ⊢ F = N → F ∈ ℕ 0 → P ∈ N WWalksN G ↔ P ∈ WWalks ⁡ G ∧ P = N + 1
17 16 adantl ⊢ F Walks ⁡ G P ∧ F = N → F ∈ ℕ 0 → P ∈ N WWalksN G ↔ P ∈ WWalks ⁡ G ∧ P = N + 1
18 17 impcom ⊢ F ∈ ℕ 0 ∧ F Walks ⁡ G P ∧ F = N → P ∈ N WWalksN G ↔ P ∈ WWalks ⁡ G ∧ P = N + 1
19 18 adantr ⊢ F ∈ ℕ 0 ∧ F Walks ⁡ G P ∧ F = N ∧ G ∈ UPGraph → P ∈ N WWalksN G ↔ P ∈ WWalks ⁡ G ∧ P = N + 1
20 6 13 19 mpbir2and ⊢ F ∈ ℕ 0 ∧ F Walks ⁡ G P ∧ F = N ∧ G ∈ UPGraph → P ∈ N WWalksN G
21 20 ex ⊢ F ∈ ℕ 0 ∧ F Walks ⁡ G P ∧ F = N → G ∈ UPGraph → P ∈ N WWalksN G
22 2 21 mpancom ⊢ F Walks ⁡ G P ∧ F = N → G ∈ UPGraph → P ∈ N WWalksN G
23 22 com12 ⊢ G ∈ UPGraph → F Walks ⁡ G P ∧ F = N → P ∈ N WWalksN G