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 |