Metamath Proof Explorer

Theorem upgrtrls

Description: The set of trails in a pseudograph, definition of walks expanded. (Contributed by Alexander van der Vekens, 20-Oct-2017) (Revised by AV, 7-Jan-2021)

Ref Expression
Hypotheses upgrtrls.v 
|- V = ( Vtx ` G )
upgrtrls.i 
|- I = ( iEdg ` G )
Assertion upgrtrls 
|- ( G e. UPGraph -> ( Trails ` G ) = { <. f , 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 trlsfval 
 |-  ( Trails ` G ) = { <. f , 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 11 opabbidv 
 |-  ( G e. UPGraph -> { <. f , p >. | ( f ( Walks ` G ) p /\ Fun `' f ) } = { <. f , 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 ) ) } ) } )
13 3 12 syl5eq 
 |-  ( G e. UPGraph -> ( Trails ` G ) = { <. f , 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 ) ) } ) } )