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 ⊢ M ∈ ℤ → seq M + ˙ F Fn ℤ ≥ M

Proof

Step Hyp Ref Expression
1 seqeq1 ⊢ M = if M ∈ ℤ M 0 → seq M + ˙ F = seq if M ∈ ℤ M 0 + ˙ F
2 fveq2 ⊢ M = if M ∈ ℤ M 0 → ℤ ≥ M = ℤ ≥ if M ∈ ℤ M 0
3 1 2 fneq12d ⊢ M = if M ∈ ℤ M 0 → seq M + ˙ F Fn ℤ ≥ M ↔ seq if M ∈ ℤ M 0 + ˙ F Fn ℤ ≥ if M ∈ ℤ M 0
4 0z ⊢ 0 ∈ ℤ
5 4 elimel ⊢ if M ∈ ℤ M 0 ∈ ℤ
6 eqid ⊢ rec ⁡ x ∈ V ⟼ x + 1 if M ∈ ℤ M 0 ↾ ω = rec ⁡ x ∈ V ⟼ x + 1 if M ∈ ℤ M 0 ↾ ω
7 fvex ⊢ F ⁡ if M ∈ ℤ M 0 ∈ V
8 eqid ⊢ rec ⁡ x ∈ V , y ∈ V ⟼ x + 1 x z ∈ V , w ∈ V ⟼ w + ˙ F ⁡ z + 1 y if M ∈ ℤ M 0 F ⁡ if M ∈ ℤ M 0 ↾ ω = rec ⁡ x ∈ V , y ∈ V ⟼ x + 1 x z ∈ V , w ∈ V ⟼ w + ˙ F ⁡ z + 1 y if M ∈ ℤ M 0 F ⁡ if M ∈ ℤ M 0 ↾ ω
9 8 seqval ⊢ seq if M ∈ ℤ M 0 + ˙ F = ran ⁡ rec ⁡ x ∈ V , y ∈ V ⟼ x + 1 x z ∈ V , w ∈ V ⟼ w + ˙ F ⁡ z + 1 y if M ∈ ℤ M 0 F ⁡ if M ∈ ℤ M 0 ↾ ω
10 5 6 7 8 9 uzrdgfni ⊢ seq if M ∈ ℤ M 0 + ˙ F Fn ℤ ≥ if M ∈ ℤ M 0
11 3 10 dedth ⊢ M ∈ ℤ → seq M + ˙ F Fn ℤ ≥ M