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

Metamath Proof Explorer

Theorem upgrimwlklem1

Description: Lemma 1 for upgrimwlk and upgrimwlklen . (Contributed by AV, 25-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 𝐼 )
Assertion upgrimwlklem1 ( 𝜑 → ( ♯ ‘ 𝐸 ) = ( ♯ ‘ 𝐹 ) )

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 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ∈ V )
9 8 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ dom 𝐹 ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ∈ V )
10 eqid ⊢ ( 𝑥 ∈ dom 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) = ( 𝑥 ∈ dom 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
11 10 fnmpt ⊢ ( ∀ 𝑥 ∈ dom 𝐹 ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ∈ V → ( 𝑥 ∈ dom 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) Fn dom 𝐹 )
12 9 11 syl ⊢ ( 𝜑 → ( 𝑥 ∈ dom 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) Fn dom 𝐹 )
13 6 fneq1i ⊢ ( 𝐸 Fn dom 𝐹 ↔ ( 𝑥 ∈ dom 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) Fn dom 𝐹 )
14 12 13 sylibr ⊢ ( 𝜑 → 𝐸 Fn dom 𝐹 )
15 hashfn ⊢ ( 𝐸 Fn dom 𝐹 → ( ♯ ‘ 𝐸 ) = ( ♯ ‘ dom 𝐹 ) )
16 14 15 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐸 ) = ( ♯ ‘ dom 𝐹 ) )
17 wrdf ⊢ ( 𝐹 ∈ Word dom 𝐼 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 )
18 ffun ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 → Fun 𝐹 )
19 7 17 18 3syl ⊢ ( 𝜑 → Fun 𝐹 )
20 19 funfnd ⊢ ( 𝜑 → 𝐹 Fn dom 𝐹 )
21 hashfn ⊢ ( 𝐹 Fn dom 𝐹 → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ dom 𝐹 ) )
22 20 21 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ dom 𝐹 ) )
23 16 22 eqtr4d ⊢ ( 𝜑 → ( ♯ ‘ 𝐸 ) = ( ♯ ‘ 𝐹 ) )