Theorem seqf

Description: Range of the recursive sequence builder (special case of seqf2 ). (Contributed by Mario Carneiro, 24-Jun-2013)

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

Proof

Step	Hyp	Ref	Expression
1		seqf.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		seqf.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		seqf.3	$$⊢\left(\phi \wedge x\in Z\right)\to F\left(x\right)\in S$$
4		seqf.4	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\right)\right)\to x\underset{\dot{}}{+}y\in S$$
5		fveq2	$$⊢x=M\to F\left(x\right)=F\left(M\right)$$
6	5	eleq1d	$$⊢x=M\to \left(F\left(x\right)\in S\leftrightarrow F\left(M\right)\in S\right)$$
7	3	ralrimiva	$$⊢\phi \to \forall x\in ZF\left(x\right)\in S$$
8		uzid	$$⊢M\in \mathbb{Z}\to M\in {\mathbb{Z}}_{\ge M}$$
9	2 8	syl	$$⊢\phi \to M\in {\mathbb{Z}}_{\ge M}$$
10	9 1	eleqtrrdi	$$⊢\phi \to M\in Z$$
11	6 7 10	rspcdva	$$⊢\phi \to F\left(M\right)\in S$$
12		peano2uzr	$$⊢\left(M\in \mathbb{Z}\wedge x\in {\mathbb{Z}}_{\ge \left(M+1\right)}\right)\to x\in {\mathbb{Z}}_{\ge M}$$
13	2 12	sylan	$$⊢\left(\phi \wedge x\in {\mathbb{Z}}_{\ge \left(M+1\right)}\right)\to x\in {\mathbb{Z}}_{\ge M}$$
14	13 1	eleqtrrdi	$$⊢\left(\phi \wedge x\in {\mathbb{Z}}_{\ge \left(M+1\right)}\right)\to x\in Z$$
15	14 3	syldan	$$⊢\left(\phi \wedge x\in {\mathbb{Z}}_{\ge \left(M+1\right)}\right)\to F\left(x\right)\in S$$
16	11 4 1 2 15	seqf2	$$⊢\phi \to seqM\left(\underset{\dot{}}{+},F\right):Z⟶S$$