Description: Restrictions of walks (i.e. special kinds of walks, for example paths - see pthsfval ) are sets. (Contributed by Alexander van der Vekens, 1-Nov-2017) (Revised by AV, 30-Dec-2020) (Proof shortened by AV, 15-Jan-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | wlkRes.1 | |- ( f ( W ` G ) p -> f ( Walks ` G ) p ) |
|
| Assertion | wlkRes | |- { <. f , p >. | ( f ( W ` G ) p /\ ph ) } e. _V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wlkRes.1 | |- ( f ( W ` G ) p -> f ( Walks ` G ) p ) |
|
| 2 | 1 | gen2 | |- A. f A. p ( f ( W ` G ) p -> f ( Walks ` G ) p ) |
| 3 | wksv | |- { <. f , p >. | f ( Walks ` G ) p } e. _V |
|
| 4 | opabbrex | |- ( ( A. f A. p ( f ( W ` G ) p -> f ( Walks ` G ) p ) /\ { <. f , p >. | f ( Walks ` G ) p } e. _V ) -> { <. f , p >. | ( f ( W ` G ) p /\ ph ) } e. _V ) |
|
| 5 | 2 3 4 | mp2an | |- { <. f , p >. | ( f ( W ` G ) p /\ ph ) } e. _V |