Metamath Proof Explorer

Theorem elwspths2spth

Description: A simple path of length 2 between two vertices as length 3 string in a pseudograph. (Contributed by Alexander van der Vekens, 28-Feb-2018) (Revised by AV, 18-May-2021) (Proof shortened by AV, 16-Mar-2022)

Ref Expression
Hypothesis elwwlks2.v 
|- V = ( Vtx ` G )
Assertion elwspths2spth 
|- ( G e. UPGraph -> ( W e. ( 2 WSPathsN G ) <-> E. a e. V E. b e. V E. c e. V ( W = <" a b c "> /\ E. f E. p ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elwwlks2.v 
 |-  V = ( Vtx ` G )
2 1 wspthsnwspthsnon 
 |-  ( W e. ( 2 WSPathsN G ) <-> E. a e. V E. c e. V W e. ( a ( 2 WSPathsNOn G ) c ) )
3 2 a1i 
 |-  ( G e. UPGraph -> ( W e. ( 2 WSPathsN G ) <-> E. a e. V E. c e. V W e. ( a ( 2 WSPathsNOn G ) c ) ) )
4 1 elwspths2on 
 |-  ( ( G e. UPGraph /\ a e. V /\ c e. V ) -> ( W e. ( a ( 2 WSPathsNOn G ) c ) <-> E. b e. V ( W = <" a b c "> /\ <" a b c "> e. ( a ( 2 WSPathsNOn G ) c ) ) ) )
5 4 3expb 
 |-  ( ( G e. UPGraph /\ ( a e. V /\ c e. V ) ) -> ( W e. ( a ( 2 WSPathsNOn G ) c ) <-> E. b e. V ( W = <" a b c "> /\ <" a b c "> e. ( a ( 2 WSPathsNOn G ) c ) ) ) )
6 5 2rexbidva 
 |-  ( G e. UPGraph -> ( E. a e. V E. c e. V W e. ( a ( 2 WSPathsNOn G ) c ) <-> E. a e. V E. c e. V E. b e. V ( W = <" a b c "> /\ <" a b c "> e. ( a ( 2 WSPathsNOn G ) c ) ) ) )
7 rexcom 
 |-  ( E. c e. V E. b e. V ( W = <" a b c "> /\ <" a b c "> e. ( a ( 2 WSPathsNOn G ) c ) ) <-> E. b e. V E. c e. V ( W = <" a b c "> /\ <" a b c "> e. ( a ( 2 WSPathsNOn G ) c ) ) )
8 wspthnon 
 |-  ( <" a b c "> e. ( a ( 2 WSPathsNOn G ) c ) <-> ( <" a b c "> e. ( a ( 2 WWalksNOn G ) c ) /\ E. f f ( a ( SPathsOn ` G ) c ) <" a b c "> ) )
9 ancom 
 |-  ( ( <" a b c "> e. ( a ( 2 WWalksNOn G ) c ) /\ E. f f ( a ( SPathsOn ` G ) c ) <" a b c "> ) <-> ( E. f f ( a ( SPathsOn ` G ) c ) <" a b c "> /\ <" a b c "> e. ( a ( 2 WWalksNOn G ) c ) ) )
10 19.41v 
 |-  ( E. f ( f ( a ( SPathsOn ` G ) c ) <" a b c "> /\ <" a b c "> e. ( a ( 2 WWalksNOn G ) c ) ) <-> ( E. f f ( a ( SPathsOn ` G ) c ) <" a b c "> /\ <" a b c "> e. ( a ( 2 WWalksNOn G ) c ) ) )
11 9 10 bitr4i 
 |-  ( ( <" a b c "> e. ( a ( 2 WWalksNOn G ) c ) /\ E. f f ( a ( SPathsOn ` G ) c ) <" a b c "> ) <-> E. f ( f ( a ( SPathsOn ` G ) c ) <" a b c "> /\ <" a b c "> e. ( a ( 2 WWalksNOn G ) c ) ) )
12 simpr 
 |-  ( ( G e. UPGraph /\ a e. V ) -> a e. V )
13 simpr 
 |-  ( ( b e. V /\ c e. V ) -> c e. V )
14 12 13 anim12i 
 |-  ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) -> ( a e. V /\ c e. V ) )
15 vex 
 |-  f e. _V
16 s3cli 
 |-  <" a b c "> e. Word _V
17 15 16 pm3.2i 
 |-  ( f e. _V /\ <" a b c "> e. Word _V )
18 1 isspthonpth 
 |-  ( ( ( a e. V /\ c e. V ) /\ ( f e. _V /\ <" a b c "> e. Word _V ) ) -> ( f ( a ( SPathsOn ` G ) c ) <" a b c "> <-> ( f ( SPaths ` G ) <" a b c "> /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` ( # ` f ) ) = c ) ) )
19 14 17 18 sylancl 
 |-  ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) -> ( f ( a ( SPathsOn ` G ) c ) <" a b c "> <-> ( f ( SPaths ` G ) <" a b c "> /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` ( # ` f ) ) = c ) ) )
20 wwlknon 
 |-  ( <" a b c "> e. ( a ( 2 WWalksNOn G ) c ) <-> ( <" a b c "> e. ( 2 WWalksN G ) /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` 2 ) = c ) )
21 2nn0 
 |-  2 e. NN0
22 iswwlksn 
 |-  ( 2 e. NN0 -> ( <" a b c "> e. ( 2 WWalksN G ) <-> ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) ) )
23 21 22 mp1i 
 |-  ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) -> ( <" a b c "> e. ( 2 WWalksN G ) <-> ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) ) )
24 23 3anbi1d 
 |-  ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) -> ( ( <" a b c "> e. ( 2 WWalksN G ) /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` 2 ) = c ) <-> ( ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` 2 ) = c ) ) )
25 20 24 bitrid 
 |-  ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) -> ( <" a b c "> e. ( a ( 2 WWalksNOn G ) c ) <-> ( ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` 2 ) = c ) ) )
