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 = ℤ_{\geq M}$
	seqf.2	$⊢ φ \to M \in ℤ$
	seqf.3	$⊢ (φ \land x \in Z) \to F (x) \in S$
	seqf.4	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
Assertion	seqf	$⊢ φ \to seq M (\underset{˙}{+}, F) : Z ⟶ S$

Step	Hyp	Ref	Expression
1		seqf.1	$⊢ Z = ℤ_{\geq M}$
2		seqf.2	$⊢ φ \to M \in ℤ$
3		seqf.3	$⊢ (φ \land x \in Z) \to F (x) \in S$
4		seqf.4	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
5		fveq2	$⊢ x = M \to F (x) = F (M)$
6	5	eleq1d	$⊢ x = M \to (F (x) \in S \leftrightarrow F (M) \in S)$
7	3	ralrimiva	$⊢ φ \to \forall x \in Z F (x) \in S$
8		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
9	2 8	syl	$⊢ φ \to M \in ℤ_{\geq M}$
10	9 1	eleqtrrdi	$⊢ φ \to M \in Z$
11	6 7 10	rspcdva	$⊢ φ \to F (M) \in S$
12		peano2uzr	$⊢ (M \in ℤ \land x \in ℤ_{\geq (M + 1)}) \to x \in ℤ_{\geq M}$
13	2 12	sylan	$⊢ (φ \land x \in ℤ_{\geq (M + 1)}) \to x \in ℤ_{\geq M}$
14	13 1	eleqtrrdi	$⊢ (φ \land x \in ℤ_{\geq (M + 1)}) \to x \in Z$
15	14 3	syldan	$⊢ (φ \land x \in ℤ_{\geq (M + 1)}) \to F (x) \in S$
16	11 4 1 2 15	seqf2	$⊢ φ \to seq M (\underset{˙}{+}, F) : Z ⟶ S$

Metamath Proof Explorer