Metamath Proof Explorer

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 ⊢ φ → G ∈ USHGraph
upgrimwlk.h ⊢ φ → H ∈ USHGraph
upgrimwlk.n ⊢ φ → N ∈ G GraphIso H
upgrimwlk.e ⊢ E = x ∈ dom ⁡ F ⟼ J -1 ⁡ N I ⁡ F ⁡ x
upgrimwlk.f ⊢ φ → F ∈ Word dom ⁡ I
upgrimwlklem.p ⊢ φ → P : 0 … F ⟶ Vtx ⁡ G
Assertion upgrimwlklem4 ⊢ φ → N ∘ 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 ⊢ φ → G ∈ USHGraph
4 upgrimwlk.h ⊢ φ → H ∈ USHGraph
5 upgrimwlk.n ⊢ φ → N ∈ G GraphIso H
6 upgrimwlk.e ⊢ E = x ∈ dom ⁡ F ⟼ J -1 ⁡ N I ⁡ F ⁡ x
7 upgrimwlk.f ⊢ φ → F ∈ Word dom ⁡ I
8 upgrimwlklem.p ⊢ φ → P : 0 … F ⟶ Vtx ⁡ G
9 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
10 eqid ⊢ Vtx ⁡ H = Vtx ⁡ H
11 9 10 grimf1o ⊢ N ∈ 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 ⊢ φ → N : Vtx ⁡ G ⟶ Vtx ⁡ H
14 1 2 3 4 5 6 7 upgrimwlklem1 ⊢ φ → E = F
15 14 oveq2d ⊢ φ → 0 … E = 0 … F
16 15 feq2d ⊢ φ → P : 0 … E ⟶ Vtx ⁡ G ↔ P : 0 … F ⟶ Vtx ⁡ G
17 8 16 mpbird ⊢ φ → P : 0 … E ⟶ Vtx ⁡ G
18 13 17 fcod ⊢ φ → N ∘ P : 0 … E ⟶ Vtx ⁡ H