This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pthd

Description: Two words representing a trail which also represent a path in a graph. (Contributed by AV, 10-Feb-2021) (Proof shortened by AV, 30-Oct-2021)

Ref Expression
Hypotheses pthd.p 
|- ( ph -> P e. Word _V )
pthd.r 
|- R = ( ( # ` P ) - 1 )
pthd.s 
|- ( ph -> A. i e. ( 0 ..^ ( # ` P ) ) A. j e. ( 1 ..^ R ) ( i =/= j -> ( P ` i ) =/= ( P ` j ) ) )
pthd.f 
|- ( # ` F ) = R
pthd.t 
|- ( ph -> F ( Trails ` G ) P )
Assertion pthd 
|- ( ph -> F ( Paths ` G ) P )

Proof

Step Hyp Ref Expression
1 pthd.p 
 |-  ( ph -> P e. Word _V )
2 pthd.r 
 |-  R = ( ( # ` P ) - 1 )
3 pthd.s 
 |-  ( ph -> A. i e. ( 0 ..^ ( # ` P ) ) A. j e. ( 1 ..^ R ) ( i =/= j -> ( P ` i ) =/= ( P ` j ) ) )
4 pthd.f 
 |-  ( # ` F ) = R
5 pthd.t 
 |-  ( ph -> F ( Trails ` G ) P )
6 4 2 eqtri 
 |-  ( # ` F ) = ( ( # ` P ) - 1 )
7 4 oveq2i 
 |-  ( 1 ..^ ( # ` F ) ) = ( 1 ..^ R )
8 7 raleqi 
 |-  ( A. j e. ( 1 ..^ ( # ` F ) ) ( i =/= j -> ( P ` i ) =/= ( P ` j ) ) <-> A. j e. ( 1 ..^ R ) ( i =/= j -> ( P ` i ) =/= ( P ` j ) ) )
9 8 ralbii 
 |-  ( A. i e. ( 0 ..^ ( # ` P ) ) A. j e. ( 1 ..^ ( # ` F ) ) ( i =/= j -> ( P ` i ) =/= ( P ` j ) ) <-> A. i e. ( 0 ..^ ( # ` P ) ) A. j e. ( 1 ..^ R ) ( i =/= j -> ( P ` i ) =/= ( P ` j ) ) )
10 3 9 sylibr 
 |-  ( ph -> A. i e. ( 0 ..^ ( # ` P ) ) A. j e. ( 1 ..^ ( # ` F ) ) ( i =/= j -> ( P ` i ) =/= ( P ` j ) ) )
11 1 6 10 pthdlem1 
 |-  ( ph -> Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) )
12 1 6 10 pthdlem2 
 |-  ( ph -> ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) )
13 ispth 
 |-  ( F ( Paths ` G ) P <-> ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) )
14 5 11 12 13 syl3anbrc 
 |-  ( ph -> F ( Paths ` G ) P )