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

Proof

Step Hyp Ref Expression
1 seqeq1 ⊢ M = if M ∈ ℤ M 0 → seq M + ˙ F = seq if M ∈ ℤ M 0 + ˙ F
2 id ⊢ M = if M ∈ ℤ M 0 → M = if M ∈ ℤ M 0
3 1 2 fveq12d ⊢ M = if M ∈ ℤ M 0 → seq M + ˙ F ⁡ M = seq if M ∈ ℤ M 0 + ˙ F ⁡ if M ∈ ℤ M 0
4 fveq2 ⊢ M = if M ∈ ℤ M 0 → F ⁡ M = F ⁡ if M ∈ ℤ M 0
5 3 4 eqeq12d ⊢ M = if M ∈ ℤ M 0 → seq M + ˙ F ⁡ M = F ⁡ M ↔ seq if M ∈ ℤ M 0 + ˙ F ⁡ if M ∈ ℤ M 0 = F ⁡ if M ∈ ℤ M 0
6 0z ⊢ 0 ∈ ℤ
7 6 elimel ⊢ if M ∈ ℤ M 0 ∈ ℤ
8 eqid ⊢ rec ⁡ x ∈ V ⟼ x + 1 if M ∈ ℤ M 0 ↾ ω = rec ⁡ x ∈ V ⟼ x + 1 if M ∈ ℤ M 0 ↾ ω
9 fvex ⊢ F ⁡ if M ∈ ℤ M 0 ∈ V
10 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 ↾ ω
11 10 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 ↾ ω
12 7 8 9 10 11 uzrdg0i ⊢ seq if M ∈ ℤ M 0 + ˙ F ⁡ if M ∈ ℤ M 0 = F ⁡ if M ∈ ℤ M 0
13 5 12 dedth ⊢ M ∈ ℤ → seq M + ˙ F ⁡ M = F ⁡ M