Theorem upgrf1istrl

Description: Properties of a pair of a one-to-one function into the set of indices of edges and a function into the set of vertices to be a trail in a pseudograph. (Contributed by Alexander van der Vekens, 20-Oct-2017) (Revised by AV, 7-Jan-2021) (Revised by AV, 29-Oct-2021)

	Ref	Expression
Hypotheses	upgrtrls.v	|- V = ( Vtx ` G )
	upgrtrls.i	|- I = ( iEdg ` G )
Assertion	upgrf1istrl	|- ( G e. UPGraph -> ( F ( Trails ` G ) P <-> ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		upgrtrls.v	|- V = ( Vtx ` G )
2		upgrtrls.i	|- I = ( iEdg ` G )
3	1 2	upgristrl	|- ( G e. UPGraph -> ( F ( Trails ` G ) P <-> ( ( F e. Word dom I /\ Fun `' F ) /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
4		iswrdb	|- ( F e. Word dom I <-> F : ( 0 ..^ ( # ` F ) ) --> dom I )
5	4	a1i	|- ( G e. UPGraph -> ( F e. Word dom I <-> F : ( 0 ..^ ( # ` F ) ) --> dom I ) )
6	5	anbi1d	|- ( G e. UPGraph -> ( ( F e. Word dom I /\ Fun `' F ) <-> ( F : ( 0 ..^ ( # ` F ) ) --> dom I /\ Fun `' F ) ) )
7		df-f1	|- ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I <-> ( F : ( 0 ..^ ( # ` F ) ) --> dom I /\ Fun `' F ) )
8	6 7	bitr4di	|- ( G e. UPGraph -> ( ( F e. Word dom I /\ Fun `' F ) <-> F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I ) )
9	8	3anbi1d	|- ( G e. UPGraph -> ( ( ( F e. Word dom I /\ Fun `' F ) /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) <-> ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
10	3 9	bitrd	|- ( G e. UPGraph -> ( F ( Trails ` G ) P <-> ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )