Step | Hyp | Ref
| Expression |
1 | | seqexw.2 |
. . . 4
⊢ 𝑀 ∈ ℤ |
2 | | seqfn 13382 |
. . . 4
⊢ (𝑀 ∈ ℤ → seq𝑀( + , 𝐹) Fn (ℤ≥‘𝑀)) |
3 | 1, 2 | ax-mp 5 |
. . 3
⊢ seq𝑀( + , 𝐹) Fn (ℤ≥‘𝑀) |
4 | | fnfun 6453 |
. . 3
⊢ (seq𝑀( + , 𝐹) Fn (ℤ≥‘𝑀) → Fun seq𝑀( + , 𝐹)) |
5 | 3, 4 | ax-mp 5 |
. 2
⊢ Fun
seq𝑀( + , 𝐹) |
6 | | fndm 6455 |
. . . 4
⊢ (seq𝑀( + , 𝐹) Fn (ℤ≥‘𝑀) → dom seq𝑀( + , 𝐹) = (ℤ≥‘𝑀)) |
7 | 3, 6 | ax-mp 5 |
. . 3
⊢ dom
seq𝑀( + , 𝐹) = (ℤ≥‘𝑀) |
8 | | fvex 6683 |
. . 3
⊢
(ℤ≥‘𝑀) ∈ V |
9 | 7, 8 | eqeltri 2909 |
. 2
⊢ dom
seq𝑀( + , 𝐹) ∈ V |
10 | | seqexw.1 |
. . . . 5
⊢ + ∈
V |
11 | 10 | rnex 7617 |
. . . 4
⊢ ran + ∈
V |
12 | | prex 5333 |
. . . 4
⊢ {∅,
(𝐹‘𝑀)} ∈ V |
13 | 11, 12 | unex 7469 |
. . 3
⊢ (ran
+ ∪
{∅, (𝐹‘𝑀)}) ∈ V |
14 | | fveq2 6670 |
. . . . . . 7
⊢ (𝑦 = 𝑀 → (seq𝑀( + , 𝐹)‘𝑦) = (seq𝑀( + , 𝐹)‘𝑀)) |
15 | 14 | eleq1d 2897 |
. . . . . 6
⊢ (𝑦 = 𝑀 → ((seq𝑀( + , 𝐹)‘𝑦) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}) ↔ (seq𝑀( + , 𝐹)‘𝑀) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}))) |
16 | | fveq2 6670 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → (seq𝑀( + , 𝐹)‘𝑦) = (seq𝑀( + , 𝐹)‘𝑧)) |
17 | 16 | eleq1d 2897 |
. . . . . 6
⊢ (𝑦 = 𝑧 → ((seq𝑀( + , 𝐹)‘𝑦) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}) ↔ (seq𝑀( + , 𝐹)‘𝑧) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}))) |
18 | | fveq2 6670 |
. . . . . . 7
⊢ (𝑦 = (𝑧 + 1) → (seq𝑀( + , 𝐹)‘𝑦) = (seq𝑀( + , 𝐹)‘(𝑧 + 1))) |
19 | 18 | eleq1d 2897 |
. . . . . 6
⊢ (𝑦 = (𝑧 + 1) → ((seq𝑀( + , 𝐹)‘𝑦) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}) ↔ (seq𝑀( + , 𝐹)‘(𝑧 + 1)) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}))) |
20 | | fveq2 6670 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (seq𝑀( + , 𝐹)‘𝑦) = (seq𝑀( + , 𝐹)‘𝑥)) |
21 | 20 | eleq1d 2897 |
. . . . . 6
⊢ (𝑦 = 𝑥 → ((seq𝑀( + , 𝐹)‘𝑦) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}) ↔ (seq𝑀( + , 𝐹)‘𝑥) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}))) |
22 | | seq1 13383 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀)) |
23 | | ssun2 4149 |
. . . . . . . 8
⊢ {∅,
(𝐹‘𝑀)} ⊆ (ran + ∪ {∅, (𝐹‘𝑀)}) |
24 | | fvex 6683 |
. . . . . . . . 9
⊢ (𝐹‘𝑀) ∈ V |
25 | 24 | prid2 4699 |
. . . . . . . 8
⊢ (𝐹‘𝑀) ∈ {∅, (𝐹‘𝑀)} |
26 | 23, 25 | sselii 3964 |
. . . . . . 7
⊢ (𝐹‘𝑀) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}) |
27 | 22, 26 | eqeltrdi 2921 |
. . . . . 6
⊢ (𝑀 ∈ ℤ → (seq𝑀( + , 𝐹)‘𝑀) ∈ (ran + ∪ {∅, (𝐹‘𝑀)})) |
28 | | seqp1 13385 |
. . . . . . . . 9
⊢ (𝑧 ∈
(ℤ≥‘𝑀) → (seq𝑀( + , 𝐹)‘(𝑧 + 1)) = ((seq𝑀( + , 𝐹)‘𝑧) + (𝐹‘(𝑧 + 1)))) |
29 | 28 | adantr 483 |
. . . . . . . 8
⊢ ((𝑧 ∈
(ℤ≥‘𝑀) ∧ (seq𝑀( + , 𝐹)‘𝑧) ∈ (ran + ∪ {∅, (𝐹‘𝑀)})) → (seq𝑀( + , 𝐹)‘(𝑧 + 1)) = ((seq𝑀( + , 𝐹)‘𝑧) + (𝐹‘(𝑧 + 1)))) |
30 | | df-ov 7159 |
. . . . . . . . . 10
⊢
((seq𝑀( + , 𝐹)‘𝑧) + (𝐹‘(𝑧 + 1))) = ( + ‘〈(seq𝑀( + , 𝐹)‘𝑧), (𝐹‘(𝑧 + 1))〉) |
31 | | snsspr1 4747 |
. . . . . . . . . . . 12
⊢ {∅}
⊆ {∅, (𝐹‘𝑀)} |
32 | | unss2 4157 |
. . . . . . . . . . . 12
⊢
({∅} ⊆ {∅, (𝐹‘𝑀)} → (ran + ∪ {∅}) ⊆
(ran +
∪ {∅, (𝐹‘𝑀)})) |
33 | 31, 32 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (ran
+ ∪
{∅}) ⊆ (ran + ∪ {∅, (𝐹‘𝑀)}) |
34 | | fvrn0 6698 |
. . . . . . . . . . 11
⊢ ( +
‘〈(seq𝑀( + , 𝐹)‘𝑧), (𝐹‘(𝑧 + 1))〉) ∈ (ran + ∪
{∅}) |
35 | 33, 34 | sselii 3964 |
. . . . . . . . . 10
⊢ ( +
‘〈(seq𝑀( + , 𝐹)‘𝑧), (𝐹‘(𝑧 + 1))〉) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}) |
36 | 30, 35 | eqeltri 2909 |
. . . . . . . . 9
⊢
((seq𝑀( + , 𝐹)‘𝑧) + (𝐹‘(𝑧 + 1))) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}) |
37 | 36 | a1i 11 |
. . . . . . . 8
⊢ ((𝑧 ∈
(ℤ≥‘𝑀) ∧ (seq𝑀( + , 𝐹)‘𝑧) ∈ (ran + ∪ {∅, (𝐹‘𝑀)})) → ((seq𝑀( + , 𝐹)‘𝑧) + (𝐹‘(𝑧 + 1))) ∈ (ran + ∪ {∅, (𝐹‘𝑀)})) |
38 | 29, 37 | eqeltrd 2913 |
. . . . . . 7
⊢ ((𝑧 ∈
(ℤ≥‘𝑀) ∧ (seq𝑀( + , 𝐹)‘𝑧) ∈ (ran + ∪ {∅, (𝐹‘𝑀)})) → (seq𝑀( + , 𝐹)‘(𝑧 + 1)) ∈ (ran + ∪ {∅, (𝐹‘𝑀)})) |
39 | 38 | ex 415 |
. . . . . 6
⊢ (𝑧 ∈
(ℤ≥‘𝑀) → ((seq𝑀( + , 𝐹)‘𝑧) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}) → (seq𝑀( + , 𝐹)‘(𝑧 + 1)) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}))) |
40 | 15, 17, 19, 21, 27, 39 | uzind4 12307 |
. . . . 5
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → (seq𝑀( + , 𝐹)‘𝑥) ∈ (ran + ∪ {∅, (𝐹‘𝑀)})) |
41 | 40 | rgen 3148 |
. . . 4
⊢
∀𝑥 ∈
(ℤ≥‘𝑀)(seq𝑀( + , 𝐹)‘𝑥) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}) |
42 | | fnfvrnss 6884 |
. . . 4
⊢
((seq𝑀( + , 𝐹) Fn
(ℤ≥‘𝑀) ∧ ∀𝑥 ∈ (ℤ≥‘𝑀)(seq𝑀( + , 𝐹)‘𝑥) ∈ (ran + ∪ {∅, (𝐹‘𝑀)})) → ran seq𝑀( + , 𝐹) ⊆ (ran + ∪ {∅, (𝐹‘𝑀)})) |
43 | 3, 41, 42 | mp2an 690 |
. . 3
⊢ ran
seq𝑀( + , 𝐹) ⊆ (ran + ∪ {∅, (𝐹‘𝑀)}) |
44 | 13, 43 | ssexi 5226 |
. 2
⊢ ran
seq𝑀( + , 𝐹) ∈ V |
45 | | funexw 7653 |
. 2
⊢ ((Fun
seq𝑀( + , 𝐹) ∧ dom seq𝑀( + , 𝐹) ∈ V ∧ ran seq𝑀( + , 𝐹) ∈ V) → seq𝑀( + , 𝐹) ∈ V) |
46 | 5, 9, 44, 45 | mp3an 1457 |
1
⊢ seq𝑀( + , 𝐹) ∈ V |