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