Metamath Proof Explorer

Theorem iswlk

Description: Properties of a pair of functions to be a walk. (Contributed by AV, 30-Dec-2020)

Ref Expression
Hypotheses wksfval.v 
|- V = ( Vtx ` G )
wksfval.i 
|- I = ( iEdg ` G )
Assertion iswlk 
|- ( ( G e. W /\ F e. U /\ P e. Z ) -> ( F ( Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 wksfval.v 
 |-  V = ( Vtx ` G )
2 wksfval.i 
 |-  I = ( iEdg ` G )
3 df-br 
 |-  ( F ( Walks ` G ) P <-> <. F , P >. e. ( Walks ` G ) )
4 1 2 wksfval 
 |-  ( G e. W -> ( Walks ` G ) = { <. f , p >. | ( f e. Word dom I /\ p : ( 0 ... ( # ` f ) ) --> V /\ A. k e. ( 0 ..^ ( # ` f ) ) if- ( ( p ` k ) = ( p ` ( k + 1 ) ) , ( I ` ( f ` k ) ) = { ( p ` k ) } , { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( I ` ( f ` k ) ) ) ) } )
5 4 3ad2ant1 
 |-  ( ( G e. W /\ F e. U /\ P e. Z ) -> ( Walks ` G ) = { <. f , p >. | ( f e. Word dom I /\ p : ( 0 ... ( # ` f ) ) --> V /\ A. k e. ( 0 ..^ ( # ` f ) ) if- ( ( p ` k ) = ( p ` ( k + 1 ) ) , ( I ` ( f ` k ) ) = { ( p ` k ) } , { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( I ` ( f ` k ) ) ) ) } )
6 5 eleq2d 
 |-  ( ( G e. W /\ F e. U /\ P e. Z ) -> ( <. F , P >. e. ( Walks ` G ) <-> <. F , P >. e. { <. f , p >. | ( f e. Word dom I /\ p : ( 0 ... ( # ` f ) ) --> V /\ A. k e. ( 0 ..^ ( # ` f ) ) if- ( ( p ` k ) = ( p ` ( k + 1 ) ) , ( I ` ( f ` k ) ) = { ( p ` k ) } , { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( I ` ( f ` k ) ) ) ) } ) )
7 3 6 syl5bb 
 |-  ( ( G e. W /\ F e. U /\ P e. Z ) -> ( F ( Walks ` G ) P <-> <. F , P >. e. { <. f , p >. | ( f e. Word dom I /\ p : ( 0 ... ( # ` f ) ) --> V /\ A. k e. ( 0 ..^ ( # ` f ) ) if- ( ( p ` k ) = ( p ` ( k + 1 ) ) , ( I ` ( f ` k ) ) = { ( p ` k ) } , { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( I ` ( f ` k ) ) ) ) } ) )
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 
 |-  ( p = P -> ( p ` k ) = ( P ` k ) )
18 fveq1 
 |-  ( p = P -> ( p ` ( k + 1 ) ) = ( P ` ( k + 1 ) ) )
19 17 18 eqeq12d 
 |-  ( p = P -> ( ( p ` k ) = ( p ` ( k + 1 ) ) <-> ( P ` k ) = ( P ` ( k + 1 ) ) ) )
20 19 adantl 
 |-  ( ( f = F /\ p = P ) -> ( ( p ` k ) = ( p ` ( k + 1 ) ) <-> ( P ` k ) = ( P ` ( k + 1 ) ) ) )
21 fveq1 
 |-  ( f = F -> ( f ` k ) = ( F ` k ) )
22 21 fveq2d 
 |-  ( f = F -> ( I ` ( f ` k ) ) = ( I ` ( F ` k ) ) )
23 17 sneqd 
 |-  ( p = P -> { ( p ` k ) } = { ( P ` k ) } )
24 22 23 eqeqan12d 
 |-  ( ( f = F /\ p = P ) -> ( ( I ` ( f ` k ) ) = { ( p ` k ) } <-> ( I ` ( F ` k ) ) = { ( P ` k ) } ) )
25 17 18 preq12d 
 |-  ( p = P -> { ( p ` k ) , ( p ` ( k + 1 ) ) } = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
26 25 adantl 
 |-  ( ( f = F /\ p = P ) -> { ( p ` k ) , ( p ` ( k + 1 ) ) } = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
27 22 adantr 
 |-  ( ( f = F /\ p = P ) -> ( I ` ( f ` k ) ) = ( I ` ( F ` k ) ) )
28 26 27 sseq12d 
 |-  ( ( f = F /\ p = P ) -> ( { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( I ` ( f ` k ) ) <-> { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) )
29 20 24 28 ifpbi123d 
 |-  ( ( f = F /\ p = P ) -> ( if- ( ( p ` k ) = ( p ` ( k + 1 ) ) , ( I ` ( f ` k ) ) = { ( p ` k ) } , { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( I ` ( f ` k ) ) ) <-> if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) )
30 16 29 raleqbidv 
 |-  ( ( f = F /\ p = P ) -> ( A. k e. ( 0 ..^ ( # ` f ) ) if- ( ( p ` k ) = ( p ` ( k + 1 ) ) , ( I ` ( f ` k ) ) = { ( p ` k ) } , { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( I ` ( f ` k ) ) ) <-> A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) )
31 9 14 30 3anbi123d 
 |-  ( ( f = F /\ p = P ) -> ( ( f e. Word dom I /\ p : ( 0 ... ( # ` f ) ) --> V /\ A. k e. ( 0 ..^ ( # ` f ) ) if- ( ( p ` k ) = ( p ` ( k + 1 ) ) , ( I ` ( f ` k ) ) = { ( p ` k ) } , { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( I ` ( f ` k ) ) ) ) <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) )
32 31 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 ) ) if- ( ( p ` k ) = ( p ` ( k + 1 ) ) , ( I ` ( f ` k ) ) = { ( p ` k ) } , { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( I ` ( f ` k ) ) ) ) } <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) )
33 32 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 ) ) if- ( ( p ` k ) = ( p ` ( k + 1 ) ) , ( I ` ( f ` k ) ) = { ( p ` k ) } , { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( I ` ( f ` k ) ) ) ) } <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) )
34 7 33 bitrd 
 |-  ( ( G e. W /\ F e. U /\ P e. Z ) -> ( F ( Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) )