| 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 |
|
upgrimtrls.t |
|- ( ph -> F ( Trails ` G ) P ) |
| 8 |
|
uspgruhgr |
|- ( G e. USPGraph -> G e. UHGraph ) |
| 9 |
3 8
|
syl |
|- ( ph -> G e. UHGraph ) |
| 10 |
|
uspgruhgr |
|- ( H e. USPGraph -> H e. UHGraph ) |
| 11 |
4 10
|
syl |
|- ( ph -> H e. UHGraph ) |
| 12 |
9 11
|
jca |
|- ( ph -> ( G e. UHGraph /\ H e. UHGraph ) ) |
| 13 |
12
|
adantr |
|- ( ( ph /\ X e. dom F ) -> ( G e. UHGraph /\ H e. UHGraph ) ) |
| 14 |
5
|
adantr |
|- ( ( ph /\ X e. dom F ) -> N e. ( G GraphIso H ) ) |
| 15 |
1
|
uhgrfun |
|- ( G e. UHGraph -> Fun I ) |
| 16 |
9 15
|
syl |
|- ( ph -> Fun I ) |
| 17 |
|
trliswlk |
|- ( F ( Trails ` G ) P -> F ( Walks ` G ) P ) |
| 18 |
1
|
wlkf |
|- ( F ( Walks ` G ) P -> F e. Word dom I ) |
| 19 |
|
wrdf |
|- ( F e. Word dom I -> F : ( 0 ..^ ( # ` F ) ) --> dom I ) |
| 20 |
19
|
ffdmd |
|- ( F e. Word dom I -> F : dom F --> dom I ) |
| 21 |
18 20
|
syl |
|- ( F ( Walks ` G ) P -> F : dom F --> dom I ) |
| 22 |
7 17 21
|
3syl |
|- ( ph -> F : dom F --> dom I ) |
| 23 |
22
|
ffvelcdmda |
|- ( ( ph /\ X e. dom F ) -> ( F ` X ) e. dom I ) |
| 24 |
1
|
iedgedg |
|- ( ( Fun I /\ ( F ` X ) e. dom I ) -> ( I ` ( F ` X ) ) e. ( Edg ` G ) ) |
| 25 |
16 23 24
|
syl2an2r |
|- ( ( ph /\ X e. dom F ) -> ( I ` ( F ` X ) ) e. ( Edg ` G ) ) |
| 26 |
|
eqid |
|- ( Edg ` G ) = ( Edg ` G ) |
| 27 |
|
eqid |
|- ( Edg ` H ) = ( Edg ` H ) |
| 28 |
26 27
|
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 ) ) |
| 29 |
13 14 25 28
|
syl12anc |
|- ( ( ph /\ X e. dom F ) -> ( N " ( I ` ( F ` X ) ) ) e. ( Edg ` H ) ) |