seqf2

Description: Range of the recursive sequence builder. (Contributed by Mario Carneiro, 24-Jun-2013) (Revised by Mario Carneiro, 27-May-2014)

	Ref	Expression
Hypotheses	seqcl2.1	$⊢ φ \to F (M) \in C$
	seqcl2.2	$⊢ (φ \land (x \in C \land y \in D)) \to x \underset{˙}{+} y \in C$
	seqf2.3	$⊢ Z = ℤ_{\geq M}$
	seqf2.4	$⊢ φ \to M \in ℤ$
	seqf2.5	$⊢ (φ \land x \in ℤ_{\geq (M + 1)}) \to F (x) \in D$
Assertion	seqf2	$⊢ φ \to seq M (\underset{˙}{+}, F) : Z ⟶ C$

Step	Hyp	Ref	Expression
1		seqcl2.1	$⊢ φ \to F (M) \in C$
2		seqcl2.2	$⊢ (φ \land (x \in C \land y \in D)) \to x \underset{˙}{+} y \in C$
3		seqf2.3	$⊢ Z = ℤ_{\geq M}$
4		seqf2.4	$⊢ φ \to M \in ℤ$
5		seqf2.5	$⊢ (φ \land x \in ℤ_{\geq (M + 1)}) \to F (x) \in D$
6		seqfn	$⊢ M \in ℤ \to seq M (\underset{˙}{+}, F) Fn ℤ_{\geq M}$
7	4 6	syl	$⊢ φ \to seq M (\underset{˙}{+}, F) Fn ℤ_{\geq M}$
8	1	adantr	$⊢ (φ \land k \in ℤ_{\geq M}) \to F (M) \in C$
9	2	adantlr	$⊢ ((φ \land k \in ℤ_{\geq M}) \land (x \in C \land y \in D)) \to x \underset{˙}{+} y \in C$
10		simpr	$⊢ (φ \land k \in ℤ_{\geq M}) \to k \in ℤ_{\geq M}$
11		elfzuz	$⊢ x \in (M + 1 \dots k) \to x \in ℤ_{\geq (M + 1)}$
12	11 5	sylan2	$⊢ (φ \land x \in (M + 1 \dots k)) \to F (x) \in D$
13	12	adantlr	$⊢ ((φ \land k \in ℤ_{\geq M}) \land x \in (M + 1 \dots k)) \to F (x) \in D$
14	8 9 10 13	seqcl2	$⊢ (φ \land k \in ℤ_{\geq M}) \to seq M (\underset{˙}{+}, F) (k) \in C$
15	14	ralrimiva	$⊢ φ \to \forall k \in ℤ_{\geq M} seq M (\underset{˙}{+}, F) (k) \in C$
16		ffnfv	$⊢ seq M (\underset{˙}{+}, F) : ℤ_{\geq M} ⟶ C \leftrightarrow (seq M (\underset{˙}{+}, F) Fn ℤ_{\geq M} \land \forall k \in ℤ_{\geq M} seq M (\underset{˙}{+}, F) (k) \in C)$
17	7 15 16	sylanbrc	$⊢ φ \to seq M (\underset{˙}{+}, F) : ℤ_{\geq M} ⟶ C$
18	3	feq2i	$⊢ seq M (\underset{˙}{+}, F) : Z ⟶ C \leftrightarrow seq M (\underset{˙}{+}, F) : ℤ_{\geq M} ⟶ C$
19	17 18	sylibr	$⊢ φ \to seq M (\underset{˙}{+}, F) : Z ⟶ C$

Metamath Proof Explorer