Metamath Proof Explorer

Theorem isupwlk

Description: Properties of a pair of functions to be a simple walk. (Contributed by Alexander van der Vekens, 20-Oct-2017) (Revised by AV, 28-Dec-2020)

Ref Expression
Hypotheses upwlksfval.v 
|- V = ( Vtx ` G )
upwlksfval.i 
|- I = ( iEdg ` G )
Assertion isupwlk 
|- ( ( G e. W /\ F e. U /\ P e. Z ) -> ( F ( UPWalks ` G ) P <-> ( F e. Word 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 upwlksfval.v 
 |-  V = ( Vtx ` G )
2 upwlksfval.i 
 |-  I = ( iEdg ` G )
3 df-br 
 |-  ( F ( UPWalks ` G ) P <-> <. F , P >. e. ( UPWalks ` G ) )
4 1 2 upwlksfval 
 |-  ( G e. W -> ( UPWalks ` G ) = { <. f , 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 3ad2ant1 
 |-  ( ( G e. W /\ F e. U /\ P e. Z ) -> ( UPWalks ` G ) = { <. f , p >. | ( f e. Word dom I /\ p : ( 0 ... ( # ` f ) ) --> V /\ A. k e. ( 0 ..^ ( # ` f ) ) ( I ` ( f ` k ) ) = { ( p ` k ) , ( p ` ( k + 1 ) ) } ) } )
6 5 eleq2d 
 |-  ( ( G e. W /\ F e. U /\ P e. Z ) -> ( <. F , P >. e. ( UPWalks ` G ) <-> <. F , P >. e. { <. f , p >. | ( f e. Word dom I /\ p : ( 0 ... ( # ` f ) ) --> V /\ A. k e. ( 0 ..^ ( # ` f ) ) ( I ` ( f ` k ) ) = { ( p ` k ) , ( p ` ( k + 1 ) ) } ) } ) )
7 3 6 syl5bb 
 |-  ( ( G e. W /\ F e. U /\ P e. Z ) -> ( F ( UPWalks ` G ) P <-> <. F , P >. e. { <. f , p >. | ( f e. Word dom I /\ p : ( 0 ... ( # ` f ) ) --> V /\ A. k e. ( 0 ..^ ( # ` f ) ) ( I ` ( f ` k ) ) = { ( p ` k ) , ( p ` ( k + 1 ) ) } ) } ) )
8 eleq1 
 |-  ( f = F -> ( f e. Word dom I <-> F e. Word dom I ) )
9 8 adantr 
 |-  ( ( f = F /\ p = P ) -> ( f e. Word dom I <-> F e. Word dom I ) )
10 simpr 
 |-  ( ( f = F /\ p = P ) -> p = P )
11 fveq2 
 |-  ( f = F -> ( # ` f ) = ( # ` F ) )
12 11 oveq2d 
 |-  ( f = F -> ( 0 ... ( # ` f ) ) = ( 0 ... ( # ` F ) ) )
13 12 adantr 
 |-  ( ( f = F /\ p = P ) -> ( 0 ... ( # ` f ) ) = ( 0 ... ( # ` F ) ) )
14 10 13 feq12d 
 |-  ( ( f = F /\ p = P ) -> ( p : ( 0 ... ( # ` f ) ) --> V <-> P : ( 0 ... ( # ` F ) ) --> V ) )
15 11 oveq2d 
 |-  ( f = F -> ( 0 ..^ ( # ` f ) ) = ( 0 ..^ ( # ` F ) ) )
16 15 adantr 
 |-  ( ( f = F /\ p = P ) -> ( 0 ..^ ( # ` f ) ) = ( 0 ..^ ( # ` F ) ) )
17 fveq1 
 |-  ( f = F -> ( f ` k ) = ( F ` k ) )
18 17 fveq2d 
 |-  ( f = F -> ( I ` ( f ` k ) ) = ( I ` ( F ` k ) ) )
19 fveq1 
 |-  ( p = P -> ( p ` k ) = ( P ` k ) )
20 fveq1 
 |-  ( p = P -> ( p ` ( k + 1 ) ) = ( P ` ( k + 1 ) ) )
21 19 20 preq12d 
 |-  ( p = P -> { ( p ` k ) , ( p ` ( k + 1 ) ) } = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
22 18 21 eqeqan12d 
 |-  ( ( f = F /\ p = P ) -> ( ( I ` ( f ` k ) ) = { ( p ` k ) , ( p ` ( k + 1 ) ) } <-> ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
23 16 22 raleqbidv 
 |-  ( ( f = F /\ p = P ) -> ( A. k e. ( 0 ..^ ( # ` f ) ) ( I ` ( f ` k ) ) = { ( p ` k ) , ( p ` ( k + 1 ) ) } <-> A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
24 9 14 23 3anbi123d 
 |-  ( ( f = F /\ p = P ) -> ( ( 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 ) ) } ) ) )
25 24 opelopabga 
 |-  ( ( F e. U /\ P e. Z ) -> ( <. F , P >. e. { <. f , p >. | ( 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 ) ) } ) ) )
26 25 3adant1 
 |-  ( ( G e. W /\ F e. U /\ P e. Z ) -> ( <. F , P >. e. { <. f , p >. | ( 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 ) ) } ) ) )
27 7 26 bitrd 
 |-  ( ( G e. W /\ F e. U /\ P e. Z ) -> ( F ( UPWalks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )