| 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 |
|
upgrimwlk.f |
|- ( ph -> F e. Word dom I ) |
| 8 |
|
upgrimwlklem.p |
|- ( ph -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) |
| 9 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
| 10 |
|
eqid |
|- ( Vtx ` H ) = ( Vtx ` H ) |
| 11 |
9 10
|
grimf1o |
|- ( N e. ( G GraphIso H ) -> N : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) |
| 12 |
|
f1of |
|- ( N : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) -> N : ( Vtx ` G ) --> ( Vtx ` H ) ) |
| 13 |
5 11 12
|
3syl |
|- ( ph -> N : ( Vtx ` G ) --> ( Vtx ` H ) ) |
| 14 |
1 2 3 4 5 6 7
|
upgrimwlklem1 |
|- ( ph -> ( # ` E ) = ( # ` F ) ) |
| 15 |
14
|
oveq2d |
|- ( ph -> ( 0 ... ( # ` E ) ) = ( 0 ... ( # ` F ) ) ) |
| 16 |
15
|
feq2d |
|- ( ph -> ( P : ( 0 ... ( # ` E ) ) --> ( Vtx ` G ) <-> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) ) |
| 17 |
8 16
|
mpbird |
|- ( ph -> P : ( 0 ... ( # ` E ) ) --> ( Vtx ` G ) ) |
| 18 |
13 17
|
fcod |
|- ( ph -> ( N o. P ) : ( 0 ... ( # ` E ) ) --> ( Vtx ` H ) ) |