Theorem subiwrdlen

Description: Length of a subword of an infinite word. (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	subiwrdlen	$$⊢\phi \to \left|{F\upharpoonright }_{\left(0..^N\right)}\right|=N$$

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	2	ffnd	$$⊢\phi \to FFn{\mathbb{N}}_0$$
5		fzo0ssnn0	$$⊢\left(0..^N\right)\subseteq {\mathbb{N}}_0$$
6		fnssres	$$⊢\left(FFn{\mathbb{N}}_0\wedge \left(0..^N\right)\subseteq {\mathbb{N}}_0\right)\to \left({F\upharpoonright }_{\left(0..^N\right)}\right)Fn\left(0..^N\right)$$
7	4 5 6	sylancl	$$⊢\phi \to \left({F\upharpoonright }_{\left(0..^N\right)}\right)Fn\left(0..^N\right)$$
8		hashfn	$$⊢\left({F\upharpoonright }_{\left(0..^N\right)}\right)Fn\left(0..^N\right)\to \left|{F\upharpoonright }_{\left(0..^N\right)}\right|=\left|\left(0..^N\right)\right|$$
9	7 8	syl	$$⊢\phi \to \left|{F\upharpoonright }_{\left(0..^N\right)}\right|=\left|\left(0..^N\right)\right|$$
10		hashfzo0	$$⊢N\in {\mathbb{N}}_0\to \left|\left(0..^N\right)\right|=N$$
11	3 10	syl	$$⊢\phi \to \left|\left(0..^N\right)\right|=N$$
12	9 11	eqtrd	$$⊢\phi \to \left|{F\upharpoonright }_{\left(0..^N\right)}\right|=N$$