seqfn

Description: The sequence builder function is a function. (Contributed by Mario Carneiro, 24-Jun-2013) (Revised by Mario Carneiro, 15-Sep-2013)

		Ref	Expression
	Assertion	seqfn	$⊢ M \in ℤ \to seq M (\underset{˙}{+}, F) Fn ℤ_{\geq M}$

Step	Hyp	Ref	Expression
1		seqeq1	$⊢ M = if (M \in ℤ, M, 0) \to seq M (\underset{˙}{+}, F) = seq if (M \in ℤ, M, 0) (\underset{˙}{+}, F)$
2		fveq2	$⊢ M = if (M \in ℤ, M, 0) \to ℤ_{\geq M} = ℤ_{\geq if (M \in ℤ, M, 0)}$
3	1 2	fneq12d	$⊢ M = if (M \in ℤ, M, 0) \to (seq M (\underset{˙}{+}, F) Fn ℤ_{\geq M} \leftrightarrow seq if (M \in ℤ, M, 0) (\underset{˙}{+}, F) Fn ℤ_{\geq if (M \in ℤ, M, 0)})$
4		0z	$⊢ 0 \in ℤ$
5	4	elimel	$⊢ if (M \in ℤ, M, 0) \in ℤ$
6		eqid	$⊢ {rec ((x \in V ⟼ x + 1), if (M \in ℤ, M, 0)) ↾}_{ω} = {rec ((x \in V ⟼ x + 1), if (M \in ℤ, M, 0)) ↾}_{ω}$
7		fvex	$⊢ F (if (M \in ℤ, M, 0)) \in V$
8		eqid	$⊢ {rec ((x \in V, y \in V ⟼ ⟨x + 1, x (z \in V, w \in V ⟼ w \underset{˙}{+} F (z + 1)) y⟩), ⟨if (M \in ℤ, M, 0), F (if (M \in ℤ, M, 0))⟩) ↾}_{ω} = {rec ((x \in V, y \in V ⟼ ⟨x + 1, x (z \in V, w \in V ⟼ w \underset{˙}{+} F (z + 1)) y⟩), ⟨if (M \in ℤ, M, 0), F (if (M \in ℤ, M, 0))⟩) ↾}_{ω}$
9	8	seqval	$⊢ seq if (M \in ℤ, M, 0) (\underset{˙}{+}, F) = ran ({rec ((x \in V, y \in V ⟼ ⟨x + 1, x (z \in V, w \in V ⟼ w \underset{˙}{+} F (z + 1)) y⟩), ⟨if (M \in ℤ, M, 0), F (if (M \in ℤ, M, 0))⟩) ↾}_{ω})$
10	5 6 7 8 9	uzrdgfni	$⊢ seq if (M \in ℤ, M, 0) (\underset{˙}{+}, F) Fn ℤ_{\geq if (M \in ℤ, M, 0)}$
11	3 10	dedth	$⊢ M \in ℤ \to seq M (\underset{˙}{+}, F) Fn ℤ_{\geq M}$

Metamath Proof Explorer