| Step |
Hyp |
Ref |
Expression |
| 1 |
|
eqid |
|- ( iEdg ` G ) = ( iEdg ` G ) |
| 2 |
1
|
wlkf |
|- ( F ( Walks ` G ) P -> F e. Word dom ( iEdg ` G ) ) |
| 3 |
|
wrdl1exs1 |
|- ( ( F e. Word dom ( iEdg ` G ) /\ ( # ` F ) = 1 ) -> E. i e. dom ( iEdg ` G ) F = <" i "> ) |
| 4 |
|
funcnvs1 |
|- Fun `' <" i "> |
| 5 |
|
cnveq |
|- ( F = <" i "> -> `' F = `' <" i "> ) |
| 6 |
5
|
funeqd |
|- ( F = <" i "> -> ( Fun `' F <-> Fun `' <" i "> ) ) |
| 7 |
4 6
|
mpbiri |
|- ( F = <" i "> -> Fun `' F ) |
| 8 |
7
|
rexlimivw |
|- ( E. i e. dom ( iEdg ` G ) F = <" i "> -> Fun `' F ) |
| 9 |
3 8
|
syl |
|- ( ( F e. Word dom ( iEdg ` G ) /\ ( # ` F ) = 1 ) -> Fun `' F ) |
| 10 |
2 9
|
sylan |
|- ( ( F ( Walks ` G ) P /\ ( # ` F ) = 1 ) -> Fun `' F ) |