This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐻 ) )