# Metamath Proof Explorer

## Theorem seqfn

Description: The sequence builder function is a function. (Contributed by Mario Carneiro, 24-Jun-2013) (Revised by Mario Carneiro, 15-Sep-2013)

Ref Expression
Assertion seqfn ( 𝑀 ∈ ℤ → seq 𝑀 ( + , 𝐹 ) Fn ( ℤ𝑀 ) )

### Proof

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