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 e. ( N WWalksN G ) <-> E. a e. V E. b e. V W e. ( a ( N WWalksNOn G ) b ) )

Proof

Step Hyp Ref Expression
1 wwlksnwwlksnon.v 
 |-  V = ( Vtx ` G )
2 wwlknbp1 
 |-  ( W e. ( N WWalksN G ) -> ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) )
3 1 eqcomi 
 |-  ( Vtx ` G ) = V
4 3 wrdeqi 
 |-  Word ( Vtx ` G ) = Word V
5 4 eleq2i 
 |-  ( W e. Word ( Vtx ` G ) <-> W e. Word V )
6 5 biimpi 
 |-  ( W e. Word ( Vtx ` G ) -> W e. Word V )
7 6 3ad2ant2 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> W e. Word V )
8 nn0p1nn 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN )
9 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( N + 1 ) ) <-> ( N + 1 ) e. NN )
10 8 9 sylibr 
 |-  ( N e. NN0 -> 0 e. ( 0 ..^ ( N + 1 ) ) )
11 10 3ad2ant1 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> 0 e. ( 0 ..^ ( N + 1 ) ) )
12 oveq2 
 |-  ( ( # ` W ) = ( N + 1 ) -> ( 0 ..^ ( # ` W ) ) = ( 0 ..^ ( N + 1 ) ) )
13 12 eleq2d 
 |-  ( ( # ` W ) = ( N + 1 ) -> ( 0 e. ( 0 ..^ ( # ` W ) ) <-> 0 e. ( 0 ..^ ( N + 1 ) ) ) )
14 13 3ad2ant3 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( 0 e. ( 0 ..^ ( # ` W ) ) <-> 0 e. ( 0 ..^ ( N + 1 ) ) ) )
15 11 14 mpbird 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> 0 e. ( 0 ..^ ( # ` W ) ) )
16 15 adantl 
 |-  ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) -> 0 e. ( 0 ..^ ( # ` W ) ) )
17 wrdsymbcl 
 |-  ( ( W e. Word V /\ 0 e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` 0 ) e. V )
18 7 16 17 syl2an2 
 |-  ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) -> ( W ` 0 ) e. V )
19 fzonn0p1 
 |-  ( N e. NN0 -> N e. ( 0 ..^ ( N + 1 ) ) )
20 19 3ad2ant1 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> N e. ( 0 ..^ ( N + 1 ) ) )
21 12 eleq2d 
 |-  ( ( # ` W ) = ( N + 1 ) -> ( N e. ( 0 ..^ ( # ` W ) ) <-> N e. ( 0 ..^ ( N + 1 ) ) ) )
22 21 3ad2ant3 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( N e. ( 0 ..^ ( # ` W ) ) <-> N e. ( 0 ..^ ( N + 1 ) ) ) )
23 20 22 mpbird 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> N e. ( 0 ..^ ( # ` W ) ) )
24 wrdsymbcl 
 |-  ( ( W e. Word V /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` N ) e. V )
25 7 23 24 syl2anc 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( W ` N ) e. V )
26 25 adantl 
 |-  ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) -> ( W ` N ) e. V )
27 simpl 
 |-  ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) -> W e. ( N WWalksN G ) )
28 eqidd 
 |-  ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) -> ( W ` 0 ) = ( W ` 0 ) )
29 eqidd 
 |-  ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. 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 e. ( N WWalksN G ) /\ ( W ` 0 ) = a /\ ( W ` N ) = b ) <-> ( W e. ( 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 e. ( N WWalksN G ) /\ ( W ` 0 ) = ( W ` 0 ) /\ ( W ` N ) = b ) <-> ( W e. ( N WWalksN G ) /\ ( W ` 0 ) = ( W ` 0 ) /\ ( W ` N ) = ( W ` N ) ) ) )
34 31 33 rspc2ev 
 |-  ( ( ( W ` 0 ) e. V /\ ( W ` N ) e. V /\ ( W e. ( N WWalksN G ) /\ ( W ` 0 ) = ( W ` 0 ) /\ ( W ` N ) = ( W ` N ) ) ) -> E. a e. V E. b e. V ( W e. ( N WWalksN G ) /\ ( W ` 0 ) = a /\ ( W ` N ) = b ) )
35 18 26 27 28 29 34 syl113anc 
 |-  ( ( W e. ( N WWalksN G ) /\ ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) -> E. a e. V E. b e. V ( W e. ( N WWalksN G ) /\ ( W ` 0 ) = a /\ ( W ` N ) = b ) )
36 2 35 mpdan 
 |-  ( W e. ( N WWalksN G ) -> E. a e. V E. b e. V ( W e. ( N WWalksN G ) /\ ( W ` 0 ) = a /\ ( W ` N ) = b ) )
37 simp1 
 |-  ( ( W e. ( N WWalksN G ) /\ ( W ` 0 ) = a /\ ( W ` N ) = b ) -> W e. ( N WWalksN G ) )
38 37 a1i 
 |-  ( ( a e. V /\ b e. V ) -> ( ( W e. ( N WWalksN G ) /\ ( W ` 0 ) = a /\ ( W ` N ) = b ) -> W e. ( N WWalksN G ) ) )
39 38 rexlimivv 
 |-  ( E. a e. V E. b e. V ( W e. ( N WWalksN G ) /\ ( W ` 0 ) = a /\ ( W ` N ) = b ) -> W e. ( N WWalksN G ) )
40 36 39 impbii 
 |-  ( W e. ( N WWalksN G ) <-> E. a e. V E. b e. V ( W e. ( N WWalksN G ) /\ ( W ` 0 ) = a /\ ( W ` N ) = b ) )
41 wwlknon 
 |-  ( W e. ( a ( N WWalksNOn G ) b ) <-> ( W e. ( N WWalksN G ) /\ ( W ` 0 ) = a /\ ( W ` N ) = b ) )
42 41 bicomi 
 |-  ( ( W e. ( N WWalksN G ) /\ ( W ` 0 ) = a /\ ( W ` N ) = b ) <-> W e. ( a ( N WWalksNOn G ) b ) )
43 42 2rexbii 
 |-  ( E. a e. V E. b e. V ( W e. ( N WWalksN G ) /\ ( W ` 0 ) = a /\ ( W ` N ) = b ) <-> E. a e. V E. b e. V W e. ( a ( N WWalksNOn G ) b ) )
44 40 43 bitri 
 |-  ( W e. ( N WWalksN G ) <-> E. a e. V E. b e. V W e. ( a ( N WWalksNOn G ) b ) )