Theorem subiwrd

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

	Ref	Expression
Hypotheses	iwrdsplit.s	$$⊢\phi \to S\in \mathrm{V}$$
	iwrdsplit.f	$$⊢\phi \to F:{\mathbb{N}}_0⟶S$$
	iwrdsplit.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
Assertion	subiwrd	$$⊢\phi \to {F\upharpoonright }_{\left(0..^N\right)}\in \mathrm{Word}S$$

Proof

Step	Hyp	Ref	Expression
1		iwrdsplit.s	$$⊢\phi \to S\in \mathrm{V}$$
2		iwrdsplit.f	$$⊢\phi \to F:{\mathbb{N}}_0⟶S$$
3		iwrdsplit.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
4		fzo0ssnn0	$$⊢\left(0..^N\right)\subseteq {\mathbb{N}}_0$$
5		fssres	$$⊢\left(F:{\mathbb{N}}_0⟶S\wedge \left(0..^N\right)\subseteq {\mathbb{N}}_0\right)\to \left({F\upharpoonright }_{\left(0..^N\right)}\right):\left(0..^N\right)⟶S$$
6	2 4 5	sylancl	$$⊢\phi \to \left({F\upharpoonright }_{\left(0..^N\right)}\right):\left(0..^N\right)⟶S$$
7		iswrdi	$$⊢\left({F\upharpoonright }_{\left(0..^N\right)}\right):\left(0..^N\right)⟶S\to {F\upharpoonright }_{\left(0..^N\right)}\in \mathrm{Word}S$$
8	6 7	syl	$$⊢\phi \to {F\upharpoonright }_{\left(0..^N\right)}\in \mathrm{Word}S$$