Step |
Hyp |
Ref |
Expression |
1 |
|
0wlk.v |
|- V = ( Vtx ` G ) |
2 |
1
|
0wlk |
|- ( G e. U -> ( (/) ( Walks ` G ) P <-> P : ( 0 ... 0 ) --> V ) ) |
3 |
2
|
anbi1d |
|- ( G e. U -> ( ( (/) ( Walks ` G ) P /\ Fun `' (/) ) <-> ( P : ( 0 ... 0 ) --> V /\ Fun `' (/) ) ) ) |
4 |
|
istrl |
|- ( (/) ( Trails ` G ) P <-> ( (/) ( Walks ` G ) P /\ Fun `' (/) ) ) |
5 |
|
funcnv0 |
|- Fun `' (/) |
6 |
5
|
biantru |
|- ( P : ( 0 ... 0 ) --> V <-> ( P : ( 0 ... 0 ) --> V /\ Fun `' (/) ) ) |
7 |
3 4 6
|
3bitr4g |
|- ( G e. U -> ( (/) ( Trails ` G ) P <-> P : ( 0 ... 0 ) --> V ) ) |