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

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 ( 𝑀 ∈ ℤ → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 seqeq1 ⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → seq 𝑀 ( + , 𝐹 ) = seq if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ( + , 𝐹 ) )
2 id ⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) )
3 1 2 fveq12d ⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) = ( seq if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ( + , 𝐹 ) ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) )
4 fveq2 ⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → ( 𝐹 ‘ 𝑀 ) = ( 𝐹 ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) )
5 3 4 eqeq12d ⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) ↔ ( seq if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ( + , 𝐹 ) ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) = ( 𝐹 ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ) )
6 0z ⊢ 0 ∈ ℤ
7 6 elimel ⊢ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ∈ ℤ
8 eqid ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ↾ ω )
9 fvex ⊢ ( 𝐹 ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ∈ V
10 eqid ⊢ ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) 𝑦 ) ⟩ ) , ⟨ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) , ( 𝐹 ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ⟩ ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) 𝑦 ) ⟩ ) , ⟨ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) , ( 𝐹 ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ⟩ ) ↾ ω )
11 10 seqval ⊢ seq if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ( + , 𝐹 ) = ran ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) 𝑦 ) ⟩ ) , ⟨ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) , ( 𝐹 ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ⟩ ) ↾ ω )
12 7 8 9 10 11 uzrdg0i ⊢ ( seq if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ( + , 𝐹 ) ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) = ( 𝐹 ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) )
13 5 12 dedth ⊢ ( 𝑀 ∈ ℤ → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) )