Metamath Proof Explorer

Theorem wwlksnwwlksnon

Description: A walk of fixed length is a walk of fixed length between two vertices. (Contributed by Alexander van der Vekens, 21-Feb-2018) (Revised by AV, 12-May-2021) (Revised by AV, 13-Mar-2022)

Ref Expression
Hypothesis wwlksnwwlksnon.v ⊢ V = Vtx ⁡ G
Assertion wwlksnwwlksnon ⊢ W ∈ N WWalksN G ↔ ∃ a ∈ V ∃ b ∈ V W ∈ a N WWalksNOn G b

Proof

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