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

Metamath Proof Explorer

Theorem upgrimwlklem2

Description: Lemma 2 for upgrimwlk . (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 upgrimwlklem2 ( 𝜑 → 𝐸 ∈ Word dom 𝐽 )

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 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → 𝐻 ∈ USPGraph )
9 2 uspgrf1oedg ⊢ ( 𝐻 ∈ USPGraph → 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) )
10 8 9 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) )
11 uspgruhgr ⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UHGraph )
12 3 11 syl ⊢ ( 𝜑 → 𝐺 ∈ UHGraph )
13 uspgruhgr ⊢ ( 𝐻 ∈ USPGraph → 𝐻 ∈ UHGraph )
14 4 13 syl ⊢ ( 𝜑 → 𝐻 ∈ UHGraph )
15 12 14 jca ⊢ ( 𝜑 → ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) )
17 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) )
18 1 uhgrfun ⊢ ( 𝐺 ∈ UHGraph → Fun 𝐼 )
19 12 18 syl ⊢ ( 𝜑 → Fun 𝐼 )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → Fun 𝐼 )
21 wrdf ⊢ ( 𝐹 ∈ Word dom 𝐼 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 )
22 21 ffdmd ⊢ ( 𝐹 ∈ Word dom 𝐼 → 𝐹 : dom 𝐹 ⟶ dom 𝐼 )
23 7 22 syl ⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ dom 𝐼 )
24 23 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) ∈ dom 𝐼 )
25 1 iedgedg ⊢ ( ( Fun 𝐼 ∧ ( 𝐹 ‘ 𝑥 ) ∈ dom 𝐼 ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ( Edg ‘ 𝐺 ) )
26 20 24 25 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ( Edg ‘ 𝐺 ) )
27 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
28 eqid ⊢ ( Edg ‘ 𝐻 ) = ( Edg ‘ 𝐻 )
29 27 28 uhgrimedgi ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ ( Edg ‘ 𝐻 ) )
30 16 17 26 29 syl12anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ ( Edg ‘ 𝐻 ) )
31 f1ocnvdm ⊢ ( ( 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) ∧ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ ( Edg ‘ 𝐻 ) ) → ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ∈ dom 𝐽 )
32 10 30 31 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ∈ dom 𝐽 )
33 32 6 fmptd ⊢ ( 𝜑 → 𝐸 : dom 𝐹 ⟶ dom 𝐽 )
34 1 2 3 4 5 6 7 upgrimwlklem1 ⊢ ( 𝜑 → ( ♯ ‘ 𝐸 ) = ( ♯ ‘ 𝐹 ) )
35 34 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐸 ) ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
36 iswrdb ⊢ ( 𝐹 ∈ Word dom 𝐼 ↔ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 )
37 fdm ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 → dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
38 37 eqcomd ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = dom 𝐹 )
39 36 38 sylbi ⊢ ( 𝐹 ∈ Word dom 𝐼 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = dom 𝐹 )
40 7 39 syl ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = dom 𝐹 )
41 35 40 eqtrd ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐸 ) ) = dom 𝐹 )
42 41 feq2d ⊢ ( 𝜑 → ( 𝐸 : ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ⟶ dom 𝐽 ↔ 𝐸 : dom 𝐹 ⟶ dom 𝐽 ) )
43 33 42 mpbird ⊢ ( 𝜑 → 𝐸 : ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ⟶ dom 𝐽 )
44 iswrdb ⊢ ( 𝐸 ∈ Word dom 𝐽 ↔ 𝐸 : ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ⟶ dom 𝐽 )
45 43 44 sylibr ⊢ ( 𝜑 → 𝐸 ∈ Word dom 𝐽 )