Theorem seqcl

Description: Closure properties of the recursive sequence builder. (Contributed by Mario Carneiro, 2-Jul-2013) (Revised by Mario Carneiro, 27-May-2014)

	Ref	Expression
Hypotheses	seqcl.1	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
	seqcl.2	$$⊢\left(\phi \wedge x\in \left(M\dots N\right)\right)\to F\left(x\right)\in S$$
	seqcl.3	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\right)\right)\to x\underset{\dot{}}{+}y\in S$$
Assertion	seqcl	$$⊢\phi \to seqM\left(\underset{\dot{}}{+},F\right)\left(N\right)\in S$$

Proof

Step	Hyp	Ref	Expression
1		seqcl.1	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
2		seqcl.2	$$⊢\left(\phi \wedge x\in \left(M\dots N\right)\right)\to F\left(x\right)\in S$$
3		seqcl.3	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\right)\right)\to x\underset{\dot{}}{+}y\in S$$
4		fveq2	$$⊢x=M\to F\left(x\right)=F\left(M\right)$$
5	4	eleq1d	$$⊢x=M\to \left(F\left(x\right)\in S\leftrightarrow F\left(M\right)\in S\right)$$
6	2	ralrimiva	$$⊢\phi \to \forall x\in \left(M\dots N\right)F\left(x\right)\in S$$
7		eluzfz1	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in \left(M\dots N\right)$$
8	1 7	syl	$$⊢\phi \to M\in \left(M\dots N\right)$$
9	5 6 8	rspcdva	$$⊢\phi \to F\left(M\right)\in S$$
10		eluzel2	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in \mathbb{Z}$$
11	1 10	syl	$$⊢\phi \to M\in \mathbb{Z}$$
12		fzp1ss	$$⊢M\in \mathbb{Z}\to \left(M+1\dots N\right)\subseteq \left(M\dots N\right)$$
13	11 12	syl	$$⊢\phi \to \left(M+1\dots N\right)\subseteq \left(M\dots N\right)$$
14	13	sselda	$$⊢\left(\phi \wedge x\in \left(M+1\dots N\right)\right)\to x\in \left(M\dots N\right)$$
15	14 2	syldan	$$⊢\left(\phi \wedge x\in \left(M+1\dots N\right)\right)\to F\left(x\right)\in S$$
16	9 3 1 15	seqcl2	$$⊢\phi \to seqM\left(\underset{\dot{}}{+},F\right)\left(N\right)\in S$$