pfxf1

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

	Ref	Expression
Hypotheses	pfxf1.1	$⊢ φ \to W \in Word S$
	pfxf1.2	$⊢ φ \to W : dom W \underset{1-1}{⟶} S$
	pfxf1.3	$⊢ φ \to L \in (0 \dots \|W\|)$
Assertion	pfxf1	$⊢ φ \to (W prefix L) : dom (W prefix L) \underset{1-1}{⟶} S$

Step	Hyp	Ref	Expression
1		pfxf1.1	$⊢ φ \to W \in Word S$
2		pfxf1.2	$⊢ φ \to W : dom W \underset{1-1}{⟶} S$
3		pfxf1.3	$⊢ φ \to L \in (0 \dots \|W\|)$
4		elfzuz3	$⊢ L \in (0 \dots \|W\|) \to \|W\| \in ℤ_{\geq L}$
5		fzoss2	$⊢ \|W\| \in ℤ_{\geq L} \to (0 ..^L) \subseteq (0 ..^\|W\|)$
6	3 4 5	3syl	$⊢ φ \to (0 ..^L) \subseteq (0 ..^\|W\|)$
7		wrddm	$⊢ W \in Word S \to dom W = (0 ..^\|W\|)$
8	1 7	syl	$⊢ φ \to dom W = (0 ..^\|W\|)$
9	6 8	sseqtrrd	$⊢ φ \to (0 ..^L) \subseteq dom W$
10		wrdf	$⊢ W \in Word S \to W : (0 ..^\|W\|) ⟶ S$
11	1 10	syl	$⊢ φ \to W : (0 ..^\|W\|) ⟶ S$
12	11 6	fssresd	$⊢ φ \to ({W ↾}_{(0 ..^L)}) : (0 ..^L) ⟶ S$
13		f1resf1	$⊢ (W : dom W \underset{1-1}{⟶} S \land (0 ..^L) \subseteq dom W \land ({W ↾}_{(0 ..^L)}) : (0 ..^L) ⟶ S) \to ({W ↾}_{(0 ..^L)}) : (0 ..^L) \underset{1-1}{⟶} S$
14	2 9 12 13	syl3anc	$⊢ φ \to ({W ↾}_{(0 ..^L)}) : (0 ..^L) \underset{1-1}{⟶} S$
15		pfxres	$⊢ (W \in Word S \land L \in (0 \dots \|W\|)) \to W prefix L = {W ↾}_{(0 ..^L)}$
16	1 3 15	syl2anc	$⊢ φ \to W prefix L = {W ↾}_{(0 ..^L)}$
17		pfxfn	$⊢ (W \in Word S \land L \in (0 \dots \|W\|)) \to (W prefix L) Fn (0 ..^L)$
18	1 3 17	syl2anc	$⊢ φ \to (W prefix L) Fn (0 ..^L)$
19	18	fndmd	$⊢ φ \to dom (W prefix L) = (0 ..^L)$
20		eqidd	$⊢ φ \to S = S$
21	16 19 20	f1eq123d	$⊢ φ \to ((W prefix L) : dom (W prefix L) \underset{1-1}{⟶} S \leftrightarrow ({W ↾}_{(0 ..^L)}) : (0 ..^L) \underset{1-1}{⟶} S)$
22	14 21	mpbird	$⊢ φ \to (W prefix L) : dom (W prefix L) \underset{1-1}{⟶} S$

Metamath Proof Explorer