Metamath Proof Explorer

Theorem wksfval

Description: The set of walks (in an undirected graph). (Contributed by AV, 30-Dec-2020)

Ref Expression
Hypotheses wksfval.v 
|- V = ( Vtx ` G )
wksfval.i 
|- I = ( iEdg ` G )
Assertion 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 ) ) ) ) } )

Proof

Step Hyp Ref Expression
1 wksfval.v 
 |-  V = ( Vtx ` G )
2 wksfval.i 
 |-  I = ( iEdg ` G )
3 df-wlks 
 |-  Walks = ( g e. _V |-> { <. f , p >. | ( f e. Word dom ( iEdg ` g ) /\ p : ( 0 ... ( # ` f ) ) --> ( Vtx ` g ) /\ A. k e. ( 0 ..^ ( # ` f ) ) if- ( ( p ` k ) = ( p ` ( k + 1 ) ) , ( ( iEdg ` g ) ` ( f ` k ) ) = { ( p ` k ) } , { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( ( iEdg ` g ) ` ( f ` k ) ) ) ) } )
4 fveq2 
 |-  ( g = G -> ( iEdg ` g ) = ( iEdg ` G ) )
5 4 2 eqtr4di 
 |-  ( g = G -> ( iEdg ` g ) = I )
6 5 dmeqd 
 |-  ( g = G -> dom ( iEdg ` g ) = dom I )
7 wrdeq 
 |-  ( dom ( iEdg ` g ) = dom I -> Word dom ( iEdg ` g ) = Word dom I )
8 6 7 syl 
 |-  ( g = G -> Word dom ( iEdg ` g ) = Word dom I )
9 8 eleq2d 
 |-  ( g = G -> ( f e. Word dom ( iEdg ` g ) <-> f e. Word dom I ) )
10 fveq2 
 |-  ( g = G -> ( Vtx ` g ) = ( Vtx ` G ) )
11 10 1 eqtr4di 
 |-  ( g = G -> ( Vtx ` g ) = V )
12 11 feq3d 
 |-  ( g = G -> ( p : ( 0 ... ( # ` f ) ) --> ( Vtx ` g ) <-> p : ( 0 ... ( # ` f ) ) --> V ) )
13 5 fveq1d 
 |-  ( g = G -> ( ( iEdg ` g ) ` ( f ` k ) ) = ( I ` ( f ` k ) ) )
14 13 eqeq1d 
 |-  ( g = G -> ( ( ( iEdg ` g ) ` ( f ` k ) ) = { ( p ` k ) } <-> ( I ` ( f ` k ) ) = { ( p ` k ) } ) )
15 13 sseq2d 
 |-  ( g = G -> ( { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( ( iEdg ` g ) ` ( f ` k ) ) <-> { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( I ` ( f ` k ) ) ) )
16 14 15 ifpbi23d 
 |-  ( g = G -> ( if- ( ( p ` k ) = ( p ` ( k + 1 ) ) , ( ( iEdg ` g ) ` ( f ` k ) ) = { ( p ` k ) } , { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( ( iEdg ` g ) ` ( f ` k ) ) ) <-> if- ( ( p ` k ) = ( p ` ( k + 1 ) ) , ( I ` ( f ` k ) ) = { ( p ` k ) } , { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( I ` ( f ` k ) ) ) ) )
17 16 ralbidv 
 |-  ( g = G -> ( A. k e. ( 0 ..^ ( # ` f ) ) if- ( ( p ` k ) = ( p ` ( k + 1 ) ) , ( ( iEdg ` g ) ` ( f ` k ) ) = { ( p ` k ) } , { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( ( iEdg ` g ) ` ( 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 ) ) ) ) )
18 9 12 17 3anbi123d 
 |-  ( g = G -> ( ( f e. Word dom ( iEdg ` g ) /\ p : ( 0 ... ( # ` f ) ) --> ( Vtx ` g ) /\ A. k e. ( 0 ..^ ( # ` f ) ) if- ( ( p ` k ) = ( p ` ( k + 1 ) ) , ( ( iEdg ` g ) ` ( f ` k ) ) = { ( p ` k ) } , { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( ( iEdg ` g ) ` ( 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 ) ) ) ) ) )
19 18 opabbidv 
 |-  ( g = G -> { <. f , p >. | ( f e. Word dom ( iEdg ` g ) /\ p : ( 0 ... ( # ` f ) ) --> ( Vtx ` g ) /\ A. k e. ( 0 ..^ ( # ` f ) ) if- ( ( p ` k ) = ( p ` ( k + 1 ) ) , ( ( iEdg ` g ) ` ( f ` k ) ) = { ( p ` k ) } , { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( ( iEdg ` g ) ` ( f ` k ) ) ) ) } = { <. 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 ) ) ) ) } )
20 elex 
 |-  ( G e. W -> G e. _V )
21 3anass 
 |-  ( ( 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 ) ) ) ) ) )
22 21 opabbii 
 |-  { <. 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 , 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 ) ) ) ) ) }
23 2 fvexi 
 |-  I e. _V
24 23 dmex 
 |-  dom I e. _V
25 wrdexg 
 |-  ( dom I e. _V -> Word dom I e. _V )
26 24 25 mp1i 
 |-  ( G e. W -> Word dom I e. _V )
27 ovex 
 |-  ( 0 ... ( # ` f ) ) e. _V
28 1 fvexi 
 |-  V e. _V
29 28 a1i 
 |-  ( ( G e. W /\ f e. Word dom I ) -> V e. _V )
30 mapex 
 |-  ( ( ( 0 ... ( # ` f ) ) e. _V /\ V e. _V ) -> { p | p : ( 0 ... ( # ` f ) ) --> V } e. _V )
31 27 29 30 sylancr 
 |-  ( ( G e. W /\ f e. Word dom I ) -> { p | p : ( 0 ... ( # ` f ) ) --> V } e. _V )
32 simpl 
 |-  ( ( 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 ) ) ) ) -> p : ( 0 ... ( # ` f ) ) --> V )
33 32 ss2abi 
 |-  { p | ( 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 ) ) ) ) } C_ { p | p : ( 0 ... ( # ` f ) ) --> V }
34 33 a1i 
 |-  ( ( G e. W /\ f e. Word dom I ) -> { p | ( 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 ) ) ) ) } C_ { p | p : ( 0 ... ( # ` f ) ) --> V } )
35 31 34 ssexd 
 |-  ( ( G e. W /\ f e. Word dom I ) -> { p | ( 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 ) ) ) ) } e. _V )
36 26 35 opabex3d 
 |-  ( G e. W -> { <. 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 ) ) ) ) ) } e. _V )
37 22 36 eqeltrid 
 |-  ( G e. W -> { <. 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 ) ) ) ) } e. _V )
38 3 19 20 37 fvmptd3 
 |-  ( 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 ) ) ) ) } )