| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | seqexw.2 | . . . 4
⊢ 𝑀 ∈ ℤ | 
| 2 |  | seqfn 14055 | . . . 4
⊢ (𝑀 ∈ ℤ → seq𝑀( + , 𝐹) Fn (ℤ≥‘𝑀)) | 
| 3 | 1, 2 | ax-mp 5 | . . 3
⊢ seq𝑀( + , 𝐹) Fn (ℤ≥‘𝑀) | 
| 4 |  | fnfun 6667 | . . 3
⊢ (seq𝑀( + , 𝐹) Fn (ℤ≥‘𝑀) → Fun seq𝑀( + , 𝐹)) | 
| 5 | 3, 4 | ax-mp 5 | . 2
⊢ Fun
seq𝑀( + , 𝐹) | 
| 6 | 3 | fndmi 6671 | . . 3
⊢ dom
seq𝑀( + , 𝐹) = (ℤ≥‘𝑀) | 
| 7 |  | fvex 6918 | . . 3
⊢
(ℤ≥‘𝑀) ∈ V | 
| 8 | 6, 7 | eqeltri 2836 | . 2
⊢ dom
seq𝑀( + , 𝐹) ∈ V | 
| 9 |  | seqexw.1 | . . . . 5
⊢  + ∈
V | 
| 10 | 9 | rnex 7933 | . . . 4
⊢ ran + ∈
V | 
| 11 |  | prex 5436 | . . . 4
⊢ {∅,
(𝐹‘𝑀)} ∈ V | 
| 12 | 10, 11 | unex 7765 | . . 3
⊢ (ran
+ ∪
{∅, (𝐹‘𝑀)}) ∈ V | 
| 13 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑦 = 𝑀 → (seq𝑀( + , 𝐹)‘𝑦) = (seq𝑀( + , 𝐹)‘𝑀)) | 
| 14 | 13 | eleq1d 2825 | . . . . . 6
⊢ (𝑦 = 𝑀 → ((seq𝑀( + , 𝐹)‘𝑦) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}) ↔ (seq𝑀( + , 𝐹)‘𝑀) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}))) | 
| 15 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑦 = 𝑧 → (seq𝑀( + , 𝐹)‘𝑦) = (seq𝑀( + , 𝐹)‘𝑧)) | 
| 16 | 15 | eleq1d 2825 | . . . . . 6
⊢ (𝑦 = 𝑧 → ((seq𝑀( + , 𝐹)‘𝑦) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}) ↔ (seq𝑀( + , 𝐹)‘𝑧) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}))) | 
| 17 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑦 = (𝑧 + 1) → (seq𝑀( + , 𝐹)‘𝑦) = (seq𝑀( + , 𝐹)‘(𝑧 + 1))) | 
| 18 | 17 | eleq1d 2825 | . . . . . 6
⊢ (𝑦 = (𝑧 + 1) → ((seq𝑀( + , 𝐹)‘𝑦) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}) ↔ (seq𝑀( + , 𝐹)‘(𝑧 + 1)) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}))) | 
| 19 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑦 = 𝑥 → (seq𝑀( + , 𝐹)‘𝑦) = (seq𝑀( + , 𝐹)‘𝑥)) | 
| 20 | 19 | eleq1d 2825 | . . . . . 6
⊢ (𝑦 = 𝑥 → ((seq𝑀( + , 𝐹)‘𝑦) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}) ↔ (seq𝑀( + , 𝐹)‘𝑥) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}))) | 
| 21 |  | seq1 14056 | . . . . . . 7
⊢ (𝑀 ∈ ℤ → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀)) | 
| 22 |  | ssun2 4178 | . . . . . . . 8
⊢ {∅,
(𝐹‘𝑀)} ⊆ (ran + ∪ {∅, (𝐹‘𝑀)}) | 
| 23 |  | fvex 6918 | . . . . . . . . 9
⊢ (𝐹‘𝑀) ∈ V | 
| 24 | 23 | prid2 4762 | . . . . . . . 8
⊢ (𝐹‘𝑀) ∈ {∅, (𝐹‘𝑀)} | 
| 25 | 22, 24 | sselii 3979 | . . . . . . 7
⊢ (𝐹‘𝑀) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}) | 
| 26 | 21, 25 | eqeltrdi 2848 | . . . . . 6
⊢ (𝑀 ∈ ℤ → (seq𝑀( + , 𝐹)‘𝑀) ∈ (ran + ∪ {∅, (𝐹‘𝑀)})) | 
| 27 |  | seqp1 14058 | . . . . . . . . 9
⊢ (𝑧 ∈
(ℤ≥‘𝑀) → (seq𝑀( + , 𝐹)‘(𝑧 + 1)) = ((seq𝑀( + , 𝐹)‘𝑧) + (𝐹‘(𝑧 + 1)))) | 
| 28 | 27 | adantr 480 | . . . . . . . 8
⊢ ((𝑧 ∈
(ℤ≥‘𝑀) ∧ (seq𝑀( + , 𝐹)‘𝑧) ∈ (ran + ∪ {∅, (𝐹‘𝑀)})) → (seq𝑀( + , 𝐹)‘(𝑧 + 1)) = ((seq𝑀( + , 𝐹)‘𝑧) + (𝐹‘(𝑧 + 1)))) | 
| 29 |  | df-ov 7435 | . . . . . . . . . 10
⊢
((seq𝑀( + , 𝐹)‘𝑧) + (𝐹‘(𝑧 + 1))) = ( + ‘〈(seq𝑀( + , 𝐹)‘𝑧), (𝐹‘(𝑧 + 1))〉) | 
| 30 |  | snsspr1 4813 | . . . . . . . . . . . 12
⊢ {∅}
⊆ {∅, (𝐹‘𝑀)} | 
| 31 |  | unss2 4186 | . . . . . . . . . . . 12
⊢
({∅} ⊆ {∅, (𝐹‘𝑀)} → (ran + ∪ {∅}) ⊆
(ran +
∪ {∅, (𝐹‘𝑀)})) | 
| 32 | 30, 31 | ax-mp 5 | . . . . . . . . . . 11
⊢ (ran
+ ∪
{∅}) ⊆ (ran + ∪ {∅, (𝐹‘𝑀)}) | 
| 33 |  | fvrn0 6935 | . . . . . . . . . . 11
⊢ ( +
‘〈(seq𝑀( + , 𝐹)‘𝑧), (𝐹‘(𝑧 + 1))〉) ∈ (ran + ∪
{∅}) | 
| 34 | 32, 33 | sselii 3979 | . . . . . . . . . 10
⊢ ( +
‘〈(seq𝑀( + , 𝐹)‘𝑧), (𝐹‘(𝑧 + 1))〉) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}) | 
| 35 | 29, 34 | eqeltri 2836 | . . . . . . . . 9
⊢
((seq𝑀( + , 𝐹)‘𝑧) + (𝐹‘(𝑧 + 1))) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}) | 
| 36 | 35 | a1i 11 | . . . . . . . 8
⊢ ((𝑧 ∈
(ℤ≥‘𝑀) ∧ (seq𝑀( + , 𝐹)‘𝑧) ∈ (ran + ∪ {∅, (𝐹‘𝑀)})) → ((seq𝑀( + , 𝐹)‘𝑧) + (𝐹‘(𝑧 + 1))) ∈ (ran + ∪ {∅, (𝐹‘𝑀)})) | 
| 37 | 28, 36 | eqeltrd 2840 | . . . . . . 7
⊢ ((𝑧 ∈
(ℤ≥‘𝑀) ∧ (seq𝑀( + , 𝐹)‘𝑧) ∈ (ran + ∪ {∅, (𝐹‘𝑀)})) → (seq𝑀( + , 𝐹)‘(𝑧 + 1)) ∈ (ran + ∪ {∅, (𝐹‘𝑀)})) | 
| 38 | 37 | ex 412 | . . . . . 6
⊢ (𝑧 ∈
(ℤ≥‘𝑀) → ((seq𝑀( + , 𝐹)‘𝑧) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}) → (seq𝑀( + , 𝐹)‘(𝑧 + 1)) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}))) | 
| 39 | 14, 16, 18, 20, 26, 38 | uzind4 12949 | . . . . 5
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → (seq𝑀( + , 𝐹)‘𝑥) ∈ (ran + ∪ {∅, (𝐹‘𝑀)})) | 
| 40 | 39 | rgen 3062 | . . . 4
⊢
∀𝑥 ∈
(ℤ≥‘𝑀)(seq𝑀( + , 𝐹)‘𝑥) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}) | 
| 41 |  | fnfvrnss 7140 | . . . 4
⊢
((seq𝑀( + , 𝐹) Fn
(ℤ≥‘𝑀) ∧ ∀𝑥 ∈ (ℤ≥‘𝑀)(seq𝑀( + , 𝐹)‘𝑥) ∈ (ran + ∪ {∅, (𝐹‘𝑀)})) → ran seq𝑀( + , 𝐹) ⊆ (ran + ∪ {∅, (𝐹‘𝑀)})) | 
| 42 | 3, 40, 41 | mp2an 692 | . . 3
⊢ ran
seq𝑀( + , 𝐹) ⊆ (ran + ∪ {∅, (𝐹‘𝑀)}) | 
| 43 | 12, 42 | ssexi 5321 | . 2
⊢ ran
seq𝑀( + , 𝐹) ∈ V | 
| 44 |  | funexw 7977 | . 2
⊢ ((Fun
seq𝑀( + , 𝐹) ∧ dom seq𝑀( + , 𝐹) ∈ V ∧ ran seq𝑀( + , 𝐹) ∈ V) → seq𝑀( + , 𝐹) ∈ V) | 
| 45 | 5, 8, 43, 44 | mp3an 1462 | 1
⊢ seq𝑀( + , 𝐹) ∈ V |