| 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 |
6
|
a1i |
|- ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> E = ( x e. dom F |-> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) ) ) |
| 9 |
|
2fveq3 |
|- ( x = X -> ( I ` ( F ` x ) ) = ( I ` ( F ` X ) ) ) |
| 10 |
9
|
imaeq2d |
|- ( x = X -> ( N " ( I ` ( F ` x ) ) ) = ( N " ( I ` ( F ` X ) ) ) ) |
| 11 |
10
|
fveq2d |
|- ( x = X -> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) = ( `' J ` ( N " ( I ` ( F ` X ) ) ) ) ) |
| 12 |
11
|
adantl |
|- ( ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) /\ x = X ) -> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) = ( `' J ` ( N " ( I ` ( F ` X ) ) ) ) ) |
| 13 |
1 2 3 4 5 6 7
|
upgrimwlklem1 |
|- ( ph -> ( # ` E ) = ( # ` F ) ) |
| 14 |
13
|
oveq2d |
|- ( ph -> ( 0 ..^ ( # ` E ) ) = ( 0 ..^ ( # ` F ) ) ) |
| 15 |
|
wrdf |
|- ( F e. Word dom I -> F : ( 0 ..^ ( # ` F ) ) --> dom I ) |
| 16 |
|
fdm |
|- ( F : ( 0 ..^ ( # ` F ) ) --> dom I -> dom F = ( 0 ..^ ( # ` F ) ) ) |
| 17 |
16
|
eqcomd |
|- ( F : ( 0 ..^ ( # ` F ) ) --> dom I -> ( 0 ..^ ( # ` F ) ) = dom F ) |
| 18 |
15 17
|
syl |
|- ( F e. Word dom I -> ( 0 ..^ ( # ` F ) ) = dom F ) |
| 19 |
7 18
|
syl |
|- ( ph -> ( 0 ..^ ( # ` F ) ) = dom F ) |
| 20 |
14 19
|
eqtrd |
|- ( ph -> ( 0 ..^ ( # ` E ) ) = dom F ) |
| 21 |
20
|
eleq2d |
|- ( ph -> ( X e. ( 0 ..^ ( # ` E ) ) <-> X e. dom F ) ) |
| 22 |
21
|
biimpa |
|- ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> X e. dom F ) |
| 23 |
|
fvexd |
|- ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> ( `' J ` ( N " ( I ` ( F ` X ) ) ) ) e. _V ) |
| 24 |
8 12 22 23
|
fvmptd |
|- ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> ( E ` X ) = ( `' J ` ( N " ( I ` ( F ` X ) ) ) ) ) |
| 25 |
24
|
fveq2d |
|- ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> ( J ` ( E ` X ) ) = ( J ` ( `' J ` ( N " ( I ` ( F ` X ) ) ) ) ) ) |
| 26 |
4
|
adantr |
|- ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> H e. USPGraph ) |
| 27 |
2
|
uspgrf1oedg |
|- ( H e. USPGraph -> J : dom J -1-1-onto-> ( Edg ` H ) ) |
| 28 |
26 27
|
syl |
|- ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> J : dom J -1-1-onto-> ( Edg ` H ) ) |
| 29 |
|
uspgruhgr |
|- ( G e. USPGraph -> G e. UHGraph ) |
| 30 |
3 29
|
syl |
|- ( ph -> G e. UHGraph ) |
| 31 |
|
uspgruhgr |
|- ( H e. USPGraph -> H e. UHGraph ) |
| 32 |
4 31
|
syl |
|- ( ph -> H e. UHGraph ) |
| 33 |
30 32
|
jca |
|- ( ph -> ( G e. UHGraph /\ H e. UHGraph ) ) |
| 34 |
33
|
adantr |
|- ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> ( G e. UHGraph /\ H e. UHGraph ) ) |
| 35 |
5
|
adantr |
|- ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> N e. ( G GraphIso H ) ) |
| 36 |
1
|
uhgrfun |
|- ( G e. UHGraph -> Fun I ) |
| 37 |
30 36
|
syl |
|- ( ph -> Fun I ) |
| 38 |
37
|
adantr |
|- ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> Fun I ) |
| 39 |
13 7
|
wrdfd |
|- ( ph -> F : ( 0 ..^ ( # ` E ) ) --> dom I ) |
| 40 |
39
|
ffvelcdmda |
|- ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> ( F ` X ) e. dom I ) |
| 41 |
1
|
iedgedg |
|- ( ( Fun I /\ ( F ` X ) e. dom I ) -> ( I ` ( F ` X ) ) e. ( Edg ` G ) ) |
| 42 |
38 40 41
|
syl2anc |
|- ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> ( I ` ( F ` X ) ) e. ( Edg ` G ) ) |
| 43 |
|
eqid |
|- ( Edg ` G ) = ( Edg ` G ) |
| 44 |
|
eqid |
|- ( Edg ` H ) = ( Edg ` H ) |
| 45 |
43 44
|
uhgrimedgi |
|- ( ( ( G e. UHGraph /\ H e. UHGraph ) /\ ( N e. ( G GraphIso H ) /\ ( I ` ( F ` X ) ) e. ( Edg ` G ) ) ) -> ( N " ( I ` ( F ` X ) ) ) e. ( Edg ` H ) ) |
| 46 |
34 35 42 45
|
syl12anc |
|- ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> ( N " ( I ` ( F ` X ) ) ) e. ( Edg ` H ) ) |
| 47 |
|
f1ocnvfv2 |
|- ( ( J : dom J -1-1-onto-> ( Edg ` H ) /\ ( N " ( I ` ( F ` X ) ) ) e. ( Edg ` H ) ) -> ( J ` ( `' J ` ( N " ( I ` ( F ` X ) ) ) ) ) = ( N " ( I ` ( F ` X ) ) ) ) |
| 48 |
28 46 47
|
syl2anc |
|- ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> ( J ` ( `' J ` ( N " ( I ` ( F ` X ) ) ) ) ) = ( N " ( I ` ( F ` X ) ) ) ) |
| 49 |
25 48
|
eqtrd |
|- ( ( ph /\ X e. ( 0 ..^ ( # ` E ) ) ) -> ( J ` ( E ` X ) ) = ( N " ( I ` ( F ` X ) ) ) ) |