| Step |
Hyp |
Ref |
Expression |
| 1 |
|
trlf1.i |
|- I = ( iEdg ` G ) |
| 2 |
|
istrl |
|- ( F ( Trails ` G ) P <-> ( F ( Walks ` G ) P /\ Fun `' F ) ) |
| 3 |
1
|
wlkf |
|- ( F ( Walks ` G ) P -> F e. Word dom I ) |
| 4 |
|
wrdf |
|- ( F e. Word dom I -> F : ( 0 ..^ ( # ` F ) ) --> dom I ) |
| 5 |
|
df-f1 |
|- ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I <-> ( F : ( 0 ..^ ( # ` F ) ) --> dom I /\ Fun `' F ) ) |
| 6 |
5
|
simplbi2 |
|- ( F : ( 0 ..^ ( # ` F ) ) --> dom I -> ( Fun `' F -> F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I ) ) |
| 7 |
3 4 6
|
3syl |
|- ( F ( Walks ` G ) P -> ( Fun `' F -> F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I ) ) |
| 8 |
7
|
imp |
|- ( ( F ( Walks ` G ) P /\ Fun `' F ) -> F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I ) |
| 9 |
2 8
|
sylbi |
|- ( F ( Trails ` G ) P -> F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I ) |