Metamath Proof Explorer

Theorem upwlksfval

Description: The set of simple walks (in an undirected graph). (Contributed by Alexander van der Vekens, 19-Oct-2017) (Revised by AV, 28-Dec-2020)

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

Proof

Step Hyp Ref Expression
1 upwlksfval.v 
 |-  V = ( Vtx ` G )
2 upwlksfval.i 
 |-  I = ( iEdg ` G )
3 df-upwlks 
 |-  UPWalks = ( g e. _V |-> { <. f , p >. | ( f e. Word dom ( iEdg ` g ) /\ p : ( 0 ... ( # ` f ) ) --> ( Vtx ` g ) /\ A. k e. ( 0 ..^ ( # ` f ) ) ( ( iEdg ` g ) ` ( f ` k ) ) = { ( p ` k ) , ( p ` ( k + 1 ) ) } ) } )
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 ) , ( p ` ( k + 1 ) ) } <-> ( I ` ( f ` k ) ) = { ( p ` k ) , ( p ` ( k + 1 ) ) } ) )
15 14 ralbidv 
 |-  ( g = G -> ( A. k e. ( 0 ..^ ( # ` f ) ) ( ( iEdg ` g ) ` ( f ` k ) ) = { ( p ` k ) , ( p ` ( k + 1 ) ) } <-> A. k e. ( 0 ..^ ( # ` f ) ) ( I ` ( f ` k ) ) = { ( p ` k ) , ( p ` ( k + 1 ) ) } ) )
16 9 12 15 3anbi123d 
 |-  ( g = G -> ( ( f e. Word dom ( iEdg ` g ) /\ p : ( 0 ... ( # ` f ) ) --> ( Vtx ` g ) /\ A. k e. ( 0 ..^ ( # ` f ) ) ( ( iEdg ` g ) ` ( 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 ) ) } ) ) )
17 16 opabbidv 
 |-  ( g = G -> { <. f , p >. | ( f e. Word dom ( iEdg ` g ) /\ p : ( 0 ... ( # ` f ) ) --> ( Vtx ` g ) /\ A. k e. ( 0 ..^ ( # ` f ) ) ( ( iEdg ` g ) ` ( f ` k ) ) = { ( p ` k ) , ( p ` ( k + 1 ) ) } ) } = { <. f , p >. | ( f e. Word dom I /\ p : ( 0 ... ( # ` f ) ) --> V /\ A. k e. ( 0 ..^ ( # ` f ) ) ( I ` ( f ` k ) ) = { ( p ` k ) , ( p ` ( k + 1 ) ) } ) } )
18 elex 
 |-  ( G e. W -> G e. _V )
19 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 ) ) } ) ) )
20 19 opabbii 
 |-  { <. 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 , p >. | ( f e. Word dom I /\ ( p : ( 0 ... ( # ` f ) ) --> V /\ A. k e. ( 0 ..^ ( # ` f ) ) ( I ` ( f ` k ) ) = { ( p ` k ) , ( p ` ( k + 1 ) ) } ) ) }
21 2 fvexi 
 |-  I e. _V
22 21 dmex 
 |-  dom I e. _V
23 wrdexg 
 |-  ( dom I e. _V -> Word dom I e. _V )
24 22 23 mp1i 
 |-  ( G e. W -> Word dom I e. _V )
25 ovex 
 |-  ( 0 ... ( # ` f ) ) e. _V
26 1 fvexi 
 |-  V e. _V
27 26 a1i 
 |-  ( ( G e. W /\ f e. Word dom I ) -> V e. _V )
28 mapex 
 |-  ( ( ( 0 ... ( # ` f ) ) e. _V /\ V e. _V ) -> { p | p : ( 0 ... ( # ` f ) ) --> V } e. _V )
29 25 27 28 sylancr 
 |-  ( ( G e. W /\ f e. Word dom I ) -> { p | p : ( 0 ... ( # ` f ) ) --> V } e. _V )
30 simpl 
 |-  ( ( p : ( 0 ... ( # ` f ) ) --> V /\ A. k e. ( 0 ..^ ( # ` f ) ) ( I ` ( f ` k ) ) = { ( p ` k ) , ( p ` ( k + 1 ) ) } ) -> p : ( 0 ... ( # ` f ) ) --> V )
31 30 ss2abi 
 |-  { p | ( p : ( 0 ... ( # ` f ) ) --> V /\ A. k e. ( 0 ..^ ( # ` f ) ) ( I ` ( f ` k ) ) = { ( p ` k ) , ( p ` ( k + 1 ) ) } ) } C_ { p | p : ( 0 ... ( # ` f ) ) --> V }
32 31 a1i 
 |-  ( ( G e. W /\ f e. Word dom I ) -> { p | ( p : ( 0 ... ( # ` f ) ) --> V /\ A. k e. ( 0 ..^ ( # ` f ) ) ( I ` ( f ` k ) ) = { ( p ` k ) , ( p ` ( k + 1 ) ) } ) } C_ { p | p : ( 0 ... ( # ` f ) ) --> V } )
33 29 32 ssexd 
 |-  ( ( G e. W /\ f e. Word dom I ) -> { p | ( p : ( 0 ... ( # ` f ) ) --> V /\ A. k e. ( 0 ..^ ( # ` f ) ) ( I ` ( f ` k ) ) = { ( p ` k ) , ( p ` ( k + 1 ) ) } ) } e. _V )
34 24 33 opabex3d 
 |-  ( G e. W -> { <. f , p >. | ( f e. Word dom I /\ ( p : ( 0 ... ( # ` f ) ) --> V /\ A. k e. ( 0 ..^ ( # ` f ) ) ( I ` ( f ` k ) ) = { ( p ` k ) , ( p ` ( k + 1 ) ) } ) ) } e. _V )
35 20 34 eqeltrid 
 |-  ( G e. W -> { <. f , p >. | ( f e. Word dom I /\ p : ( 0 ... ( # ` f ) ) --> V /\ A. k e. ( 0 ..^ ( # ` f ) ) ( I ` ( f ` k ) ) = { ( p ` k ) , ( p ` ( k + 1 ) ) } ) } e. _V )
36 3 17 18 35 fvmptd3 
 |-  ( 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 ) ) } ) } )