This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑅