Theorem wrdf1d

Description: A one-to-one word maps its domain into its alphabet. (Contributed by Mingli Yuan, 11-Aug-2026)

	Ref	Expression
Hypotheses	wrdf1d.w	$$⊢\phi \to W\in \mathrm{Word}D$$
	wrdf1d.f	$$⊢\phi \to \mathrm{Fun}{W}^{-1}$$
Assertion	wrdf1d	$$⊢\phi \to W:\mathrm{dom}W\underset{1-1}{⟶}D$$

Proof

Step	Hyp	Ref	Expression
1		wrdf1d.w	$$⊢\phi \to W\in \mathrm{Word}D$$
2		wrdf1d.f	$$⊢\phi \to \mathrm{Fun}{W}^{-1}$$
3		wrddm	$$⊢W\in \mathrm{Word}D\to \mathrm{dom}W=\left(0..^\left|W\right|\right)$$
4	1 3	syl	$$⊢\phi \to \mathrm{dom}W=\left(0..^\left|W\right|\right)$$
5	4	eqcomd	$$⊢\phi \to \left(0..^\left|W\right|\right)=\mathrm{dom}W$$
6		wrdf	$$⊢W\in \mathrm{Word}D\to W:\left(0..^\left|W\right|\right)⟶D$$
7	1 6	syl	$$⊢\phi \to W:\left(0..^\left|W\right|\right)⟶D$$
8	5 7	feq2dd	$$⊢\phi \to W:\mathrm{dom}W⟶D$$
9		df-f1	$$⊢W:\mathrm{dom}W\underset{1-1}{⟶}D\leftrightarrow \left(W:\mathrm{dom}W⟶D\wedge \mathrm{Fun}{W}^{-1}\right)$$
10	9	a1i	$$⊢\phi \to \left(W:\mathrm{dom}W\underset{1-1}{⟶}D\leftrightarrow \left(W:\mathrm{dom}W⟶D\wedge \mathrm{Fun}{W}^{-1}\right)\right)$$
11	8 2 10	mpbir2and	$$⊢\phi \to W:\mathrm{dom}W\underset{1-1}{⟶}D$$