Metamath Proof Explorer

Theorem upgristrl

Description: Properties of a pair of functions to be a trail in a pseudograph, definition of walks expanded. (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 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 ) ) } ) ) )

Proof

Step Hyp Ref Expression
1 upgrtrls.v 
 |-  V = ( Vtx ` G )
2 upgrtrls.i 
 |-  I = ( iEdg ` G )
3 istrl 
 |-  ( F ( Trails ` G ) P <-> ( F ( Walks ` G ) P /\ Fun `' F ) )
4 1 2 upgriswlk 
 |-  ( G e. UPGraph -> ( F ( Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
5 4 anbi1d 
 |-  ( G e. UPGraph -> ( ( F ( Walks ` G ) P /\ Fun `' F ) <-> ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) /\ Fun `' F ) ) )
6 an32 
 |-  ( ( ( F e. Word dom I /\ ( P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) /\ Fun `' F ) <-> ( ( F e. Word dom I /\ Fun `' F ) /\ ( P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
7 3anass 
 |-  ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) <-> ( F e. Word dom I /\ ( P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
8 7 anbi1i 
 |-  ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) /\ Fun `' F ) <-> ( ( F e. Word dom I /\ ( P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) /\ Fun `' F ) )
9 3anass 
 |-  ( ( ( 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 e. Word dom I /\ Fun `' F ) /\ ( P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
10 6 8 9 3bitr4i 
 |-  ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) /\ Fun `' F ) <-> ( ( F e. Word dom I /\ Fun `' F ) /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
11 5 10 bitrdi 
 |-  ( G e. UPGraph -> ( ( F ( Walks ` G ) P /\ Fun `' F ) <-> ( ( F e. Word dom I /\ Fun `' F ) /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
12 3 11 syl5bb 
 |-  ( 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 ) ) } ) ) )