Theorem seqval

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

	Ref	Expression
Hypothesis	seqval.1	⊢ 𝑅 = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) 𝑦 ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) ↾ ω )
Assertion	seqval	⊢ seq 𝑀 ( + , 𝐹 ) = ran 𝑅

Proof

Step	Hyp	Ref	Expression
1		seqval.1	⊢ 𝑅 = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) 𝑦 ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) ↾ ω )
2		df-ima	⊢ ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) “ ω ) = ran ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) ↾ ω )
3		df-seq	⊢ seq 𝑀 ( + , 𝐹 ) = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) “ ω )
4		eqid	⊢ V = V
5		fvoveq1	⊢ ( 𝑧 = 𝑥 → ( 𝐹 ‘ ( 𝑧 + 1 ) ) = ( 𝐹 ‘ ( 𝑥 + 1 ) ) )
6	5	oveq2d	⊢ ( 𝑧 = 𝑥 → ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) = ( 𝑤 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) )
7		oveq1	⊢ ( 𝑤 = 𝑦 → ( 𝑤 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) = ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) )
8		eqid	⊢ ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) = ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) )
9		ovex	⊢ ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ∈ V
10	6 7 8 9	ovmpo	⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) 𝑦 ) = ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) )
11	10	el2v	⊢ ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) 𝑦 ) = ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) )
12	11	opeq2i	⊢ ⟨ ( 𝑥 + 1 ) , ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) 𝑦 ) ⟩ = ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩
13	4 4 12	mpoeq123i	⊢ ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) 𝑦 ) ⟩ ) = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ )
14		rdgeq1	⊢ ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) 𝑦 ) ⟩ ) = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) → rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) 𝑦 ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) = rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) )
15	13 14	ax-mp	⊢ rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) 𝑦 ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) = rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ )
16	15	reseq1i	⊢ ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) 𝑦 ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) ↾ ω )
17	1 16	eqtri	⊢ 𝑅 = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) ↾ ω )
18	17	rneqi	⊢ ran 𝑅 = ran ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) ↾ ω )
19	2 3 18	3eqtr4i	⊢ seq 𝑀 ( + , 𝐹 ) = ran 𝑅