Metamath Proof Explorer

Theorem upgrimwlklem2

Description: Lemma 2 for upgrimwlk . (Contributed by AV, 25-Oct-2025)

Ref Expression
Hypotheses upgrimwlk.i 
|- I = ( iEdg ` G )
upgrimwlk.j 
|- J = ( iEdg ` H )
upgrimwlk.g 
|- ( ph -> G e. USPGraph )
upgrimwlk.h 
|- ( ph -> H e. USPGraph )
upgrimwlk.n 
|- ( ph -> N e. ( G GraphIso H ) )
upgrimwlk.e 
|- E = ( x e. dom F |-> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) )
upgrimwlk.f 
|- ( ph -> F e. Word dom I )
Assertion upgrimwlklem2 
|- ( ph -> E e. Word dom J )

Proof

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 4 adantr 
 |-  ( ( ph /\ x e. dom F ) -> H e. USPGraph )
9 2 uspgrf1oedg 
 |-  ( H e. USPGraph -> J : dom J -1-1-onto-> ( Edg ` H ) )
10 8 9 syl 
 |-  ( ( ph /\ x e. dom F ) -> J : dom J -1-1-onto-> ( Edg ` H ) )
11 uspgruhgr 
 |-  ( G e. USPGraph -> G e. UHGraph )
12 3 11 syl 
 |-  ( ph -> G e. UHGraph )
13 uspgruhgr 
 |-  ( H e. USPGraph -> H e. UHGraph )
14 4 13 syl 
 |-  ( ph -> H e. UHGraph )
15 12 14 jca 
 |-  ( ph -> ( G e. UHGraph /\ H e. UHGraph ) )
16 15 adantr 
 |-  ( ( ph /\ x e. dom F ) -> ( G e. UHGraph /\ H e. UHGraph ) )
17 5 adantr 
 |-  ( ( ph /\ x e. dom F ) -> N e. ( G GraphIso H ) )
18 1 uhgrfun 
 |-  ( G e. UHGraph -> Fun I )
19 12 18 syl 
 |-  ( ph -> Fun I )
20 19 adantr 
 |-  ( ( ph /\ x e. dom F ) -> Fun I )
21 wrdf 
 |-  ( F e. Word dom I -> F : ( 0 ..^ ( # ` F ) ) --> dom I )
22 21 ffdmd 
 |-  ( F e. Word dom I -> F : dom F --> dom I )
23 7 22 syl 
 |-  ( ph -> F : dom F --> dom I )
24 23 ffvelcdmda 
 |-  ( ( ph /\ x e. dom F ) -> ( F ` x ) e. dom I )
25 1 iedgedg 
 |-  ( ( Fun I /\ ( F ` x ) e. dom I ) -> ( I ` ( F ` x ) ) e. ( Edg ` G ) )
26 20 24 25 syl2anc 
 |-  ( ( ph /\ x e. dom F ) -> ( I ` ( F ` x ) ) e. ( Edg ` G ) )
27 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
28 eqid 
 |-  ( Edg ` H ) = ( Edg ` H )
29 27 28 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 ) )
30 16 17 26 29 syl12anc 
 |-  ( ( ph /\ x e. dom F ) -> ( N " ( I ` ( F ` x ) ) ) e. ( Edg ` H ) )
31 f1ocnvdm 
 |-  ( ( J : dom J -1-1-onto-> ( Edg ` H ) /\ ( N " ( I ` ( F ` x ) ) ) e. ( Edg ` H ) ) -> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) e. dom J )
32 10 30 31 syl2anc 
 |-  ( ( ph /\ x e. dom F ) -> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) e. dom J )
33 32 6 fmptd 
 |-  ( ph -> E : dom F --> dom J )
34 1 2 3 4 5 6 7 upgrimwlklem1 
 |-  ( ph -> ( # ` E ) = ( # ` F ) )
35 34 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` E ) ) = ( 0 ..^ ( # ` F ) ) )
36 iswrdb 
 |-  ( F e. Word dom I <-> F : ( 0 ..^ ( # ` F ) ) --> dom I )
37 fdm 
 |-  ( F : ( 0 ..^ ( # ` F ) ) --> dom I -> dom F = ( 0 ..^ ( # ` F ) ) )
38 37 eqcomd 
 |-  ( F : ( 0 ..^ ( # ` F ) ) --> dom I -> ( 0 ..^ ( # ` F ) ) = dom F )
39 36 38 sylbi 
 |-  ( F e. Word dom I -> ( 0 ..^ ( # ` F ) ) = dom F )
40 7 39 syl 
 |-  ( ph -> ( 0 ..^ ( # ` F ) ) = dom F )
41 35 40 eqtrd 
 |-  ( ph -> ( 0 ..^ ( # ` E ) ) = dom F )
42 41 feq2d 
 |-  ( ph -> ( E : ( 0 ..^ ( # ` E ) ) --> dom J <-> E : dom F --> dom J ) )
43 33 42 mpbird 
 |-  ( ph -> E : ( 0 ..^ ( # ` E ) ) --> dom J )
44 iswrdb 
 |-  ( E e. Word dom J <-> E : ( 0 ..^ ( # ` E ) ) --> dom J )
45 43 44 sylibr 
 |-  ( ph -> E e. Word dom J )