Theorem subiwrd

Description: Lemma for sseqp1 . (Contributed by Thierry Arnoux, 25-Apr-2019)

	Ref	Expression
Hypotheses	iwrdsplit.s	|- ( ph -> S e. _V )
	iwrdsplit.f	|- ( ph -> F : NN0 --> S )
	iwrdsplit.n	|- ( ph -> N e. NN0 )
Assertion	subiwrd	|- ( ph -> ( F |` ( 0 ..^ N ) ) e. Word S )

Proof

Step	Hyp	Ref	Expression
1		iwrdsplit.s	|- ( ph -> S e. _V )
2		iwrdsplit.f	|- ( ph -> F : NN0 --> S )
3		iwrdsplit.n	|- ( ph -> N e. NN0 )
4		fzo0ssnn0	|- ( 0 ..^ N ) C_ NN0
5		fssres	|- ( ( F : NN0 --> S /\ ( 0 ..^ N ) C_ NN0 ) -> ( F |` ( 0 ..^ N ) ) : ( 0 ..^ N ) --> S )
6	2 4 5	sylancl	|- ( ph -> ( F |` ( 0 ..^ N ) ) : ( 0 ..^ N ) --> S )
7		iswrdi	|- ( ( F |` ( 0 ..^ N ) ) : ( 0 ..^ N ) --> S -> ( F |` ( 0 ..^ N ) ) e. Word S )
8	6 7	syl	|- ( ph -> ( F |` ( 0 ..^ N ) ) e. Word S )