Theorem pfxf1

Description: Condition for a prefix to be injective. (Contributed by Thierry Arnoux, 13-Dec-2023)

	Ref	Expression
Hypotheses	pfxf1.1	|- ( ph -> W e. Word S )
	pfxf1.2	|- ( ph -> W : dom W -1-1-> S )
	pfxf1.3	|- ( ph -> L e. ( 0 ... ( # ` W ) ) )
Assertion	pfxf1	|- ( ph -> ( W prefix L ) : dom ( W prefix L ) -1-1-> S )

Proof

Step	Hyp	Ref	Expression
1		pfxf1.1	|- ( ph -> W e. Word S )
2		pfxf1.2	|- ( ph -> W : dom W -1-1-> S )
3		pfxf1.3	|- ( ph -> L e. ( 0 ... ( # ` W ) ) )
4		elfzuz3	|- ( L e. ( 0 ... ( # ` W ) ) -> ( # ` W ) e. ( ZZ>= ` L ) )
5		fzoss2	|- ( ( # ` W ) e. ( ZZ>= ` L ) -> ( 0 ..^ L ) C_ ( 0 ..^ ( # ` W ) ) )
6	3 4 5	3syl	|- ( ph -> ( 0 ..^ L ) C_ ( 0 ..^ ( # ` W ) ) )
7		wrddm	|- ( W e. Word S -> dom W = ( 0 ..^ ( # ` W ) ) )
8	1 7	syl	|- ( ph -> dom W = ( 0 ..^ ( # ` W ) ) )
9	6 8	sseqtrrd	|- ( ph -> ( 0 ..^ L ) C_ dom W )
10		wrdf	|- ( W e. Word S -> W : ( 0 ..^ ( # ` W ) ) --> S )
11	1 10	syl	|- ( ph -> W : ( 0 ..^ ( # ` W ) ) --> S )
12	11 6	fssresd	|- ( ph -> ( W |` ( 0 ..^ L ) ) : ( 0 ..^ L ) --> S )
13		f1resf1	|- ( ( W : dom W -1-1-> S /\ ( 0 ..^ L ) C_ dom W /\ ( W |` ( 0 ..^ L ) ) : ( 0 ..^ L ) --> S ) -> ( W |` ( 0 ..^ L ) ) : ( 0 ..^ L ) -1-1-> S )
14	2 9 12 13	syl3anc	|- ( ph -> ( W |` ( 0 ..^ L ) ) : ( 0 ..^ L ) -1-1-> S )
15		pfxres	|- ( ( W e. Word S /\ L e. ( 0 ... ( # ` W ) ) ) -> ( W prefix L ) = ( W |` ( 0 ..^ L ) ) )
16	1 3 15	syl2anc	|- ( ph -> ( W prefix L ) = ( W |` ( 0 ..^ L ) ) )
17		pfxfn	|- ( ( W e. Word S /\ L e. ( 0 ... ( # ` W ) ) ) -> ( W prefix L ) Fn ( 0 ..^ L ) )
18	1 3 17	syl2anc	|- ( ph -> ( W prefix L ) Fn ( 0 ..^ L ) )
19	18	fndmd	|- ( ph -> dom ( W prefix L ) = ( 0 ..^ L ) )
20		eqidd	|- ( ph -> S = S )
21	16 19 20	f1eq123d	|- ( ph -> ( ( W prefix L ) : dom ( W prefix L ) -1-1-> S <-> ( W |` ( 0 ..^ L ) ) : ( 0 ..^ L ) -1-1-> S ) )
22	14 21	mpbird	|- ( ph -> ( W prefix L ) : dom ( W prefix L ) -1-1-> S )