Metamath Proof Explorer

Theorem wspthsnwspthsnon

Description: A simple path of fixed length is a simple path of fixed length between two vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018) (Revised by AV, 16-May-2021) (Revised by AV, 13-Mar-2022)

Ref Expression
Hypothesis wwlksnwwlksnon.v 
|- V = ( Vtx ` G )
Assertion wspthsnwspthsnon 
|- ( W e. ( N WSPathsN G ) <-> E. a e. V E. b e. V W e. ( a ( N WSPathsNOn G ) b ) )

Proof

Step Hyp Ref Expression
1 wwlksnwwlksnon.v 
 |-  V = ( Vtx ` G )
2 iswspthn 
 |-  ( W e. ( N WSPathsN G ) <-> ( W e. ( N WWalksN G ) /\ E. f f ( SPaths ` G ) W ) )
3 1 wwlksnwwlksnon 
 |-  ( W e. ( N WWalksN G ) <-> E. a e. V E. b e. V W e. ( a ( N WWalksNOn G ) b ) )
4 3 anbi1i 
 |-  ( ( W e. ( N WWalksN G ) /\ E. f f ( SPaths ` G ) W ) <-> ( E. a e. V E. b e. V W e. ( a ( N WWalksNOn G ) b ) /\ E. f f ( SPaths ` G ) W ) )
5 r19.41vv 
 |-  ( E. a e. V E. b e. V ( W e. ( a ( N WWalksNOn G ) b ) /\ E. f f ( SPaths ` G ) W ) <-> ( E. a e. V E. b e. V W e. ( a ( N WWalksNOn G ) b ) /\ E. f f ( SPaths ` G ) W ) )
6 4 5 bitr4i 
 |-  ( ( W e. ( N WWalksN G ) /\ E. f f ( SPaths ` G ) W ) <-> E. a e. V E. b e. V ( W e. ( a ( N WWalksNOn G ) b ) /\ E. f f ( SPaths ` G ) W ) )
7 3anass 
 |-  ( ( f ( SPaths ` G ) W /\ ( W ` 0 ) = a /\ ( W ` ( # ` f ) ) = b ) <-> ( f ( SPaths ` G ) W /\ ( ( W ` 0 ) = a /\ ( W ` ( # ` f ) ) = b ) ) )
8 7 a1i 
 |-  ( ( ( a e. V /\ b e. V ) /\ W e. ( a ( N WWalksNOn G ) b ) ) -> ( ( f ( SPaths ` G ) W /\ ( W ` 0 ) = a /\ ( W ` ( # ` f ) ) = b ) <-> ( f ( SPaths ` G ) W /\ ( ( W ` 0 ) = a /\ ( W ` ( # ` f ) ) = b ) ) ) )
9 vex 
 |-  f e. _V
10 1 isspthonpth 
 |-  ( ( ( a e. V /\ b e. V ) /\ ( f e. _V /\ W e. ( a ( N WWalksNOn G ) b ) ) ) -> ( f ( a ( SPathsOn ` G ) b ) W <-> ( f ( SPaths ` G ) W /\ ( W ` 0 ) = a /\ ( W ` ( # ` f ) ) = b ) ) )
11 9 10 mpanr1 
 |-  ( ( ( a e. V /\ b e. V ) /\ W e. ( a ( N WWalksNOn G ) b ) ) -> ( f ( a ( SPathsOn ` G ) b ) W <-> ( f ( SPaths ` G ) W /\ ( W ` 0 ) = a /\ ( W ` ( # ` f ) ) = b ) ) )
12 spthiswlk 
 |-  ( f ( SPaths ` G ) W -> f ( Walks ` G ) W )
13 wlklenvm1 
 |-  ( f ( Walks ` G ) W -> ( # ` f ) = ( ( # ` W ) - 1 ) )
14 wwlknon 
 |-  ( W e. ( a ( N WWalksNOn G ) b ) <-> ( W e. ( N WWalksN G ) /\ ( W ` 0 ) = a /\ ( W ` N ) = b ) )
15 simpl2 
 |-  ( ( ( W e. ( N WWalksN G ) /\ ( W ` 0 ) = a /\ ( W ` N ) = b ) /\ ( # ` f ) = ( ( # ` W ) - 1 ) ) -> ( W ` 0 ) = a )
16 simpr 
 |-  ( ( ( W e. ( N WWalksN G ) /\ ( W ` 0 ) = a /\ ( W ` N ) = b ) /\ ( # ` f ) = ( ( # ` W ) - 1 ) ) -> ( # ` f ) = ( ( # ` W ) - 1 ) )
17 wwlknbp1 
 |-  ( W e. ( N WWalksN G ) -> ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) )
18 oveq1 
 |-  ( ( # ` W ) = ( N + 1 ) -> ( ( # ` W ) - 1 ) = ( ( N + 1 ) - 1 ) )
19 18 3ad2ant3 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( ( # ` W ) - 1 ) = ( ( N + 1 ) - 1 ) )
20 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
21 pncan1 
 |-  ( N e. CC -> ( ( N + 1 ) - 1 ) = N )
22 20 21 syl 
 |-  ( N e. NN0 -> ( ( N + 1 ) - 1 ) = N )
23 22 3ad2ant1 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( ( N + 1 ) - 1 ) = N )
24 19 23 eqtrd 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( ( # ` W ) - 1 ) = N )
25 17 24 syl 
 |-  ( W e. ( N WWalksN G ) -> ( ( # ` W ) - 1 ) = N )
26 25 3ad2ant1 
 |-  ( ( W e. ( N WWalksN G ) /\ ( W ` 0 ) = a /\ ( W ` N ) = b ) -> ( ( # ` W ) - 1 ) = N )
27 26 adantr 
 |-  ( ( ( W e. ( N WWalksN G ) /\ ( W ` 0 ) = a /\ ( W ` N ) = b ) /\ ( # ` f ) = ( ( # ` W ) - 1 ) ) -> ( ( # ` W ) - 1 ) = N )
28 16 27 eqtrd 
 |-  ( ( ( W e. ( N WWalksN G ) /\ ( W ` 0 ) = a /\ ( W ` N ) = b ) /\ ( # ` f ) = ( ( # ` W ) - 1 ) ) -> ( # ` f ) = N )
29 28 fveq2d 
 |-  ( ( ( W e. ( N WWalksN G ) /\ ( W ` 0 ) = a /\ ( W ` N ) = b ) /\ ( # ` f ) = ( ( # ` W ) - 1 ) ) -> ( W ` ( # ` f ) ) = ( W ` N ) )
30 simpl3 
 |-  ( ( ( W e. ( N WWalksN G ) /\ ( W ` 0 ) = a /\ ( W ` N ) = b ) /\ ( # ` f ) = ( ( # ` W ) - 1 ) ) -> ( W ` N ) = b )
31 29 30 eqtrd 
 |-  ( ( ( W e. ( N WWalksN G ) /\ ( W ` 0 ) = a /\ ( W ` N ) = b ) /\ ( # ` f ) = ( ( # ` W ) - 1 ) ) -> ( W ` ( # ` f ) ) = b )
32 15 31 jca 
 |-  ( ( ( W e. ( N WWalksN G ) /\ ( W ` 0 ) = a /\ ( W ` N ) = b ) /\ ( # ` f ) = ( ( # ` W ) - 1 ) ) -> ( ( W ` 0 ) = a /\ ( W ` ( # ` f ) ) = b ) )
33 32 ex 
 |-  ( ( W e. ( N WWalksN G ) /\ ( W ` 0 ) = a /\ ( W ` N ) = b ) -> ( ( # ` f ) = ( ( # ` W ) - 1 ) -> ( ( W ` 0 ) = a /\ ( W ` ( # ` f ) ) = b ) ) )
34 14 33 sylbi 
 |-  ( W e. ( a ( N WWalksNOn G ) b ) -> ( ( # ` f ) = ( ( # ` W ) - 1 ) -> ( ( W ` 0 ) = a /\ ( W ` ( # ` f ) ) = b ) ) )
35 34 adantl 
 |-  ( ( ( a e. V /\ b e. V ) /\ W e. ( a ( N WWalksNOn G ) b ) ) -> ( ( # ` f ) = ( ( # ` W ) - 1 ) -> ( ( W ` 0 ) = a /\ ( W ` ( # ` f ) ) = b ) ) )
36 35 com12 
 |-  ( ( # ` f ) = ( ( # ` W ) - 1 ) -> ( ( ( a e. V /\ b e. V ) /\ W e. ( a ( N WWalksNOn G ) b ) ) -> ( ( W ` 0 ) = a /\ ( W ` ( # ` f ) ) = b ) ) )
37 12 13 36 3syl 
 |-  ( f ( SPaths ` G ) W -> ( ( ( a e. V /\ b e. V ) /\ W e. ( a ( N WWalksNOn G ) b ) ) -> ( ( W ` 0 ) = a /\ ( W ` ( # ` f ) ) = b ) ) )
38 37 com12 
 |-  ( ( ( a e. V /\ b e. V ) /\ W e. ( a ( N WWalksNOn G ) b ) ) -> ( f ( SPaths ` G ) W -> ( ( W ` 0 ) = a /\ ( W ` ( # ` f ) ) = b ) ) )
39 38 pm4.71d 
 |-  ( ( ( a e. V /\ b e. V ) /\ W e. ( a ( N WWalksNOn G ) b ) ) -> ( f ( SPaths ` G ) W <-> ( f ( SPaths ` G ) W /\ ( ( W ` 0 ) = a /\ ( W ` ( # ` f ) ) = b ) ) ) )
40 8 11 39 3bitr4rd 
 |-  ( ( ( a e. V /\ b e. V ) /\ W e. ( a ( N WWalksNOn G ) b ) ) -> ( f ( SPaths ` G ) W <-> f ( a ( SPathsOn ` G ) b ) W ) )
41 40 exbidv 
 |-  ( ( ( a e. V /\ b e. V ) /\ W e. ( a ( N WWalksNOn G ) b ) ) -> ( E. f f ( SPaths ` G ) W <-> E. f f ( a ( SPathsOn ` G ) b ) W ) )
42 41 pm5.32da 
 |-  ( ( a e. V /\ b e. V ) -> ( ( W e. ( a ( N WWalksNOn G ) b ) /\ E. f f ( SPaths ` G ) W ) <-> ( W e. ( a ( N WWalksNOn G ) b ) /\ E. f f ( a ( SPathsOn ` G ) b ) W ) ) )
43 wspthnon 
 |-  ( W e. ( a ( N WSPathsNOn G ) b ) <-> ( W e. ( a ( N WWalksNOn G ) b ) /\ E. f f ( a ( SPathsOn ` G ) b ) W ) )
44 42 43 bitr4di 
 |-  ( ( a e. V /\ b e. V ) -> ( ( W e. ( a ( N WWalksNOn G ) b ) /\ E. f f ( SPaths ` G ) W ) <-> W e. ( a ( N WSPathsNOn G ) b ) ) )
45 44 2rexbiia 
 |-  ( E. a e. V E. b e. V ( W e. ( a ( N WWalksNOn G ) b ) /\ E. f f ( SPaths ` G ) W ) <-> E. a e. V E. b e. V W e. ( a ( N WSPathsNOn G ) b ) )
46 2 6 45 3bitri 
 |-  ( W e. ( N WSPathsN G ) <-> E. a e. V E. b e. V W e. ( a ( N WSPathsNOn G ) b ) )