| 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 |
2
|
uspgrf1oedg |
|- ( H e. USPGraph -> J : dom J -1-1-onto-> ( Edg ` H ) ) |
| 9 |
|
f1of1 |
|- ( J : dom J -1-1-onto-> ( Edg ` H ) -> J : dom J -1-1-> ( Edg ` H ) ) |
| 10 |
4 8 9
|
3syl |
|- ( ph -> J : dom J -1-1-> ( Edg ` H ) ) |
| 11 |
1 2 3 4 5 6 7
|
upgrimtrlslem1 |
|- ( ( ph /\ x e. dom F ) -> ( N " ( I ` ( F ` x ) ) ) e. ( Edg ` H ) ) |
| 12 |
|
edgval |
|- ( Edg ` H ) = ran ( iEdg ` H ) |
| 13 |
2
|
eqcomi |
|- ( iEdg ` H ) = J |
| 14 |
13
|
rneqi |
|- ran ( iEdg ` H ) = ran J |
| 15 |
12 14
|
eqtri |
|- ( Edg ` H ) = ran J |
| 16 |
11 15
|
eleqtrdi |
|- ( ( ph /\ x e. dom F ) -> ( N " ( I ` ( F ` x ) ) ) e. ran J ) |
| 17 |
1 2 3 4 5 6 7
|
upgrimtrlslem1 |
|- ( ( ph /\ y e. dom F ) -> ( N " ( I ` ( F ` y ) ) ) e. ( Edg ` H ) ) |
| 18 |
17 15
|
eleqtrdi |
|- ( ( ph /\ y e. dom F ) -> ( N " ( I ` ( F ` y ) ) ) e. ran J ) |
| 19 |
16 18
|
anim12dan |
|- ( ( ph /\ ( x e. dom F /\ y e. dom F ) ) -> ( ( N " ( I ` ( F ` x ) ) ) e. ran J /\ ( N " ( I ` ( F ` y ) ) ) e. ran J ) ) |
| 20 |
|
f1ocnvfvrneq |
|- ( ( J : dom J -1-1-> ( Edg ` H ) /\ ( ( N " ( I ` ( F ` x ) ) ) e. ran J /\ ( N " ( I ` ( F ` y ) ) ) e. ran J ) ) -> ( ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) = ( `' J ` ( N " ( I ` ( F ` y ) ) ) ) -> ( N " ( I ` ( F ` x ) ) ) = ( N " ( I ` ( F ` y ) ) ) ) ) |
| 21 |
10 19 20
|
syl2an2r |
|- ( ( ph /\ ( x e. dom F /\ y e. dom F ) ) -> ( ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) = ( `' J ` ( N " ( I ` ( F ` y ) ) ) ) -> ( N " ( I ` ( F ` x ) ) ) = ( N " ( I ` ( F ` y ) ) ) ) ) |
| 22 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
| 23 |
|
eqid |
|- ( Vtx ` H ) = ( Vtx ` H ) |
| 24 |
22 23
|
grimf1o |
|- ( N e. ( G GraphIso H ) -> N : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) |
| 25 |
|
f1of1 |
|- ( N : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) -> N : ( Vtx ` G ) -1-1-> ( Vtx ` H ) ) |
| 26 |
5 24 25
|
3syl |
|- ( ph -> N : ( Vtx ` G ) -1-1-> ( Vtx ` H ) ) |
| 27 |
|
uspgruhgr |
|- ( G e. USPGraph -> G e. UHGraph ) |
| 28 |
3 27
|
syl |
|- ( ph -> G e. UHGraph ) |
| 29 |
|
trliswlk |
|- ( F ( Trails ` G ) P -> F ( Walks ` G ) P ) |
| 30 |
1
|
wlkf |
|- ( F ( Walks ` G ) P -> F e. Word dom I ) |
| 31 |
|
wrdf |
|- ( F e. Word dom I -> F : ( 0 ..^ ( # ` F ) ) --> dom I ) |
| 32 |
|
id |
|- ( F : ( 0 ..^ ( # ` F ) ) --> dom I -> F : ( 0 ..^ ( # ` F ) ) --> dom I ) |
| 33 |
32
|
ffdmd |
|- ( F : ( 0 ..^ ( # ` F ) ) --> dom I -> F : dom F --> dom I ) |
| 34 |
30 31 33
|
3syl |
|- ( F ( Walks ` G ) P -> F : dom F --> dom I ) |
| 35 |
7 29 34
|
3syl |
|- ( ph -> F : dom F --> dom I ) |
| 36 |
35
|
ffvelcdmda |
|- ( ( ph /\ x e. dom F ) -> ( F ` x ) e. dom I ) |
| 37 |
22 1
|
uhgrss |
|- ( ( G e. UHGraph /\ ( F ` x ) e. dom I ) -> ( I ` ( F ` x ) ) C_ ( Vtx ` G ) ) |
| 38 |
28 36 37
|
syl2an2r |
|- ( ( ph /\ x e. dom F ) -> ( I ` ( F ` x ) ) C_ ( Vtx ` G ) ) |
| 39 |
35
|
ffvelcdmda |
|- ( ( ph /\ y e. dom F ) -> ( F ` y ) e. dom I ) |
| 40 |
22 1
|
uhgrss |
|- ( ( G e. UHGraph /\ ( F ` y ) e. dom I ) -> ( I ` ( F ` y ) ) C_ ( Vtx ` G ) ) |
| 41 |
28 39 40
|
syl2an2r |
|- ( ( ph /\ y e. dom F ) -> ( I ` ( F ` y ) ) C_ ( Vtx ` G ) ) |
| 42 |
38 41
|
anim12dan |
|- ( ( ph /\ ( x e. dom F /\ y e. dom F ) ) -> ( ( I ` ( F ` x ) ) C_ ( Vtx ` G ) /\ ( I ` ( F ` y ) ) C_ ( Vtx ` G ) ) ) |
| 43 |
|
f1imaeq |
|- ( ( N : ( Vtx ` G ) -1-1-> ( Vtx ` H ) /\ ( ( I ` ( F ` x ) ) C_ ( Vtx ` G ) /\ ( I ` ( F ` y ) ) C_ ( Vtx ` G ) ) ) -> ( ( N " ( I ` ( F ` x ) ) ) = ( N " ( I ` ( F ` y ) ) ) <-> ( I ` ( F ` x ) ) = ( I ` ( F ` y ) ) ) ) |
| 44 |
26 42 43
|
syl2an2r |
|- ( ( ph /\ ( x e. dom F /\ y e. dom F ) ) -> ( ( N " ( I ` ( F ` x ) ) ) = ( N " ( I ` ( F ` y ) ) ) <-> ( I ` ( F ` x ) ) = ( I ` ( F ` y ) ) ) ) |
| 45 |
1
|
uspgrf1oedg |
|- ( G e. USPGraph -> I : dom I -1-1-onto-> ( Edg ` G ) ) |
| 46 |
|
f1of1 |
|- ( I : dom I -1-1-onto-> ( Edg ` G ) -> I : dom I -1-1-> ( Edg ` G ) ) |
| 47 |
3 45 46
|
3syl |
|- ( ph -> I : dom I -1-1-> ( Edg ` G ) ) |
| 48 |
1
|
trlf1 |
|- ( F ( Trails ` G ) P -> F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I ) |
| 49 |
|
f1f |
|- ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I -> F : ( 0 ..^ ( # ` F ) ) --> dom I ) |
| 50 |
|
fdm |
|- ( F : ( 0 ..^ ( # ` F ) ) --> dom I -> dom F = ( 0 ..^ ( # ` F ) ) ) |
| 51 |
50
|
eqcomd |
|- ( F : ( 0 ..^ ( # ` F ) ) --> dom I -> ( 0 ..^ ( # ` F ) ) = dom F ) |
| 52 |
49 51
|
syl |
|- ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I -> ( 0 ..^ ( # ` F ) ) = dom F ) |
| 53 |
|
f1eq2 |
|- ( ( 0 ..^ ( # ` F ) ) = dom F -> ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I <-> F : dom F -1-1-> dom I ) ) |
| 54 |
53
|
biimpcd |
|- ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I -> ( ( 0 ..^ ( # ` F ) ) = dom F -> F : dom F -1-1-> dom I ) ) |
| 55 |
52 54
|
mpd |
|- ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I -> F : dom F -1-1-> dom I ) |
| 56 |
7 48 55
|
3syl |
|- ( ph -> F : dom F -1-1-> dom I ) |
| 57 |
47 56
|
jca |
|- ( ph -> ( I : dom I -1-1-> ( Edg ` G ) /\ F : dom F -1-1-> dom I ) ) |
| 58 |
|
f1cofveqaeq |
|- ( ( ( I : dom I -1-1-> ( Edg ` G ) /\ F : dom F -1-1-> dom I ) /\ ( x e. dom F /\ y e. dom F ) ) -> ( ( I ` ( F ` x ) ) = ( I ` ( F ` y ) ) -> x = y ) ) |
| 59 |
57 58
|
sylan |
|- ( ( ph /\ ( x e. dom F /\ y e. dom F ) ) -> ( ( I ` ( F ` x ) ) = ( I ` ( F ` y ) ) -> x = y ) ) |
| 60 |
44 59
|
sylbid |
|- ( ( ph /\ ( x e. dom F /\ y e. dom F ) ) -> ( ( N " ( I ` ( F ` x ) ) ) = ( N " ( I ` ( F ` y ) ) ) -> x = y ) ) |
| 61 |
21 60
|
syld |
|- ( ( ph /\ ( x e. dom F /\ y e. dom F ) ) -> ( ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) = ( `' J ` ( N " ( I ` ( F ` y ) ) ) ) -> x = y ) ) |