Theorem wlkdlem3

Description: Lemma 3 for wlkd . (Contributed by Alexander van der Vekens, 10-Nov-2017) (Revised by AV, 7-Feb-2021)

	Ref	Expression
Hypotheses	wlkd.p	|- ( ph -> P e. Word _V )
	wlkd.f	|- ( ph -> F e. Word _V )
	wlkd.l	|- ( ph -> ( # ` P ) = ( ( # ` F ) + 1 ) )
	wlkd.e	|- ( ph -> A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) )
Assertion	wlkdlem3	|- ( ph -> F e. Word dom I )

Proof

Step	Hyp	Ref	Expression
1		wlkd.p	|- ( ph -> P e. Word _V )
2		wlkd.f	|- ( ph -> F e. Word _V )
3		wlkd.l	|- ( ph -> ( # ` P ) = ( ( # ` F ) + 1 ) )
4		wlkd.e	|- ( ph -> A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) )
5	1 2 3 4	wlkdlem2	|- ( ph -> ( ( ( # ` F ) e. NN -> ( P ` ( # ` F ) ) e. ( I ` ( F ` ( ( # ` F ) - 1 ) ) ) ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) e. ( I ` ( F ` k ) ) ) )
6		elfvdm	|- ( ( P ` k ) e. ( I ` ( F ` k ) ) -> ( F ` k ) e. dom I )
7	6	ralimi	|- ( A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) e. ( I ` ( F ` k ) ) -> A. k e. ( 0 ..^ ( # ` F ) ) ( F ` k ) e. dom I )
8	5 7	simpl2im	|- ( ph -> A. k e. ( 0 ..^ ( # ` F ) ) ( F ` k ) e. dom I )
9		iswrdsymb	|- ( ( F e. Word _V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( F ` k ) e. dom I ) -> F e. Word dom I )
10	2 8 9	syl2anc	|- ( ph -> F e. Word dom I )