Metamath Proof Explorer

Theorem seq1

Description: Value of the sequence builder function at its initial value. (Contributed by Mario Carneiro, 24-Jun-2013) (Revised by Mario Carneiro, 15-Sep-2013)

		Ref	Expression
	Assertion	seq1	$⊢ M \in ℤ \to seq M (\underset{˙}{+}, F) (M) = F (M)$

Proof

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		id	$⊢ M = if (M \in ℤ, M, 0) \to M = if (M \in ℤ, M, 0)$
3	1 2	fveq12d	$⊢ M = if (M \in ℤ, M, 0) \to seq M (\underset{˙}{+}, F) (M) = seq if (M \in ℤ, M, 0) (\underset{˙}{+}, F) (if (M \in ℤ, M, 0))$
4		fveq2	$⊢ M = if (M \in ℤ, M, 0) \to F (M) = F (if (M \in ℤ, M, 0))$
5	3 4	eqeq12d	$⊢ M = if (M \in ℤ, M, 0) \to (seq M (\underset{˙}{+}, F) (M) = F (M) \leftrightarrow seq if (M \in ℤ, M, 0) (\underset{˙}{+}, F) (if (M \in ℤ, M, 0)) = F (if (M \in ℤ, M, 0)))$
6		0z	$⊢ 0 \in ℤ$
7	6	elimel	$⊢ if (M \in ℤ, M, 0) \in ℤ$
8		eqid	$⊢ {rec ((x \in V ⟼ x + 1), if (M \in ℤ, M, 0)) ↾}_{ω} = {rec ((x \in V ⟼ x + 1), if (M \in ℤ, M, 0)) ↾}_{ω}$
9		fvex	$⊢ F (if (M \in ℤ, M, 0)) \in V$
10		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))⟩) ↾}_{ω}$
11	10	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))⟩) ↾}_{ω})$
12	7 8 9 10 11	uzrdg0i	$⊢ seq if (M \in ℤ, M, 0) (\underset{˙}{+}, F) (if (M \in ℤ, M, 0)) = F (if (M \in ℤ, M, 0))$
13	5 12	dedth	$⊢ M \in ℤ \to seq M (\underset{˙}{+}, F) (M) = F (M)$