| Step |
Hyp |
Ref |
Expression |
| 1 |
|
trlsegvdeg.v |
|- V = ( Vtx ` G ) |
| 2 |
|
trlsegvdeg.i |
|- I = ( iEdg ` G ) |
| 3 |
|
trlsegvdeg.f |
|- ( ph -> Fun I ) |
| 4 |
|
trlsegvdeg.n |
|- ( ph -> N e. ( 0 ..^ ( # ` F ) ) ) |
| 5 |
|
trlsegvdeg.u |
|- ( ph -> U e. V ) |
| 6 |
|
trlsegvdeg.w |
|- ( ph -> F ( Trails ` G ) P ) |
| 7 |
|
trlsegvdeg.vx |
|- ( ph -> ( Vtx ` X ) = V ) |
| 8 |
|
trlsegvdeg.vy |
|- ( ph -> ( Vtx ` Y ) = V ) |
| 9 |
|
trlsegvdeg.vz |
|- ( ph -> ( Vtx ` Z ) = V ) |
| 10 |
|
trlsegvdeg.ix |
|- ( ph -> ( iEdg ` X ) = ( I |` ( F " ( 0 ..^ N ) ) ) ) |
| 11 |
|
trlsegvdeg.iy |
|- ( ph -> ( iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } ) |
| 12 |
|
trlsegvdeg.iz |
|- ( ph -> ( iEdg ` Z ) = ( I |` ( F " ( 0 ... N ) ) ) ) |
| 13 |
1 2 3 4 5 6 7 8 9 10 11 12
|
trlsegvdeglem4 |
|- ( ph -> dom ( iEdg ` X ) = ( ( F " ( 0 ..^ N ) ) i^i dom I ) ) |
| 14 |
2
|
trlf1 |
|- ( F ( Trails ` G ) P -> F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I ) |
| 15 |
|
f1fun |
|- ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I -> Fun F ) |
| 16 |
6 14 15
|
3syl |
|- ( ph -> Fun F ) |
| 17 |
|
fzofi |
|- ( 0 ..^ N ) e. Fin |
| 18 |
|
imafi |
|- ( ( Fun F /\ ( 0 ..^ N ) e. Fin ) -> ( F " ( 0 ..^ N ) ) e. Fin ) |
| 19 |
16 17 18
|
sylancl |
|- ( ph -> ( F " ( 0 ..^ N ) ) e. Fin ) |
| 20 |
|
infi |
|- ( ( F " ( 0 ..^ N ) ) e. Fin -> ( ( F " ( 0 ..^ N ) ) i^i dom I ) e. Fin ) |
| 21 |
19 20
|
syl |
|- ( ph -> ( ( F " ( 0 ..^ N ) ) i^i dom I ) e. Fin ) |
| 22 |
13 21
|
eqeltrd |
|- ( ph -> dom ( iEdg ` X ) e. Fin ) |