Theorem upgrimwlklem4

Description: Lemma 4 for upgrimwlk . (Contributed by AV, 28-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 )
	upgrimwlklem.p	|- ( ph -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
Assertion	upgrimwlklem4	|- ( ph -> ( N o. P ) : ( 0 ... ( # ` E ) ) --> ( Vtx ` H ) )

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		upgrimwlklem.p	|- ( ph -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
9		eqid	|- ( Vtx ` G ) = ( Vtx ` G )
10		eqid	|- ( Vtx ` H ) = ( Vtx ` H )
11	9 10	grimf1o	|- ( N e. ( G GraphIso H ) -> N : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) )
12		f1of	|- ( N : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) -> N : ( Vtx ` G ) --> ( Vtx ` H ) )
13	5 11 12	3syl	|- ( ph -> N : ( Vtx ` G ) --> ( Vtx ` H ) )
14	1 2 3 4 5 6 7	upgrimwlklem1	|- ( ph -> ( # ` E ) = ( # ` F ) )
15	14	oveq2d	|- ( ph -> ( 0 ... ( # ` E ) ) = ( 0 ... ( # ` F ) ) )
16	15	feq2d	|- ( ph -> ( P : ( 0 ... ( # ` E ) ) --> ( Vtx ` G ) <-> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) )
17	8 16	mpbird	|- ( ph -> P : ( 0 ... ( # ` E ) ) --> ( Vtx ` G ) )
18	13 17	fcod	|- ( ph -> ( N o. P ) : ( 0 ... ( # ` E ) ) --> ( Vtx ` H ) )