| Step |
Hyp |
Ref |
Expression |
| 1 |
|
upgrimwlk.i |
|- I = ( iEdg ` G ) |
| 2 |
|
upgrimwlk.j |
|- J = ( iEdg ` H ) |
| 3 |
|
upgrimwlk.g |
|- ( ph -> G e. USPGraph ) |
| 4 |
|
upgrimwlk.h |
|- ( ph -> H e. USPGraph ) |
| 5 |
|
upgrimwlk.n |
|- ( ph -> N e. ( G GraphIso H ) ) |
| 6 |
|
upgrimwlk.e |
|- E = ( x e. dom F |-> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) ) |
| 7 |
|
upgrimspths.s |
|- ( ph -> F ( SPaths ` G ) P ) |
| 8 |
|
spthispth |
|- ( F ( SPaths ` G ) P -> F ( Paths ` G ) P ) |
| 9 |
|
pthistrl |
|- ( F ( Paths ` G ) P -> F ( Trails ` G ) P ) |
| 10 |
7 8 9
|
3syl |
|- ( ph -> F ( Trails ` G ) P ) |
| 11 |
1 2 3 4 5 6 10
|
upgrimtrls |
|- ( ph -> E ( Trails ` H ) ( N o. P ) ) |
| 12 |
|
isspth |
|- ( F ( SPaths ` G ) P <-> ( F ( Trails ` G ) P /\ Fun `' P ) ) |
| 13 |
12
|
simprbi |
|- ( F ( SPaths ` G ) P -> Fun `' P ) |
| 14 |
7 13
|
syl |
|- ( ph -> Fun `' P ) |
| 15 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
| 16 |
|
eqid |
|- ( Vtx ` H ) = ( Vtx ` H ) |
| 17 |
15 16
|
grimf1o |
|- ( N e. ( G GraphIso H ) -> N : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) |
| 18 |
|
dff1o3 |
|- ( N : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) <-> ( N : ( Vtx ` G ) -onto-> ( Vtx ` H ) /\ Fun `' N ) ) |
| 19 |
18
|
simprbi |
|- ( N : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) -> Fun `' N ) |
| 20 |
5 17 19
|
3syl |
|- ( ph -> Fun `' N ) |
| 21 |
|
funco |
|- ( ( Fun `' P /\ Fun `' N ) -> Fun ( `' P o. `' N ) ) |
| 22 |
14 20 21
|
syl2anc |
|- ( ph -> Fun ( `' P o. `' N ) ) |
| 23 |
|
cnvco |
|- `' ( N o. P ) = ( `' P o. `' N ) |
| 24 |
23
|
funeqi |
|- ( Fun `' ( N o. P ) <-> Fun ( `' P o. `' N ) ) |
| 25 |
22 24
|
sylibr |
|- ( ph -> Fun `' ( N o. P ) ) |
| 26 |
|
isspth |
|- ( E ( SPaths ` H ) ( N o. P ) <-> ( E ( Trails ` H ) ( N o. P ) /\ Fun `' ( N o. P ) ) ) |
| 27 |
11 25 26
|
sylanbrc |
|- ( ph -> E ( SPaths ` H ) ( N o. P ) ) |