| 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 |
|
fvexd |
|- ( ( ph /\ x e. dom F ) -> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) e. _V ) |
| 9 |
8
|
ralrimiva |
|- ( ph -> A. x e. dom F ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) e. _V ) |
| 10 |
|
eqid |
|- ( x e. dom F |-> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) ) = ( x e. dom F |-> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) ) |
| 11 |
10
|
fnmpt |
|- ( A. x e. dom F ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) e. _V -> ( x e. dom F |-> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) ) Fn dom F ) |
| 12 |
9 11
|
syl |
|- ( ph -> ( x e. dom F |-> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) ) Fn dom F ) |
| 13 |
6
|
fneq1i |
|- ( E Fn dom F <-> ( x e. dom F |-> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) ) Fn dom F ) |
| 14 |
12 13
|
sylibr |
|- ( ph -> E Fn dom F ) |
| 15 |
|
hashfn |
|- ( E Fn dom F -> ( # ` E ) = ( # ` dom F ) ) |
| 16 |
14 15
|
syl |
|- ( ph -> ( # ` E ) = ( # ` dom F ) ) |
| 17 |
|
wrdf |
|- ( F e. Word dom I -> F : ( 0 ..^ ( # ` F ) ) --> dom I ) |
| 18 |
|
ffun |
|- ( F : ( 0 ..^ ( # ` F ) ) --> dom I -> Fun F ) |
| 19 |
7 17 18
|
3syl |
|- ( ph -> Fun F ) |
| 20 |
19
|
funfnd |
|- ( ph -> F Fn dom F ) |
| 21 |
|
hashfn |
|- ( F Fn dom F -> ( # ` F ) = ( # ` dom F ) ) |
| 22 |
20 21
|
syl |
|- ( ph -> ( # ` F ) = ( # ` dom F ) ) |
| 23 |
16 22
|
eqtr4d |
|- ( ph -> ( # ` E ) = ( # ` F ) ) |