Metamath Proof Explorer


Theorem wksv

Description: The class of walks is a set. (Contributed by AV, 15-Jan-2021)

Ref Expression
Assertion wksv
|- { <. f , p >. | f ( Walks ` G ) p } e. _V

Proof

Step Hyp Ref Expression
1 fvex
 |-  ( Vtx ` G ) e. _V
2 fvex
 |-  ( iEdg ` G ) e. _V
3 2 dmex
 |-  dom ( iEdg ` G ) e. _V
4 wrdexg
 |-  ( dom ( iEdg ` G ) e. _V -> Word dom ( iEdg ` G ) e. _V )
5 3 4 mp1i
 |-  ( ( Vtx ` G ) e. _V -> Word dom ( iEdg ` G ) e. _V )
6 wrdexg
 |-  ( ( Vtx ` G ) e. _V -> Word ( Vtx ` G ) e. _V )
7 eqid
 |-  ( iEdg ` G ) = ( iEdg ` G )
8 7 wlkf
 |-  ( f ( Walks ` G ) p -> f e. Word dom ( iEdg ` G ) )
9 8 adantl
 |-  ( ( ( Vtx ` G ) e. _V /\ f ( Walks ` G ) p ) -> f e. Word dom ( iEdg ` G ) )
10 eqid
 |-  ( Vtx ` G ) = ( Vtx ` G )
11 10 wlkpwrd
 |-  ( f ( Walks ` G ) p -> p e. Word ( Vtx ` G ) )
12 11 adantl
 |-  ( ( ( Vtx ` G ) e. _V /\ f ( Walks ` G ) p ) -> p e. Word ( Vtx ` G ) )
13 5 6 9 12 opabex2
 |-  ( ( Vtx ` G ) e. _V -> { <. f , p >. | f ( Walks ` G ) p } e. _V )
14 1 13 ax-mp
 |-  { <. f , p >. | f ( Walks ` G ) p } e. _V