Metamath Proof Explorer

Theorem trlreslem

Description: Lemma for trlres . Formerly part of proof of eupthres . (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Mario Carneiro, 3-May-2015) (Revised by AV, 6-Mar-2021) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022)

Ref Expression
Hypotheses trlres.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
trlres.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
trlres.d ⊢ ( 𝜑 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
trlres.n ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
trlres.h ⊢ 𝐻 = ( 𝐹 prefix 𝑁 )
Assertion trlreslem ( 𝜑 → 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ dom ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 trlres.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 trlres.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 trlres.d ⊢ ( 𝜑 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
4 trlres.n ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
5 trlres.h ⊢ 𝐻 = ( 𝐹 prefix 𝑁 )
6 2 trlf1 ⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 )
7 3 6 syl ⊢ ( 𝜑 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 )
8 elfzouz2 ⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
9 fzoss2 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 𝑁 ) → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
10 4 8 9 3syl ⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
11 f1ores ⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ∧ ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) : ( 0 ..^ 𝑁 ) –1-1-onto→ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) )
12 7 10 11 syl2anc ⊢ ( 𝜑 → ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) : ( 0 ..^ 𝑁 ) –1-1-onto→ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) )
13 trliswlk ⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
14 2 wlkf ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom 𝐼 )
15 3 13 14 3syl ⊢ ( 𝜑 → 𝐹 ∈ Word dom 𝐼 )
16 fzossfz ⊢ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝐹 ) )
17 16 4 sselid ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
18 pfxres ⊢ ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 prefix 𝑁 ) = ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) )
19 15 17 18 syl2anc ⊢ ( 𝜑 → ( 𝐹 prefix 𝑁 ) = ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) )
20 5 19 syl5eq ⊢ ( 𝜑 → 𝐻 = ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) )
21 5 fveq2i ⊢ ( ♯ ‘ 𝐻 ) = ( ♯ ‘ ( 𝐹 prefix 𝑁 ) )
22 elfzofz ⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
23 4 22 syl ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
24 pfxlen ⊢ ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ♯ ‘ ( 𝐹 prefix 𝑁 ) ) = 𝑁 )
25 15 23 24 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐹 prefix 𝑁 ) ) = 𝑁 )
26 21 25 syl5eq ⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) = 𝑁 )
27 26 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐻 ) ) = ( 0 ..^ 𝑁 ) )
28 wrdf ⊢ ( 𝐹 ∈ Word dom 𝐼 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 )
29 fimass ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 → ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ⊆ dom 𝐼 )
30 14 28 29 3syl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ⊆ dom 𝐼 )
31 3 13 30 3syl ⊢ ( 𝜑 → ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ⊆ dom 𝐼 )
32 ssdmres ⊢ ( ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ⊆ dom 𝐼 ↔ dom ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) = ( 𝐹 “ ( 0 ..^ 𝑁 ) ) )
33 31 32 sylib ⊢ ( 𝜑 → dom ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) = ( 𝐹 “ ( 0 ..^ 𝑁 ) ) )
34 20 27 33 f1oeq123d ⊢ ( 𝜑 → ( 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ dom ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ↔ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) : ( 0 ..^ 𝑁 ) –1-1-onto→ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) )
35 12 34 mpbird ⊢ ( 𝜑 → 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ dom ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) )