Metamath Proof Explorer

Theorem seqval

Description: Value of the sequence builder function. (Contributed by Mario Carneiro, 24-Jun-2013)

		Ref	Expression
	Hypothesis	seqval.1	$⊢ R = {rec ((x \in V, y \in V ⟼ ⟨x + 1, x (z \in V, w \in V ⟼ w \underset{˙}{+} F (z + 1)) y⟩), ⟨M, F (M)⟩) ↾}_{ω}$
	Assertion	seqval	$⊢ seq M (\underset{˙}{+}, F) = ran R$

Proof

Step	Hyp	Ref	Expression
1		seqval.1	$⊢ R = {rec ((x \in V, y \in V ⟼ ⟨x + 1, x (z \in V, w \in V ⟼ w \underset{˙}{+} F (z + 1)) y⟩), ⟨M, F (M)⟩) ↾}_{ω}$
2		df-ima	$⊢ rec ((x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} F (x + 1)⟩), ⟨M, F (M)⟩) [ω] = ran ({rec ((x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} F (x + 1)⟩), ⟨M, F (M)⟩) ↾}_{ω})$
3		df-seq	$⊢ seq M (\underset{˙}{+}, F) = rec ((x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} F (x + 1)⟩), ⟨M, F (M)⟩) [ω]$
4		eqid	$⊢ V = V$
5		fvoveq1	$⊢ z = x \to F (z + 1) = F (x + 1)$
6	5	oveq2d	$⊢ z = x \to w \underset{˙}{+} F (z + 1) = w \underset{˙}{+} F (x + 1)$
7		oveq1	$⊢ w = y \to w \underset{˙}{+} F (x + 1) = y \underset{˙}{+} F (x + 1)$
8		eqid	$⊢ (z \in V, w \in V ⟼ w \underset{˙}{+} F (z + 1)) = (z \in V, w \in V ⟼ w \underset{˙}{+} F (z + 1))$
9		ovex	$⊢ y \underset{˙}{+} F (x + 1) \in V$
10	6 7 8 9	ovmpo	$⊢ (x \in V \land y \in V) \to x (z \in V, w \in V ⟼ w \underset{˙}{+} F (z + 1)) y = y \underset{˙}{+} F (x + 1)$
11	10	el2v	$⊢ x (z \in V, w \in V ⟼ w \underset{˙}{+} F (z + 1)) y = y \underset{˙}{+} F (x + 1)$
12	11	opeq2i	$⊢ ⟨x + 1, x (z \in V, w \in V ⟼ w \underset{˙}{+} F (z + 1)) y⟩ = ⟨x + 1, y \underset{˙}{+} F (x + 1)⟩$
13	4 4 12	mpoeq123i	$⊢ (x \in V, y \in V ⟼ ⟨x + 1, x (z \in V, w \in V ⟼ w \underset{˙}{+} F (z + 1)) y⟩) = (x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} F (x + 1)⟩)$
14		rdgeq1	$⊢ (x \in V, y \in V ⟼ ⟨x + 1, x (z \in V, w \in V ⟼ w \underset{˙}{+} F (z + 1)) y⟩) = (x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} F (x + 1)⟩) \to rec ((x \in V, y \in V ⟼ ⟨x + 1, x (z \in V, w \in V ⟼ w \underset{˙}{+} F (z + 1)) y⟩), ⟨M, F (M)⟩) = rec ((x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} F (x + 1)⟩), ⟨M, F (M)⟩)$
15	13 14	ax-mp	$⊢ rec ((x \in V, y \in V ⟼ ⟨x + 1, x (z \in V, w \in V ⟼ w \underset{˙}{+} F (z + 1)) y⟩), ⟨M, F (M)⟩) = rec ((x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} F (x + 1)⟩), ⟨M, F (M)⟩)$
16	15	reseq1i	$⊢ {rec ((x \in V, y \in V ⟼ ⟨x + 1, x (z \in V, w \in V ⟼ w \underset{˙}{+} F (z + 1)) y⟩), ⟨M, F (M)⟩) ↾}_{ω} = {rec ((x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} F (x + 1)⟩), ⟨M, F (M)⟩) ↾}_{ω}$
17	1 16	eqtri	$⊢ R = {rec ((x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} F (x + 1)⟩), ⟨M, F (M)⟩) ↾}_{ω}$
18	17	rneqi	$⊢ ran R = ran ({rec ((x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} F (x + 1)⟩), ⟨M, F (M)⟩) ↾}_{ω})$
19	2 3 18	3eqtr4i	$⊢ seq M (\underset{˙}{+}, F) = ran R$