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	|- ( ph -> W e. Word D )
	wrdf1d.f	|- ( ph -> Fun `' W )
Assertion	wrdf1d	|- ( ph -> W : dom W -1-1-> D )

Proof

Step	Hyp	Ref	Expression
1		wrdf1d.w	|- ( ph -> W e. Word D )
2		wrdf1d.f	|- ( ph -> Fun `' W )
3		wrddm	|- ( W e. Word D -> dom W = ( 0 ..^ ( # ` W ) ) )
4	1 3	syl	|- ( ph -> dom W = ( 0 ..^ ( # ` W ) ) )
5	4	eqcomd	|- ( ph -> ( 0 ..^ ( # ` W ) ) = dom W )
6		wrdf	|- ( W e. Word D -> W : ( 0 ..^ ( # ` W ) ) --> D )
7	1 6	syl	|- ( ph -> W : ( 0 ..^ ( # ` W ) ) --> D )
8	5 7	feq2dd	|- ( ph -> W : dom W --> D )
9		df-f1	|- ( W : dom W -1-1-> D <-> ( W : dom W --> D /\ Fun `' W ) )
10	9	a1i	|- ( ph -> ( W : dom W -1-1-> D <-> ( W : dom W --> D /\ Fun `' W ) ) )
11	8 2 10	mpbir2and	|- ( ph -> W : dom W -1-1-> D )