Metamath Proof Explorer

Theorem upgrimwlklem1

Description: Lemma 1 for upgrimwlk and upgrimwlklen . (Contributed by AV, 25-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
Assertion upgrimwlklem1 ⊢ φ → E = F

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 fvexd ⊢ φ ∧ x ∈ dom ⁡ F → J -1 ⁡ N I ⁡ F ⁡ x ∈ V
9 8 ralrimiva ⊢ φ → ∀ x ∈ dom ⁡ F J -1 ⁡ N I ⁡ F ⁡ x ∈ V
10 eqid ⊢ x ∈ dom ⁡ F ⟼ J -1 ⁡ N I ⁡ F ⁡ x = x ∈ dom ⁡ F ⟼ J -1 ⁡ N I ⁡ F ⁡ x
11 10 fnmpt ⊢ ∀ x ∈ dom ⁡ F J -1 ⁡ N I ⁡ F ⁡ x ∈ V → x ∈ dom ⁡ F ⟼ J -1 ⁡ N I ⁡ F ⁡ x Fn dom ⁡ F
12 9 11 syl ⊢ φ → x ∈ dom ⁡ F ⟼ J -1 ⁡ N I ⁡ F ⁡ x Fn dom ⁡ F
13 6 fneq1i ⊢ E Fn dom ⁡ F ↔ x ∈ dom ⁡ F ⟼ J -1 ⁡ N I ⁡ F ⁡ x Fn dom ⁡ F
14 12 13 sylibr ⊢ φ → E Fn dom ⁡ F
15 hashfn ⊢ E Fn dom ⁡ F → E = dom ⁡ F
16 14 15 syl ⊢ φ → E = dom ⁡ F
17 wrdf ⊢ F ∈ Word dom ⁡ I → F : 0 ..^ F ⟶ dom ⁡ I
18 ffun ⊢ F : 0 ..^ F ⟶ dom ⁡ I → Fun ⁡ F
19 7 17 18 3syl ⊢ φ → Fun ⁡ F
20 19 funfnd ⊢ φ → F Fn dom ⁡ F
21 hashfn ⊢ F Fn dom ⁡ F → F = dom ⁡ F
22 20 21 syl ⊢ φ → F = dom ⁡ F
23 16 22 eqtr4d ⊢ φ → E = F