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 )