Theorem upgrimwlklem4

Description: Lemma 4 for upgrimwlk . (Contributed by AV, 28-Oct-2025)

	Ref	Expression
Hypotheses	upgrimwlk.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	upgrimwlk.j	⊢ 𝐽 = ( iEdg ‘ 𝐻 )
	upgrimwlk.g	⊢ ( 𝜑 → 𝐺 ∈ USPGraph )
	upgrimwlk.h	⊢ ( 𝜑 → 𝐻 ∈ USPGraph )
	upgrimwlk.n	⊢ ( 𝜑 → 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) )
	upgrimwlk.e	⊢ 𝐸 = ( 𝑥 ∈ dom 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
	upgrimwlk.f	⊢ ( 𝜑 → 𝐹 ∈ Word dom 𝐼 )
	upgrimwlklem.p	⊢ ( 𝜑 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
Assertion	upgrimwlklem4	⊢ ( 𝜑 → ( 𝑁 ∘ 𝑃 ) : ( 0 ... ( ♯ ‘ 𝐸 ) ) ⟶ ( Vtx ‘ 𝐻 ) )

Proof

Step	Hyp	Ref	Expression
1		upgrimwlk.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2		upgrimwlk.j	⊢ 𝐽 = ( iEdg ‘ 𝐻 )
3		upgrimwlk.g	⊢ ( 𝜑 → 𝐺 ∈ USPGraph )
4		upgrimwlk.h	⊢ ( 𝜑 → 𝐻 ∈ USPGraph )
5		upgrimwlk.n	⊢ ( 𝜑 → 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) )
6		upgrimwlk.e	⊢ 𝐸 = ( 𝑥 ∈ dom 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
7		upgrimwlk.f	⊢ ( 𝜑 → 𝐹 ∈ Word dom 𝐼 )
8		upgrimwlklem.p	⊢ ( 𝜑 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
9		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
10		eqid	⊢ ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐻 )
11	9 10	grimf1o	⊢ ( 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) → 𝑁 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) )
12		f1of	⊢ ( 𝑁 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) → 𝑁 : ( Vtx ‘ 𝐺 ) ⟶ ( Vtx ‘ 𝐻 ) )
13	5 11 12	3syl	⊢ ( 𝜑 → 𝑁 : ( Vtx ‘ 𝐺 ) ⟶ ( Vtx ‘ 𝐻 ) )
14	1 2 3 4 5 6 7	upgrimwlklem1	⊢ ( 𝜑 → ( ♯ ‘ 𝐸 ) = ( ♯ ‘ 𝐹 ) )
15	14	oveq2d	⊢ ( 𝜑 → ( 0 ... ( ♯ ‘ 𝐸 ) ) = ( 0 ... ( ♯ ‘ 𝐹 ) ) )
16	15	feq2d	⊢ ( 𝜑 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐸 ) ) ⟶ ( Vtx ‘ 𝐺 ) ↔ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) )
17	8 16	mpbird	⊢ ( 𝜑 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐸 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
18	13 17	fcod	⊢ ( 𝜑 → ( 𝑁 ∘ 𝑃 ) : ( 0 ... ( ♯ ‘ 𝐸 ) ) ⟶ ( Vtx ‘ 𝐻 ) )