Step |
Hyp |
Ref |
Expression |
1 |
|
0pth.v |
|- V = ( Vtx ` G ) |
2 |
1
|
0trl |
|- ( G e. W -> ( (/) ( Trails ` G ) P <-> P : ( 0 ... 0 ) --> V ) ) |
3 |
2
|
anbi1d |
|- ( G e. W -> ( ( (/) ( Trails ` G ) P /\ Fun `' P ) <-> ( P : ( 0 ... 0 ) --> V /\ Fun `' P ) ) ) |
4 |
|
isspth |
|- ( (/) ( SPaths ` G ) P <-> ( (/) ( Trails ` G ) P /\ Fun `' P ) ) |
5 |
|
fz0sn |
|- ( 0 ... 0 ) = { 0 } |
6 |
5
|
feq2i |
|- ( P : ( 0 ... 0 ) --> V <-> P : { 0 } --> V ) |
7 |
|
c0ex |
|- 0 e. _V |
8 |
7
|
fsn2 |
|- ( P : { 0 } --> V <-> ( ( P ` 0 ) e. V /\ P = { <. 0 , ( P ` 0 ) >. } ) ) |
9 |
|
funcnvsn |
|- Fun `' { <. 0 , ( P ` 0 ) >. } |
10 |
|
cnveq |
|- ( P = { <. 0 , ( P ` 0 ) >. } -> `' P = `' { <. 0 , ( P ` 0 ) >. } ) |
11 |
10
|
funeqd |
|- ( P = { <. 0 , ( P ` 0 ) >. } -> ( Fun `' P <-> Fun `' { <. 0 , ( P ` 0 ) >. } ) ) |
12 |
9 11
|
mpbiri |
|- ( P = { <. 0 , ( P ` 0 ) >. } -> Fun `' P ) |
13 |
8 12
|
simplbiim |
|- ( P : { 0 } --> V -> Fun `' P ) |
14 |
6 13
|
sylbi |
|- ( P : ( 0 ... 0 ) --> V -> Fun `' P ) |
15 |
14
|
pm4.71i |
|- ( P : ( 0 ... 0 ) --> V <-> ( P : ( 0 ... 0 ) --> V /\ Fun `' P ) ) |
16 |
3 4 15
|
3bitr4g |
|- ( G e. W -> ( (/) ( SPaths ` G ) P <-> P : ( 0 ... 0 ) --> V ) ) |