Metamath Proof Explorer

Theorem wrdpmtrlast

Description: Reorder a word, so that the symbol given at index I is at the end. (Contributed by Thierry Arnoux, 27-May-2025)

Ref Expression
Hypotheses wrdpmtrlast.1 ⊢ 𝐽 = ( 0 ..^ ( ♯ ‘ 𝑊 ) )
wrdpmtrlast.2 ⊢ ( 𝜑 → 𝐼 ∈ 𝐽 )
wrdpmtrlast.3 ⊢ ( 𝜑 → 𝑊 ∈ Word 𝑆 )
wrdpmtrlast.4 ⊢ 𝑈 = ( ( 𝑊 ∘ 𝑠 ) prefix ( ( ♯ ‘ 𝑊 ) − 1 ) )
Assertion wrdpmtrlast ( 𝜑 → ∃ 𝑠 ( 𝑠 : 𝐽 –1-1-onto→ 𝐽 ∧ ( 𝑊 ∘ 𝑠 ) = ( 𝑈 ++ ⟨“ ( 𝑊 ‘ 𝐼 ) ”⟩ ) ) )

Proof

Step Hyp Ref Expression
1 wrdpmtrlast.1 ⊢ 𝐽 = ( 0 ..^ ( ♯ ‘ 𝑊 ) )
2 wrdpmtrlast.2 ⊢ ( 𝜑 → 𝐼 ∈ 𝐽 )
3 wrdpmtrlast.3 ⊢ ( 𝜑 → 𝑊 ∈ Word 𝑆 )
4 wrdpmtrlast.4 ⊢ 𝑈 = ( ( 𝑊 ∘ 𝑠 ) prefix ( ( ♯ ‘ 𝑊 ) − 1 ) )
5 1 2 fzo0pmtrlast ⊢ ( 𝜑 → ∃ 𝑠 ( 𝑠 : 𝐽 –1-1-onto→ 𝐽 ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) )
6 simplr ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → 𝑠 : 𝐽 –1-1-onto→ 𝐽 )
7 f1of ⊢ ( 𝑠 : 𝐽 –1-1-onto→ 𝐽 → 𝑠 : 𝐽 ⟶ 𝐽 )
8 1 feq2i ⊢ ( 𝑠 : 𝐽 ⟶ 𝐽 ↔ 𝑠 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐽 )
9 7 8 sylib ⊢ ( 𝑠 : 𝐽 –1-1-onto→ 𝐽 → 𝑠 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐽 )
10 6 9 syl ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → 𝑠 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐽 )
11 iswrdi ⊢ ( 𝑠 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐽 → 𝑠 ∈ Word 𝐽 )
12 10 11 syl ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → 𝑠 ∈ Word 𝐽 )
13 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) )
14 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → 𝑊 ∈ Word 𝑆 )
15 13 14 wrdfd ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑆 )
16 1 feq2i ⊢ ( 𝑊 : 𝐽 ⟶ 𝑆 ↔ 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑆 )
17 15 16 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → 𝑊 : 𝐽 ⟶ 𝑆 )
18 lenco ⊢ ( ( 𝑠 ∈ Word 𝐽 ∧ 𝑊 : 𝐽 ⟶ 𝑆 ) → ( ♯ ‘ ( 𝑊 ∘ 𝑠 ) ) = ( ♯ ‘ 𝑠 ) )
19 12 17 18 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( ♯ ‘ ( 𝑊 ∘ 𝑠 ) ) = ( ♯ ‘ 𝑠 ) )
20 10 ffund ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → Fun 𝑠 )
21 hashfundm ⊢ ( ( 𝑠 ∈ Word 𝐽 ∧ Fun 𝑠 ) → ( ♯ ‘ 𝑠 ) = ( ♯ ‘ dom 𝑠 ) )
22 12 20 21 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( ♯ ‘ 𝑠 ) = ( ♯ ‘ dom 𝑠 ) )
23 10 fdmd ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → dom 𝑠 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
24 23 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( ♯ ‘ dom 𝑠 ) = ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
25 2 1 eleqtrdi ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
26 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
27 elfzo0 ⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) )
28 27 simp2bi ⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
29 26 28 syl ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
30 29 nnnn0d ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
31 hashfzo0 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) = ( ♯ ‘ 𝑊 ) )
32 30 31 syl ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) = ( ♯ ‘ 𝑊 ) )
33 22 24 32 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( ♯ ‘ 𝑠 ) = ( ♯ ‘ 𝑊 ) )
34 19 33 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ ( 𝑊 ∘ 𝑠 ) ) )
35 34 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = ( ( ♯ ‘ ( 𝑊 ∘ 𝑠 ) ) − 1 ) )
36 35 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( ( 𝑊 ∘ 𝑠 ) prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( ( 𝑊 ∘ 𝑠 ) prefix ( ( ♯ ‘ ( 𝑊 ∘ 𝑠 ) ) − 1 ) ) )
37 4 36 eqtrid ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → 𝑈 = ( ( 𝑊 ∘ 𝑠 ) prefix ( ( ♯ ‘ ( 𝑊 ∘ 𝑠 ) ) − 1 ) ) )
38 26 ne0d ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ≠ ∅ )
39 f0dom0 ⊢ ( 𝑠 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐽 → ( ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ∅ ↔ 𝑠 = ∅ ) )
40 39 necon3bid ⊢ ( 𝑠 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐽 → ( ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ≠ ∅ ↔ 𝑠 ≠ ∅ ) )
41 40 biimpa ⊢ ( ( 𝑠 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐽 ∧ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ≠ ∅ ) → 𝑠 ≠ ∅ )
42 10 38 41 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → 𝑠 ≠ ∅ )
43 lswco ⊢ ( ( 𝑠 ∈ Word 𝐽 ∧ 𝑠 ≠ ∅ ∧ 𝑊 : 𝐽 ⟶ 𝑆 ) → ( lastS ‘ ( 𝑊 ∘ 𝑠 ) ) = ( 𝑊 ‘ ( lastS ‘ 𝑠 ) ) )
44 12 42 17 43 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( lastS ‘ ( 𝑊 ∘ 𝑠 ) ) = ( 𝑊 ‘ ( lastS ‘ 𝑠 ) ) )
45 lsw ⊢ ( 𝑠 ∈ Word 𝐽 → ( lastS ‘ 𝑠 ) = ( 𝑠 ‘ ( ( ♯ ‘ 𝑠 ) − 1 ) ) )
46 12 45 syl ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( lastS ‘ 𝑠 ) = ( 𝑠 ‘ ( ( ♯ ‘ 𝑠 ) − 1 ) ) )
47 33 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( ( ♯ ‘ 𝑠 ) − 1 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
48 47 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( 𝑠 ‘ ( ( ♯ ‘ 𝑠 ) − 1 ) ) = ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
49 simpr ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 )
50 46 48 49 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( lastS ‘ 𝑠 ) = 𝐼 )
51 50 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( 𝑊 ‘ ( lastS ‘ 𝑠 ) ) = ( 𝑊 ‘ 𝐼 ) )
52 44 51 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( 𝑊 ‘ 𝐼 ) = ( lastS ‘ ( 𝑊 ∘ 𝑠 ) ) )
53 52 s1eqd ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ⟨“ ( 𝑊 ‘ 𝐼 ) ”⟩ = ⟨“ ( lastS ‘ ( 𝑊 ∘ 𝑠 ) ) ”⟩ )
54 37 53 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( 𝑈 ++ ⟨“ ( 𝑊 ‘ 𝐼 ) ”⟩ ) = ( ( ( 𝑊 ∘ 𝑠 ) prefix ( ( ♯ ‘ ( 𝑊 ∘ 𝑠 ) ) − 1 ) ) ++ ⟨“ ( lastS ‘ ( 𝑊 ∘ 𝑠 ) ) ”⟩ ) )
55 1 6 14 wrdpmcl ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( 𝑊 ∘ 𝑠 ) ∈ Word 𝑆 )
56 fzo0end ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
57 29 56 syl ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
58 57 1 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ 𝐽 )
59 17 fdmd ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → dom 𝑊 = 𝐽 )
60 58 59 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ dom 𝑊 )
61 dff1o5 ⊢ ( 𝑠 : 𝐽 –1-1-onto→ 𝐽 ↔ ( 𝑠 : 𝐽 –1-1→ 𝐽 ∧ ran 𝑠 = 𝐽 ) )
62 61 simprbi ⊢ ( 𝑠 : 𝐽 –1-1-onto→ 𝐽 → ran 𝑠 = 𝐽 )
63 6 62 syl ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ran 𝑠 = 𝐽 )
64 58 63 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ran 𝑠 )
65 60 64 elind ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( dom 𝑊 ∩ ran 𝑠 ) )
66 65 ne0d ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( dom 𝑊 ∩ ran 𝑠 ) ≠ ∅ )
67 coeq0 ⊢ ( ( 𝑊 ∘ 𝑠 ) = ∅ ↔ ( dom 𝑊 ∩ ran 𝑠 ) = ∅ )
68 67 necon3bii ⊢ ( ( 𝑊 ∘ 𝑠 ) ≠ ∅ ↔ ( dom 𝑊 ∩ ran 𝑠 ) ≠ ∅ )
69 66 68 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( 𝑊 ∘ 𝑠 ) ≠ ∅ )
70 pfxlswccat ⊢ ( ( ( 𝑊 ∘ 𝑠 ) ∈ Word 𝑆 ∧ ( 𝑊 ∘ 𝑠 ) ≠ ∅ ) → ( ( ( 𝑊 ∘ 𝑠 ) prefix ( ( ♯ ‘ ( 𝑊 ∘ 𝑠 ) ) − 1 ) ) ++ ⟨“ ( lastS ‘ ( 𝑊 ∘ 𝑠 ) ) ”⟩ ) = ( 𝑊 ∘ 𝑠 ) )
71 55 69 70 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( ( ( 𝑊 ∘ 𝑠 ) prefix ( ( ♯ ‘ ( 𝑊 ∘ 𝑠 ) ) − 1 ) ) ++ ⟨“ ( lastS ‘ ( 𝑊 ∘ 𝑠 ) ) ”⟩ ) = ( 𝑊 ∘ 𝑠 ) )
72 54 71 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( 𝑊 ∘ 𝑠 ) = ( 𝑈 ++ ⟨“ ( 𝑊 ‘ 𝐼 ) ”⟩ ) )
73 6 72 jca ⊢ ( ( ( 𝜑 ∧ 𝑠 : 𝐽 –1-1-onto→ 𝐽 ) ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( 𝑠 : 𝐽 –1-1-onto→ 𝐽 ∧ ( 𝑊 ∘ 𝑠 ) = ( 𝑈 ++ ⟨“ ( 𝑊 ‘ 𝐼 ) ”⟩ ) ) )
74 73 expl ⊢ ( 𝜑 → ( ( 𝑠 : 𝐽 –1-1-onto→ 𝐽 ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ( 𝑠 : 𝐽 –1-1-onto→ 𝐽 ∧ ( 𝑊 ∘ 𝑠 ) = ( 𝑈 ++ ⟨“ ( 𝑊 ‘ 𝐼 ) ”⟩ ) ) ) )
75 74 eximdv ⊢ ( 𝜑 → ( ∃ 𝑠 ( 𝑠 : 𝐽 –1-1-onto→ 𝐽 ∧ ( 𝑠 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = 𝐼 ) → ∃ 𝑠 ( 𝑠 : 𝐽 –1-1-onto→ 𝐽 ∧ ( 𝑊 ∘ 𝑠 ) = ( 𝑈 ++ ⟨“ ( 𝑊 ‘ 𝐼 ) ”⟩ ) ) ) )
76 5 75 mpd ⊢ ( 𝜑 → ∃ 𝑠 ( 𝑠 : 𝐽 –1-1-onto→ 𝐽 ∧ ( 𝑊 ∘ 𝑠 ) = ( 𝑈 ++ ⟨“ ( 𝑊 ‘ 𝐼 ) ”⟩ ) ) )