Theorem subiwrd

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

	Ref	Expression
Hypotheses	iwrdsplit.s	⊢ ( 𝜑 → 𝑆 ∈ V )
	iwrdsplit.f	⊢ ( 𝜑 → 𝐹 : ℕ0 ⟶ 𝑆 )
	iwrdsplit.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	subiwrd	⊢ ( 𝜑 → ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ∈ Word 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		iwrdsplit.s	⊢ ( 𝜑 → 𝑆 ∈ V )
2		iwrdsplit.f	⊢ ( 𝜑 → 𝐹 : ℕ0 ⟶ 𝑆 )
3		iwrdsplit.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
4		fzo0ssnn0	⊢ ( 0 ..^ 𝑁 ) ⊆ ℕ0
5		fssres	⊢ ( ( 𝐹 : ℕ0 ⟶ 𝑆 ∧ ( 0 ..^ 𝑁 ) ⊆ ℕ0 ) → ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) : ( 0 ..^ 𝑁 ) ⟶ 𝑆 )
6	2 4 5	sylancl	⊢ ( 𝜑 → ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) : ( 0 ..^ 𝑁 ) ⟶ 𝑆 )
7		iswrdi	⊢ ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) : ( 0 ..^ 𝑁 ) ⟶ 𝑆 → ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ∈ Word 𝑆 )
8	6 7	syl	⊢ ( 𝜑 → ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ∈ Word 𝑆 )