Metamath Proof Explorer

Theorem cycpmco2f1

Description: The word U used in cycpmco2 is injective, so it can represent a cycle and form a cyclic permutation ( MU ) . (Contributed by Thierry Arnoux, 4-Jan-2024)

Ref Expression
Hypotheses cycpmco2.c ⊢ 𝑀 = ( toCyc ‘ 𝐷 )
cycpmco2.s ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
cycpmco2.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
cycpmco2.w ⊢ ( 𝜑 → 𝑊 ∈ dom 𝑀 )
cycpmco2.i ⊢ ( 𝜑 → 𝐼 ∈ ( 𝐷 ∖ ran 𝑊 ) )
cycpmco2.j ⊢ ( 𝜑 → 𝐽 ∈ ran 𝑊 )
cycpmco2.e ⊢ 𝐸 = ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 )
cycpmco2.1 ⊢ 𝑈 = ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ )
Assertion cycpmco2f1 ( 𝜑 → 𝑈 : dom 𝑈 –1-1→ 𝐷 )

Proof

Step Hyp Ref Expression
1 cycpmco2.c ⊢ 𝑀 = ( toCyc ‘ 𝐷 )
2 cycpmco2.s ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
3 cycpmco2.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
4 cycpmco2.w ⊢ ( 𝜑 → 𝑊 ∈ dom 𝑀 )
5 cycpmco2.i ⊢ ( 𝜑 → 𝐼 ∈ ( 𝐷 ∖ ran 𝑊 ) )
6 cycpmco2.j ⊢ ( 𝜑 → 𝐽 ∈ ran 𝑊 )
7 cycpmco2.e ⊢ 𝐸 = ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 )
8 cycpmco2.1 ⊢ 𝑈 = ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ )
9 ssrab2 ⊢ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⊆ Word 𝐷
10 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
11 1 2 10 tocycf ⊢ ( 𝐷 ∈ 𝑉 → 𝑀 : { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⟶ ( Base ‘ 𝑆 ) )
12 3 11 syl ⊢ ( 𝜑 → 𝑀 : { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⟶ ( Base ‘ 𝑆 ) )
13 12 fdmd ⊢ ( 𝜑 → dom 𝑀 = { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } )
14 4 13 eleqtrd ⊢ ( 𝜑 → 𝑊 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } )
15 9 14 sselid ⊢ ( 𝜑 → 𝑊 ∈ Word 𝐷 )
16 pfxcl ⊢ ( 𝑊 ∈ Word 𝐷 → ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 )
17 15 16 syl ⊢ ( 𝜑 → ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 )
18 5 eldifad ⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
19 18 s1cld ⊢ ( 𝜑 → ⟨“ 𝐼 ”⟩ ∈ Word 𝐷 )
20 ccatcl ⊢ ( ( ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 ∧ ⟨“ 𝐼 ”⟩ ∈ Word 𝐷 ) → ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ∈ Word 𝐷 )
21 17 19 20 syl2anc ⊢ ( 𝜑 → ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ∈ Word 𝐷 )
22 swrdcl ⊢ ( 𝑊 ∈ Word 𝐷 → ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝐷 )
23 15 22 syl ⊢ ( 𝜑 → ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝐷 )
24 id ⊢ ( 𝑤 = 𝑊 → 𝑤 = 𝑊 )
25 dmeq ⊢ ( 𝑤 = 𝑊 → dom 𝑤 = dom 𝑊 )
26 eqidd ⊢ ( 𝑤 = 𝑊 → 𝐷 = 𝐷 )
27 24 25 26 f1eq123d ⊢ ( 𝑤 = 𝑊 → ( 𝑤 : dom 𝑤 –1-1→ 𝐷 ↔ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) )
28 27 elrab ⊢ ( 𝑊 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ↔ ( 𝑊 ∈ Word 𝐷 ∧ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) )
29 14 28 sylib ⊢ ( 𝜑 → ( 𝑊 ∈ Word 𝐷 ∧ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) )
30 29 simprd ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
31 f1cnv ⊢ ( 𝑊 : dom 𝑊 –1-1→ 𝐷 → ◡ 𝑊 : ran 𝑊 –1-1-onto→ dom 𝑊 )
32 f1of ⊢ ( ◡ 𝑊 : ran 𝑊 –1-1-onto→ dom 𝑊 → ◡ 𝑊 : ran 𝑊 ⟶ dom 𝑊 )
33 30 31 32 3syl ⊢ ( 𝜑 → ◡ 𝑊 : ran 𝑊 ⟶ dom 𝑊 )
34 33 6 ffvelrnd ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ 𝐽 ) ∈ dom 𝑊 )
35 wrddm ⊢ ( 𝑊 ∈ Word 𝐷 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
36 15 35 syl ⊢ ( 𝜑 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
37 34 36 eleqtrd ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
38 fzofzp1 ⊢ ( ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
39 37 38 syl ⊢ ( 𝜑 → ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
40 7 39 eqeltrid ⊢ ( 𝜑 → 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
41 15 30 40 pfxf1 ⊢ ( 𝜑 → ( 𝑊 prefix 𝐸 ) : dom ( 𝑊 prefix 𝐸 ) –1-1→ 𝐷 )
42 18 s1f1 ⊢ ( 𝜑 → ⟨“ 𝐼 ”⟩ : dom ⟨“ 𝐼 ”⟩ –1-1→ 𝐷 )
43 s1rn ⊢ ( 𝐼 ∈ 𝐷 → ran ⟨“ 𝐼 ”⟩ = { 𝐼 } )
44 18 43 syl ⊢ ( 𝜑 → ran ⟨“ 𝐼 ”⟩ = { 𝐼 } )
45 44 ineq2d ⊢ ( 𝜑 → ( ran ( 𝑊 prefix 𝐸 ) ∩ ran ⟨“ 𝐼 ”⟩ ) = ( ran ( 𝑊 prefix 𝐸 ) ∩ { 𝐼 } ) )
46 pfxrn2 ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ran ( 𝑊 prefix 𝐸 ) ⊆ ran 𝑊 )
47 15 40 46 syl2anc ⊢ ( 𝜑 → ran ( 𝑊 prefix 𝐸 ) ⊆ ran 𝑊 )
48 47 ssrind ⊢ ( 𝜑 → ( ran ( 𝑊 prefix 𝐸 ) ∩ { 𝐼 } ) ⊆ ( ran 𝑊 ∩ { 𝐼 } ) )
49 5 eldifbd ⊢ ( 𝜑 → ¬ 𝐼 ∈ ran 𝑊 )
50 disjsn ⊢ ( ( ran 𝑊 ∩ { 𝐼 } ) = ∅ ↔ ¬ 𝐼 ∈ ran 𝑊 )
51 49 50 sylibr ⊢ ( 𝜑 → ( ran 𝑊 ∩ { 𝐼 } ) = ∅ )
52 48 51 sseqtrd ⊢ ( 𝜑 → ( ran ( 𝑊 prefix 𝐸 ) ∩ { 𝐼 } ) ⊆ ∅ )
53 ss0 ⊢ ( ( ran ( 𝑊 prefix 𝐸 ) ∩ { 𝐼 } ) ⊆ ∅ → ( ran ( 𝑊 prefix 𝐸 ) ∩ { 𝐼 } ) = ∅ )
54 52 53 syl ⊢ ( 𝜑 → ( ran ( 𝑊 prefix 𝐸 ) ∩ { 𝐼 } ) = ∅ )
55 45 54 eqtrd ⊢ ( 𝜑 → ( ran ( 𝑊 prefix 𝐸 ) ∩ ran ⟨“ 𝐼 ”⟩ ) = ∅ )
56 3 17 19 41 42 55 ccatf1 ⊢ ( 𝜑 → ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) : dom ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) –1-1→ 𝐷 )
57 lencl ⊢ ( 𝑊 ∈ Word 𝐷 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
58 nn0fz0 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
59 58 biimpi ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
60 15 57 59 3syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
61 15 40 60 30 swrdf1 ⊢ ( 𝜑 → ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) : dom ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) –1-1→ 𝐷 )
62 ccatrn ⊢ ( ( ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 ∧ ⟨“ 𝐼 ”⟩ ∈ Word 𝐷 ) → ran ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) = ( ran ( 𝑊 prefix 𝐸 ) ∪ ran ⟨“ 𝐼 ”⟩ ) )
63 17 19 62 syl2anc ⊢ ( 𝜑 → ran ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) = ( ran ( 𝑊 prefix 𝐸 ) ∪ ran ⟨“ 𝐼 ”⟩ ) )
64 63 ineq1d ⊢ ( 𝜑 → ( ran ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ∩ ran ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ( ( ran ( 𝑊 prefix 𝐸 ) ∪ ran ⟨“ 𝐼 ”⟩ ) ∩ ran ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
65 indir ⊢ ( ( ran ( 𝑊 prefix 𝐸 ) ∪ ran ⟨“ 𝐼 ”⟩ ) ∩ ran ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ( ( ran ( 𝑊 prefix 𝐸 ) ∩ ran ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ∪ ( ran ⟨“ 𝐼 ”⟩ ∩ ran ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
66 64 65 eqtrdi ⊢ ( 𝜑 → ( ran ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ∩ ran ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ( ( ran ( 𝑊 prefix 𝐸 ) ∩ ran ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ∪ ( ran ⟨“ 𝐼 ”⟩ ∩ ran ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) )
67 fz0ssnn0 ⊢ ( 0 ... ( ♯ ‘ 𝑊 ) ) ⊆ ℕ0
68 67 40 sselid ⊢ ( 𝜑 → 𝐸 ∈ ℕ0 )
69 pfxval ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ ℕ0 ) → ( 𝑊 prefix 𝐸 ) = ( 𝑊 substr ⟨ 0 , 𝐸 ⟩ ) )
70 15 68 69 syl2anc ⊢ ( 𝜑 → ( 𝑊 prefix 𝐸 ) = ( 𝑊 substr ⟨ 0 , 𝐸 ⟩ ) )
71 70 rneqd ⊢ ( 𝜑 → ran ( 𝑊 prefix 𝐸 ) = ran ( 𝑊 substr ⟨ 0 , 𝐸 ⟩ ) )
72 71 ineq1d ⊢ ( 𝜑 → ( ran ( 𝑊 prefix 𝐸 ) ∩ ran ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ( ran ( 𝑊 substr ⟨ 0 , 𝐸 ⟩ ) ∩ ran ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
73 0elfz ⊢ ( 𝐸 ∈ ℕ0 → 0 ∈ ( 0 ... 𝐸 ) )
74 68 73 syl ⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝐸 ) )
75 elfzuz3 ⊢ ( 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 𝐸 ) )
76 eluzfz1 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 𝐸 ) → 𝐸 ∈ ( 𝐸 ... ( ♯ ‘ 𝑊 ) ) )
77 40 75 76 3syl ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐸 ... ( ♯ ‘ 𝑊 ) ) )
78 eluzfz2 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 𝐸 ) → ( ♯ ‘ 𝑊 ) ∈ ( 𝐸 ... ( ♯ ‘ 𝑊 ) ) )
79 40 75 78 3syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ( 𝐸 ... ( ♯ ‘ 𝑊 ) ) )
80 15 74 40 30 77 79 swrdrndisj ⊢ ( 𝜑 → ( ran ( 𝑊 substr ⟨ 0 , 𝐸 ⟩ ) ∩ ran ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ∅ )
81 72 80 eqtrd ⊢ ( 𝜑 → ( ran ( 𝑊 prefix 𝐸 ) ∩ ran ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ∅ )
82 incom ⊢ ( ran ⟨“ 𝐼 ”⟩ ∩ ran ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ( ran ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∩ ran ⟨“ 𝐼 ”⟩ )
83 44 ineq2d ⊢ ( 𝜑 → ( ran ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∩ ran ⟨“ 𝐼 ”⟩ ) = ( ran ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∩ { 𝐼 } ) )
84 swrdrn2 ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ran ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ⊆ ran 𝑊 )
85 15 40 60 84 syl3anc ⊢ ( 𝜑 → ran ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ⊆ ran 𝑊 )
86 85 ssrind ⊢ ( 𝜑 → ( ran ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∩ { 𝐼 } ) ⊆ ( ran 𝑊 ∩ { 𝐼 } ) )
87 86 51 sseqtrd ⊢ ( 𝜑 → ( ran ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∩ { 𝐼 } ) ⊆ ∅ )
88 ss0 ⊢ ( ( ran ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∩ { 𝐼 } ) ⊆ ∅ → ( ran ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∩ { 𝐼 } ) = ∅ )
89 87 88 syl ⊢ ( 𝜑 → ( ran ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∩ { 𝐼 } ) = ∅ )
90 83 89 eqtrd ⊢ ( 𝜑 → ( ran ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∩ ran ⟨“ 𝐼 ”⟩ ) = ∅ )
91 82 90 syl5eq ⊢ ( 𝜑 → ( ran ⟨“ 𝐼 ”⟩ ∩ ran ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ∅ )
92 81 91 uneq12d ⊢ ( 𝜑 → ( ( ran ( 𝑊 prefix 𝐸 ) ∩ ran ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ∪ ( ran ⟨“ 𝐼 ”⟩ ∩ ran ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) = ( ∅ ∪ ∅ ) )
93 unidm ⊢ ( ∅ ∪ ∅ ) = ∅
94 93 a1i ⊢ ( 𝜑 → ( ∅ ∪ ∅ ) = ∅ )
95 66 92 94 3eqtrd ⊢ ( 𝜑 → ( ran ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ∩ ran ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ∅ )
96 3 21 23 56 61 95 ccatf1 ⊢ ( 𝜑 → ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) : dom ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) –1-1→ 𝐷 )
97 ovexd ⊢ ( 𝜑 → ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ∈ V )
98 7 97 eqeltrid ⊢ ( 𝜑 → 𝐸 ∈ V )
99 splval ⊢ ( ( 𝑊 ∈ dom 𝑀 ∧ ( 𝐸 ∈ V ∧ 𝐸 ∈ V ∧ ⟨“ 𝐼 ”⟩ ∈ Word 𝐷 ) ) → ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) = ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
100 4 98 98 19 99 syl13anc ⊢ ( 𝜑 → ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) = ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
101 8 100 syl5eq ⊢ ( 𝜑 → 𝑈 = ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
102 101 dmeqd ⊢ ( 𝜑 → dom 𝑈 = dom ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
103 eqidd ⊢ ( 𝜑 → 𝐷 = 𝐷 )
104 101 102 103 f1eq123d ⊢ ( 𝜑 → ( 𝑈 : dom 𝑈 –1-1→ 𝐷 ↔ ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) : dom ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) –1-1→ 𝐷 ) )
105 96 104 mpbird ⊢ ( 𝜑 → 𝑈 : dom 𝑈 –1-1→ 𝐷 )