26 19 25 anbi12d 
 |-  ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) -> ( ( f ( a ( SPathsOn ` G ) c ) <" a b c "> /\ <" a b c "> e. ( a ( 2 WWalksNOn G ) c ) ) <-> ( ( f ( SPaths ` G ) <" a b c "> /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` ( # ` f ) ) = c ) /\ ( ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` 2 ) = c ) ) ) )
27 26 adantr 
 |-  ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ W = <" a b c "> ) -> ( ( f ( a ( SPathsOn ` G ) c ) <" a b c "> /\ <" a b c "> e. ( a ( 2 WWalksNOn G ) c ) ) <-> ( ( f ( SPaths ` G ) <" a b c "> /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` ( # ` f ) ) = c ) /\ ( ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` 2 ) = c ) ) ) )
28 16 a1i 
 |-  ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) -> <" a b c "> e. Word _V )
29 simprl1 
 |-  ( ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ p = <" a b c "> ) /\ ( ( f ( SPaths ` G ) <" a b c "> /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` ( # ` f ) ) = c ) /\ ( ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` 2 ) = c ) ) ) -> f ( SPaths ` G ) <" a b c "> )
30 spthiswlk 
 |-  ( f ( SPaths ` G ) <" a b c "> -> f ( Walks ` G ) <" a b c "> )
31 wlklenvm1 
 |-  ( f ( Walks ` G ) <" a b c "> -> ( # ` f ) = ( ( # ` <" a b c "> ) - 1 ) )
32 simpl 
 |-  ( ( ( # ` f ) = ( ( # ` <" a b c "> ) - 1 ) /\ ( ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` 2 ) = c ) ) -> ( # ` f ) = ( ( # ` <" a b c "> ) - 1 ) )
33 oveq1 
 |-  ( ( # ` <" a b c "> ) = ( 2 + 1 ) -> ( ( # ` <" a b c "> ) - 1 ) = ( ( 2 + 1 ) - 1 ) )
34 2cn 
 |-  2 e. CC
35 pncan1 
 |-  ( 2 e. CC -> ( ( 2 + 1 ) - 1 ) = 2 )
36 34 35 ax-mp 
 |-  ( ( 2 + 1 ) - 1 ) = 2
37 33 36 eqtrdi 
 |-  ( ( # ` <" a b c "> ) = ( 2 + 1 ) -> ( ( # ` <" a b c "> ) - 1 ) = 2 )
38 37 adantl 
 |-  ( ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) -> ( ( # ` <" a b c "> ) - 1 ) = 2 )
39 38 3ad2ant1 
 |-  ( ( ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` 2 ) = c ) -> ( ( # ` <" a b c "> ) - 1 ) = 2 )
40 39 adantl 
 |-  ( ( ( # ` f ) = ( ( # ` <" a b c "> ) - 1 ) /\ ( ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` 2 ) = c ) ) -> ( ( # ` <" a b c "> ) - 1 ) = 2 )
41 32 40 eqtrd 
 |-  ( ( ( # ` f ) = ( ( # ` <" a b c "> ) - 1 ) /\ ( ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` 2 ) = c ) ) -> ( # ` f ) = 2 )
42 41 ex 
 |-  ( ( # ` f ) = ( ( # ` <" a b c "> ) - 1 ) -> ( ( ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` 2 ) = c ) -> ( # ` f ) = 2 ) )
43 30 31 42 3syl 
 |-  ( f ( SPaths ` G ) <" a b c "> -> ( ( ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` 2 ) = c ) -> ( # ` f ) = 2 ) )
44 43 3ad2ant1 
 |-  ( ( f ( SPaths ` G ) <" a b c "> /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` ( # ` f ) ) = c ) -> ( ( ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` 2 ) = c ) -> ( # ` f ) = 2 ) )
45 44 imp 
 |-  ( ( ( f ( SPaths ` G ) <" a b c "> /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` ( # ` f ) ) = c ) /\ ( ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` 2 ) = c ) ) -> ( # ` f ) = 2 )
46 45 adantl 
 |-  ( ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ p = <" a b c "> ) /\ ( ( f ( SPaths ` G ) <" a b c "> /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` ( # ` f ) ) = c ) /\ ( ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` 2 ) = c ) ) ) -> ( # ` f ) = 2 )
47 s3fv0 
 |-  ( a e. _V -> ( <" a b c "> ` 0 ) = a )
48 47 elv 
 |-  ( <" a b c "> ` 0 ) = a
49 48 eqcomi 
 |-  a = ( <" a b c "> ` 0 )
50 s3fv1 
 |-  ( b e. _V -> ( <" a b c "> ` 1 ) = b )
51 50 elv 
 |-  ( <" a b c "> ` 1 ) = b
52 51 eqcomi 
 |-  b = ( <" a b c "> ` 1 )
53 s3fv2 
 |-  ( c e. _V -> ( <" a b c "> ` 2 ) = c )
54 53 elv 
 |-  ( <" a b c "> ` 2 ) = c
55 54 eqcomi 
 |-  c = ( <" a b c "> ` 2 )
56 49 52 55 3pm3.2i 
 |-  ( a = ( <" a b c "> ` 0 ) /\ b = ( <" a b c "> ` 1 ) /\ c = ( <" a b c "> ` 2 ) )
57 56 a1i 
 |-  ( ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ p = <" a b c "> ) /\ ( ( f ( SPaths ` G ) <" a b c "> /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` ( # ` f ) ) = c ) /\ ( ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` 2 ) = c ) ) ) -> ( a = ( <" a b c "> ` 0 ) /\ b = ( <" a b c "> ` 1 ) /\ c = ( <" a b c "> ` 2 ) ) )
58 29 46 57 3jca 
 |-  ( ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ p = <" a b c "> ) /\ ( ( f ( SPaths ` G ) <" a b c "> /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` ( # ` f ) ) = c ) /\ ( ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` 2 ) = c ) ) ) -> ( f ( SPaths ` G ) <" a b c "> /\ ( # ` f ) = 2 /\ ( a = ( <" a b c "> ` 0 ) /\ b = ( <" a b c "> ` 1 ) /\ c = ( <" a b c "> ` 2 ) ) ) )
59 breq2 
 |-  ( p = <" a b c "> -> ( f ( SPaths ` G ) p <-> f ( SPaths ` G ) <" a b c "> ) )
60 fveq1 
 |-  ( p = <" a b c "> -> ( p ` 0 ) = ( <" a b c "> ` 0 ) )
61 60 eqeq2d 
 |-  ( p = <" a b c "> -> ( a = ( p ` 0 ) <-> a = ( <" a b c "> ` 0 ) ) )
62 fveq1 
 |-  ( p = <" a b c "> -> ( p ` 1 ) = ( <" a b c "> ` 1 ) )
63 62 eqeq2d 
 |-  ( p = <" a b c "> -> ( b = ( p ` 1 ) <-> b = ( <" a b c "> ` 1 ) ) )
64 fveq1 
 |-  ( p = <" a b c "> -> ( p ` 2 ) = ( <" a b c "> ` 2 ) )
65 64 eqeq2d 
 |-  ( p = <" a b c "> -> ( c = ( p ` 2 ) <-> c = ( <" a b c "> ` 2 ) ) )
66 61 63 65 3anbi123d 
 |-  ( p = <" a b c "> -> ( ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) <-> ( a = ( <" a b c "> ` 0 ) /\ b = ( <" a b c "> ` 1 ) /\ c = ( <" a b c "> ` 2 ) ) ) )
67 59 66 3anbi13d 
 |-  ( p = <" a b c "> -> ( ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) <-> ( f ( SPaths ` G ) <" a b c "> /\ ( # ` f ) = 2 /\ ( a = ( <" a b c "> ` 0 ) /\ b = ( <" a b c "> ` 1 ) /\ c = ( <" a b c "> ` 2 ) ) ) ) )
68 67 ad2antlr 
 |-  ( ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ p = <" a b c "> ) /\ ( ( f ( SPaths ` G ) <" a b c "> /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` ( # ` f ) ) = c ) /\ ( ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` 2 ) = c ) ) ) -> ( ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) <-> ( f ( SPaths ` G ) <" a b c "> /\ ( # ` f ) = 2 /\ ( a = ( <" a b c "> ` 0 ) /\ b = ( <" a b c "> ` 1 ) /\ c = ( <" a b c "> ` 2 ) ) ) ) )
69 58 68 mpbird 
 |-  ( ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ p = <" a b c "> ) /\ ( ( f ( SPaths ` G ) <" a b c "> /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` ( # ` f ) ) = c ) /\ ( ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` 2 ) = c ) ) ) -> ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) )
70 69 ex 
 |-  ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ p = <" a b c "> ) -> ( ( ( f ( SPaths ` G ) <" a b c "> /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` ( # ` f ) ) = c ) /\ ( ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` 2 ) = c ) ) -> ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) )
71 28 70 spcimedv 
 |-  ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) -> ( ( ( f ( SPaths ` G ) <" a b c "> /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` ( # ` f ) ) = c ) /\ ( ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` 2 ) = c ) ) -> E. p ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) )
72 spthiswlk 
 |-  ( f ( SPaths ` G ) p -> f ( Walks ` G ) p )
73 wlklenvp1 
 |-  ( f ( Walks ` G ) p -> ( # ` p ) = ( ( # ` f ) + 1 ) )
74 oveq1 
 |-  ( ( # ` f ) = 2 -> ( ( # ` f ) + 1 ) = ( 2 + 1 ) )
75 2p1e3 
 |-  ( 2 + 1 ) = 3
76 74 75 eqtrdi 
 |-  ( ( # ` f ) = 2 -> ( ( # ` f ) + 1 ) = 3 )
77 76 eqeq2d 
 |-  ( ( # ` f ) = 2 -> ( ( # ` p ) = ( ( # ` f ) + 1 ) <-> ( # ` p ) = 3 ) )
78 77 biimpcd 
 |-  ( ( # ` p ) = ( ( # ` f ) + 1 ) -> ( ( # ` f ) = 2 -> ( # ` p ) = 3 ) )
79 72 73 78 3syl 
 |-  ( f ( SPaths ` G ) p -> ( ( # ` f ) = 2 -> ( # ` p ) = 3 ) )
80 79 imp 
 |-  ( ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 ) -> ( # ` p ) = 3 )
81 80 3adant3 
 |-  ( ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) -> ( # ` p ) = 3 )
82 81 adantl 
 |-  ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) -> ( # ` p ) = 3 )
83 eqcom 
 |-  ( a = ( p ` 0 ) <-> ( p ` 0 ) = a )
84 eqcom 
 |-  ( b = ( p ` 1 ) <-> ( p ` 1 ) = b )
85 eqcom 
 |-  ( c = ( p ` 2 ) <-> ( p ` 2 ) = c )
86 83 84 85 3anbi123i 
 |-  ( ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) <-> ( ( p ` 0 ) = a /\ ( p ` 1 ) = b /\ ( p ` 2 ) = c ) )
87 86 biimpi 
 |-  ( ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) -> ( ( p ` 0 ) = a /\ ( p ` 1 ) = b /\ ( p ` 2 ) = c ) )
88 87 3ad2ant3 
 |-  ( ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) -> ( ( p ` 0 ) = a /\ ( p ` 1 ) = b /\ ( p ` 2 ) = c ) )
89 88 adantl 
 |-  ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) -> ( ( p ` 0 ) = a /\ ( p ` 1 ) = b /\ ( p ` 2 ) = c ) )
90 82 89 jca 
 |-  ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) -> ( ( # ` p ) = 3 /\ ( ( p ` 0 ) = a /\ ( p ` 1 ) = b /\ ( p ` 2 ) = c ) ) )
91 1 wlkpwrd 
 |-  ( f ( Walks ` G ) p -> p e. Word V )
92 72 91 syl 
 |-  ( f ( SPaths ` G ) p -> p e. Word V )
93 92 3ad2ant1 
 |-  ( ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) -> p e. Word V )
94 12 anim1i 
 |-  ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) -> ( a e. V /\ ( b e. V /\ c e. V ) ) )
95 3anass 
 |-  ( ( a e. V /\ b e. V /\ c e. V ) <-> ( a e. V /\ ( b e. V /\ c e. V ) ) )
96 94 95 sylibr 
 |-  ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) -> ( a e. V /\ b e. V /\ c e. V ) )
97 eqwrds3 
 |-  ( ( p e. Word V /\ ( a e. V /\ b e. V /\ c e. V ) ) -> ( p = <" a b c "> <-> ( ( # ` p ) = 3 /\ ( ( p ` 0 ) = a /\ ( p ` 1 ) = b /\ ( p ` 2 ) = c ) ) ) )
98 93 96 97 syl2anr 
 |-  ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) -> ( p = <" a b c "> <-> ( ( # ` p ) = 3 /\ ( ( p ` 0 ) = a /\ ( p ` 1 ) = b /\ ( p ` 2 ) = c ) ) ) )
99 90 98 mpbird 
 |-  ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) -> p = <" a b c "> )
100 59 biimpcd 
 |-  ( f ( SPaths ` G ) p -> ( p = <" a b c "> -> f ( SPaths ` G ) <" a b c "> ) )
101 100 3ad2ant1 
 |-  ( ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) -> ( p = <" a b c "> -> f ( SPaths ` G ) <" a b c "> ) )
102 101 adantl 
 |-  ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) -> ( p = <" a b c "> -> f ( SPaths ` G ) <" a b c "> ) )
103 102 imp 
 |-  ( ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) /\ p = <" a b c "> ) -> f ( SPaths ` G ) <" a b c "> )
104 48 a1i 
 |-  ( ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) /\ p = <" a b c "> ) -> ( <" a b c "> ` 0 ) = a )
105 fveq2 
 |-  ( ( # ` f ) = 2 -> ( <" a b c "> ` ( # ` f ) ) = ( <" a b c "> ` 2 ) )
106 105 54 eqtrdi 
 |-  ( ( # ` f ) = 2 -> ( <" a b c "> ` ( # ` f ) ) = c )
107 106 3ad2ant2 
 |-  ( ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) -> ( <" a b c "> ` ( # ` f ) ) = c )
108 107 ad2antlr 
 |-  ( ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) /\ p = <" a b c "> ) -> ( <" a b c "> ` ( # ` f ) ) = c )
109 103 104 108 3jca 
 |-  ( ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) /\ p = <" a b c "> ) -> ( f ( SPaths ` G ) <" a b c "> /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` ( # ` f ) ) = c ) )
110 wlkiswwlks1 
 |-  ( G e. UPGraph -> ( f ( Walks ` G ) p -> p e. ( WWalks ` G ) ) )
111 110 adantr 
 |-  ( ( G e. UPGraph /\ a e. V ) -> ( f ( Walks ` G ) p -> p e. ( WWalks ` G ) ) )
112 111 adantr 
 |-  ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) -> ( f ( Walks ` G ) p -> p e. ( WWalks ` G ) ) )
113 72 112 syl5com 
 |-  ( f ( SPaths ` G ) p -> ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) -> p e. ( WWalks ` G ) ) )
114 113 3ad2ant1 
 |-  ( ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) -> ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) -> p e. ( WWalks ` G ) ) )
115 114 impcom 
 |-  ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) -> p e. ( WWalks ` G ) )
116 115 adantr 
 |-  ( ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) /\ p = <" a b c "> ) -> p e. ( WWalks ` G ) )
117 eleq1 
 |-  ( p = <" a b c "> -> ( p e. ( WWalks ` G ) <-> <" a b c "> e. ( WWalks ` G ) ) )
118 117 bicomd 
 |-  ( p = <" a b c "> -> ( <" a b c "> e. ( WWalks ` G ) <-> p e. ( WWalks ` G ) ) )
119 118 adantl 
 |-  ( ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) /\ p = <" a b c "> ) -> ( <" a b c "> e. ( WWalks ` G ) <-> p e. ( WWalks ` G ) ) )
120 116 119 mpbird 
 |-  ( ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) /\ p = <" a b c "> ) -> <" a b c "> e. ( WWalks ` G ) )
121 s3len 
 |-  ( # ` <" a b c "> ) = 3
122 df-3 
 |-  3 = ( 2 + 1 )
123 121 122 eqtri 
 |-  ( # ` <" a b c "> ) = ( 2 + 1 )
124 120 123 jctir 
 |-  ( ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) /\ p = <" a b c "> ) -> ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) )
125 54 a1i 
 |-  ( ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) /\ p = <" a b c "> ) -> ( <" a b c "> ` 2 ) = c )
126 124 104 125 3jca 
 |-  ( ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) /\ p = <" a b c "> ) -> ( ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` 2 ) = c ) )
127 109 126 jca 
 |-  ( ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) /\ p = <" a b c "> ) -> ( ( f ( SPaths ` G ) <" a b c "> /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` ( # ` f ) ) = c ) /\ ( ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` 2 ) = c ) ) )
128 99 127 mpdan 
 |-  ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) -> ( ( f ( SPaths ` G ) <" a b c "> /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` ( # ` f ) ) = c ) /\ ( ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` 2 ) = c ) ) )
129 128 ex 
 |-  ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) -> ( ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) -> ( ( f ( SPaths ` G ) <" a b c "> /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` ( # ` f ) ) = c ) /\ ( ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` 2 ) = c ) ) ) )
130 129 exlimdv 
 |-  ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) -> ( E. p ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) -> ( ( f ( SPaths ` G ) <" a b c "> /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` ( # ` f ) ) = c ) /\ ( ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` 2 ) = c ) ) ) )
131 71 130 impbid 
 |-  ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) -> ( ( ( f ( SPaths ` G ) <" a b c "> /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` ( # ` f ) ) = c ) /\ ( ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` 2 ) = c ) ) <-> E. p ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) )
132 131 adantr 
 |-  ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ W = <" a b c "> ) -> ( ( ( f ( SPaths ` G ) <" a b c "> /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` ( # ` f ) ) = c ) /\ ( ( <" a b c "> e. ( WWalks ` G ) /\ ( # ` <" a b c "> ) = ( 2 + 1 ) ) /\ ( <" a b c "> ` 0 ) = a /\ ( <" a b c "> ` 2 ) = c ) ) <-> E. p ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) )
133 27 132 bitrd 
 |-  ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ W = <" a b c "> ) -> ( ( f ( a ( SPathsOn ` G ) c ) <" a b c "> /\ <" a b c "> e. ( a ( 2 WWalksNOn G ) c ) ) <-> E. p ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) )
134 133 exbidv 
 |-  ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ W = <" a b c "> ) -> ( E. f ( f ( a ( SPathsOn ` G ) c ) <" a b c "> /\ <" a b c "> e. ( a ( 2 WWalksNOn G ) c ) ) <-> E. f E. p ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) )
135 11 134 bitrid 
 |-  ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ W = <" a b c "> ) -> ( ( <" a b c "> e. ( a ( 2 WWalksNOn G ) c ) /\ E. f f ( a ( SPathsOn ` G ) c ) <" a b c "> ) <-> E. f E. p ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) )
136 8 135 bitrid 
 |-  ( ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) /\ W = <" a b c "> ) -> ( <" a b c "> e. ( a ( 2 WSPathsNOn G ) c ) <-> E. f E. p ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) )
137 136 pm5.32da 
 |-  ( ( ( G e. UPGraph /\ a e. V ) /\ ( b e. V /\ c e. V ) ) -> ( ( W = <" a b c "> /\ <" a b c "> e. ( a ( 2 WSPathsNOn G ) c ) ) <-> ( W = <" a b c "> /\ E. f E. p ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) ) )
138 137 2rexbidva 
 |-  ( ( G e. UPGraph /\ a e. V ) -> ( E. b e. V E. c e. V ( W = <" a b c "> /\ <" a b c "> e. ( a ( 2 WSPathsNOn G ) c ) ) <-> E. b e. V E. c e. V ( W = <" a b c "> /\ E. f E. p ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) ) )
139 7 138 bitrid 
 |-  ( ( G e. UPGraph /\ a e. V ) -> ( E. c e. V E. b e. V ( W = <" a b c "> /\ <" a b c "> e. ( a ( 2 WSPathsNOn G ) c ) ) <-> E. b e. V E. c e. V ( W = <" a b c "> /\ E. f E. p ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) ) )
140 139 rexbidva 
 |-  ( G e. UPGraph -> ( E. a e. V E. c e. V E. b e. V ( W = <" a b c "> /\ <" a b c "> e. ( a ( 2 WSPathsNOn G ) c ) ) <-> E. a e. V E. b e. V E. c e. V ( W = <" a b c "> /\ E. f E. p ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) ) )
141 3 6 140 3bitrd 
 |-  ( G e. UPGraph -> ( W e. ( 2 WSPathsN G ) <-> E. a e. V E. b e. V E. c e. V ( W = <" a b c "> /\ E. f E. p ( f ( SPaths ` G ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) ) )