Metamath Proof Explorer

Theorem upgrimtrlslem2

Description: Lemma 2 for upgrimtrls . (Contributed by AV, 29-Oct-2025)

Ref Expression
Hypotheses upgrimwlk.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
upgrimwlk.j ⊢ 𝐽 = ( iEdg ‘ 𝐻 )
upgrimwlk.g ⊢ ( 𝜑 → 𝐺 ∈ USPGraph )
upgrimwlk.h ⊢ ( 𝜑 → 𝐻 ∈ USPGraph )
upgrimwlk.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) )
upgrimwlk.e ⊢ 𝐸 = ( 𝑥 ∈ dom 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
upgrimtrls.t ⊢ ( 𝜑 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
Assertion upgrimtrlslem2 ( ( 𝜑 ∧ ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ 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 upgrimtrls.t ⊢ ( 𝜑 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
8 2 uspgrf1oedg ⊢ ( 𝐻 ∈ USPGraph → 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) )
9 f1of1 ⊢ ( 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) → 𝐽 : dom 𝐽 –1-1→ ( Edg ‘ 𝐻 ) )
10 4 8 9 3syl ⊢ ( 𝜑 → 𝐽 : dom 𝐽 –1-1→ ( Edg ‘ 𝐻 ) )
11 1 2 3 4 5 6 7 upgrimtrlslem1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ ( Edg ‘ 𝐻 ) )
12 edgval ⊢ ( Edg ‘ 𝐻 ) = ran ( iEdg ‘ 𝐻 )
13 2 eqcomi ⊢ ( iEdg ‘ 𝐻 ) = 𝐽
14 13 rneqi ⊢ ran ( iEdg ‘ 𝐻 ) = ran 𝐽
15 12 14 eqtri ⊢ ( Edg ‘ 𝐻 ) = ran 𝐽
16 11 15 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ ran 𝐽 )
17 1 2 3 4 5 6 7 upgrimtrlslem1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐹 ) → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ ( Edg ‘ 𝐻 ) )
18 17 15 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐹 ) → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ ran 𝐽 )
19 16 18 anim12dan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ) → ( ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ ran 𝐽 ∧ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ ran 𝐽 ) )
20 f1ocnvfvrneq ⊢ ( ( 𝐽 : dom 𝐽 –1-1→ ( Edg ‘ 𝐻 ) ∧ ( ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ ran 𝐽 ∧ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ ran 𝐽 ) ) → ( ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) = ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) )
21 10 19 20 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ) → ( ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) = ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) )
22 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
23 eqid ⊢ ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐻 )
24 22 23 grimf1o ⊢ ( 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) → 𝑁 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) )
25 f1of1 ⊢ ( 𝑁 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) → 𝑁 : ( Vtx ‘ 𝐺 ) –1-1→ ( Vtx ‘ 𝐻 ) )
26 5 24 25 3syl ⊢ ( 𝜑 → 𝑁 : ( Vtx ‘ 𝐺 ) –1-1→ ( Vtx ‘ 𝐻 ) )
27 uspgruhgr ⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UHGraph )
28 3 27 syl ⊢ ( 𝜑 → 𝐺 ∈ UHGraph )
29 trliswlk ⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
30 1 wlkf ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom 𝐼 )
31 wrdf ⊢ ( 𝐹 ∈ Word dom 𝐼 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 )
32 id ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 )
33 32 ffdmd ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 → 𝐹 : dom 𝐹 ⟶ dom 𝐼 )
34 30 31 33 3syl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 : dom 𝐹 ⟶ dom 𝐼 )
35 7 29 34 3syl ⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ dom 𝐼 )
36 35 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) ∈ dom 𝐼 )
37 22 1 uhgrss ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐹 ‘ 𝑥 ) ∈ dom 𝐼 ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ⊆ ( Vtx ‘ 𝐺 ) )
38 28 36 37 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ⊆ ( Vtx ‘ 𝐺 ) )
39 35 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑦 ) ∈ dom 𝐼 )
40 22 1 uhgrss ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐹 ‘ 𝑦 ) ∈ dom 𝐼 ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) ⊆ ( Vtx ‘ 𝐺 ) )
41 28 39 40 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐹 ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) ⊆ ( Vtx ‘ 𝐺 ) )
42 38 41 anim12dan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) ⊆ ( Vtx ‘ 𝐺 ) ) )
43 f1imaeq ⊢ ( ( 𝑁 : ( Vtx ‘ 𝐺 ) –1-1→ ( Vtx ‘ 𝐻 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) ⊆ ( Vtx ‘ 𝐺 ) ) ) → ( ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
44 26 42 43 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ) → ( ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
45 1 uspgrf1oedg ⊢ ( 𝐺 ∈ USPGraph → 𝐼 : dom 𝐼 –1-1-onto→ ( Edg ‘ 𝐺 ) )
46 f1of1 ⊢ ( 𝐼 : dom 𝐼 –1-1-onto→ ( Edg ‘ 𝐺 ) → 𝐼 : dom 𝐼 –1-1→ ( Edg ‘ 𝐺 ) )
47 3 45 46 3syl ⊢ ( 𝜑 → 𝐼 : dom 𝐼 –1-1→ ( Edg ‘ 𝐺 ) )
48 1 trlf1 ⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 )
49 f1f ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 )
50 fdm ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 → dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
51 50 eqcomd ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = dom 𝐹 )
52 49 51 syl ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = dom 𝐹 )
53 f1eq2 ⊢ ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = dom 𝐹 → ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ↔ 𝐹 : dom 𝐹 –1-1→ dom 𝐼 ) )
54 53 biimpcd ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 → ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = dom 𝐹 → 𝐹 : dom 𝐹 –1-1→ dom 𝐼 ) )
55 52 54 mpd ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 → 𝐹 : dom 𝐹 –1-1→ dom 𝐼 )
56 7 48 55 3syl ⊢ ( 𝜑 → 𝐹 : dom 𝐹 –1-1→ dom 𝐼 )
57 47 56 jca ⊢ ( 𝜑 → ( 𝐼 : dom 𝐼 –1-1→ ( Edg ‘ 𝐺 ) ∧ 𝐹 : dom 𝐹 –1-1→ dom 𝐼 ) )
58 f1cofveqaeq ⊢ ( ( ( 𝐼 : dom 𝐼 –1-1→ ( Edg ‘ 𝐺 ) ∧ 𝐹 : dom 𝐹 –1-1→ dom 𝐼 ) ∧ ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) )
59 57 58 sylan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) )
60 44 59 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ) → ( ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) ) → 𝑥 = 𝑦 ) )
61 21 60 syld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ) → ( ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) = ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) → 𝑥 = 𝑦 ) )