Theorem 1wlkdlem1

Description: Lemma 1 for 1wlkd . (Contributed by AV, 22-Jan-2021)

	Ref	Expression
Hypotheses	1wlkd.p	|- P = <" X Y ">
	1wlkd.f	|- F = <" J ">
	1wlkd.x	|- ( ph -> X e. V )
	1wlkd.y	|- ( ph -> Y e. V )
Assertion	1wlkdlem1	|- ( ph -> P : ( 0 ... ( # ` F ) ) --> V )

Proof

Step	Hyp	Ref	Expression
1		1wlkd.p	|- P = <" X Y ">
2		1wlkd.f	|- F = <" J ">
3		1wlkd.x	|- ( ph -> X e. V )
4		1wlkd.y	|- ( ph -> Y e. V )
5	3 4	s2cld	|- ( ph -> <" X Y "> e. Word V )
6		wrdf	|- ( <" X Y "> e. Word V -> <" X Y "> : ( 0 ..^ ( # ` <" X Y "> ) ) --> V )
7		1z	|- 1 e. ZZ
8		fzval3	|- ( 1 e. ZZ -> ( 0 ... 1 ) = ( 0 ..^ ( 1 + 1 ) ) )
9	7 8	ax-mp	|- ( 0 ... 1 ) = ( 0 ..^ ( 1 + 1 ) )
10	2	fveq2i	|- ( # ` F ) = ( # ` <" J "> )
11		s1len	|- ( # ` <" J "> ) = 1
12	10 11	eqtri	|- ( # ` F ) = 1
13	12	oveq2i	|- ( 0 ... ( # ` F ) ) = ( 0 ... 1 )
14		s2len	|- ( # ` <" X Y "> ) = 2
15		df-2	|- 2 = ( 1 + 1 )
16	14 15	eqtri	|- ( # ` <" X Y "> ) = ( 1 + 1 )
17	16	oveq2i	|- ( 0 ..^ ( # ` <" X Y "> ) ) = ( 0 ..^ ( 1 + 1 ) )
18	9 13 17	3eqtr4i	|- ( 0 ... ( # ` F ) ) = ( 0 ..^ ( # ` <" X Y "> ) )
19	18	a1i	|- ( <" X Y "> e. Word V -> ( 0 ... ( # ` F ) ) = ( 0 ..^ ( # ` <" X Y "> ) ) )
20	19	feq2d	|- ( <" X Y "> e. Word V -> ( <" X Y "> : ( 0 ... ( # ` F ) ) --> V <-> <" X Y "> : ( 0 ..^ ( # ` <" X Y "> ) ) --> V ) )
21	6 20	mpbird	|- ( <" X Y "> e. Word V -> <" X Y "> : ( 0 ... ( # ` F ) ) --> V )
22	5 21	syl	|- ( ph -> <" X Y "> : ( 0 ... ( # ` F ) ) --> V )
23	1	feq1i	|- ( P : ( 0 ... ( # ` F ) ) --> V <-> <" X Y "> : ( 0 ... ( # ` F ) ) --> V )
24	22 23	sylibr	|- ( ph -> P : ( 0 ... ( # ` F ) ) --> V )