Step |
Hyp |
Ref |
Expression |
1 |
|
seqexw.1 |
⊢ + ∈ V |
2 |
|
seqexw.2 |
⊢ 𝑀 ∈ ℤ |
3 |
|
seqfn |
⊢ ( 𝑀 ∈ ℤ → seq 𝑀 ( + , 𝐹 ) Fn ( ℤ≥ ‘ 𝑀 ) ) |
4 |
2 3
|
ax-mp |
⊢ seq 𝑀 ( + , 𝐹 ) Fn ( ℤ≥ ‘ 𝑀 ) |
5 |
|
fnfun |
⊢ ( seq 𝑀 ( + , 𝐹 ) Fn ( ℤ≥ ‘ 𝑀 ) → Fun seq 𝑀 ( + , 𝐹 ) ) |
6 |
4 5
|
ax-mp |
⊢ Fun seq 𝑀 ( + , 𝐹 ) |
7 |
4
|
fndmi |
⊢ dom seq 𝑀 ( + , 𝐹 ) = ( ℤ≥ ‘ 𝑀 ) |
8 |
|
fvex |
⊢ ( ℤ≥ ‘ 𝑀 ) ∈ V |
9 |
7 8
|
eqeltri |
⊢ dom seq 𝑀 ( + , 𝐹 ) ∈ V |
10 |
1
|
rnex |
⊢ ran + ∈ V |
11 |
|
prex |
⊢ { ∅ , ( 𝐹 ‘ 𝑀 ) } ∈ V |
12 |
10 11
|
unex |
⊢ ( ran + ∪ { ∅ , ( 𝐹 ‘ 𝑀 ) } ) ∈ V |
13 |
|
fveq2 |
⊢ ( 𝑦 = 𝑀 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑦 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) ) |
14 |
13
|
eleq1d |
⊢ ( 𝑦 = 𝑀 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑦 ) ∈ ( ran + ∪ { ∅ , ( 𝐹 ‘ 𝑀 ) } ) ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) ∈ ( ran + ∪ { ∅ , ( 𝐹 ‘ 𝑀 ) } ) ) ) |
15 |
|
fveq2 |
⊢ ( 𝑦 = 𝑧 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑦 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) ) |
16 |
15
|
eleq1d |
⊢ ( 𝑦 = 𝑧 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑦 ) ∈ ( ran + ∪ { ∅ , ( 𝐹 ‘ 𝑀 ) } ) ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) ∈ ( ran + ∪ { ∅ , ( 𝐹 ‘ 𝑀 ) } ) ) ) |
17 |
|
fveq2 |
⊢ ( 𝑦 = ( 𝑧 + 1 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑦 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ) |
18 |
17
|
eleq1d |
⊢ ( 𝑦 = ( 𝑧 + 1 ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑦 ) ∈ ( ran + ∪ { ∅ , ( 𝐹 ‘ 𝑀 ) } ) ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ∈ ( ran + ∪ { ∅ , ( 𝐹 ‘ 𝑀 ) } ) ) ) |
19 |
|
fveq2 |
⊢ ( 𝑦 = 𝑥 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑦 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ) |
20 |
19
|
eleq1d |
⊢ ( 𝑦 = 𝑥 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑦 ) ∈ ( ran + ∪ { ∅ , ( 𝐹 ‘ 𝑀 ) } ) ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ∈ ( ran + ∪ { ∅ , ( 𝐹 ‘ 𝑀 ) } ) ) ) |
21 |
|
seq1 |
⊢ ( 𝑀 ∈ ℤ → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) ) |
22 |
|
ssun2 |
⊢ { ∅ , ( 𝐹 ‘ 𝑀 ) } ⊆ ( ran + ∪ { ∅ , ( 𝐹 ‘ 𝑀 ) } ) |
23 |
|
fvex |
⊢ ( 𝐹 ‘ 𝑀 ) ∈ V |
24 |
23
|
prid2 |
⊢ ( 𝐹 ‘ 𝑀 ) ∈ { ∅ , ( 𝐹 ‘ 𝑀 ) } |
25 |
22 24
|
sselii |
⊢ ( 𝐹 ‘ 𝑀 ) ∈ ( ran + ∪ { ∅ , ( 𝐹 ‘ 𝑀 ) } ) |
26 |
21 25
|
eqeltrdi |
⊢ ( 𝑀 ∈ ℤ → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) ∈ ( ran + ∪ { ∅ , ( 𝐹 ‘ 𝑀 ) } ) ) |
27 |
|
seqp1 |
⊢ ( 𝑧 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑧 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) |
28 |
27
|
adantr |
⊢ ( ( 𝑧 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) ∈ ( ran + ∪ { ∅ , ( 𝐹 ‘ 𝑀 ) } ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑧 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ) |
29 |
|
df-ov |
⊢ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) = ( + ‘ 〈 ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) , ( 𝐹 ‘ ( 𝑧 + 1 ) ) 〉 ) |
30 |
|
snsspr1 |
⊢ { ∅ } ⊆ { ∅ , ( 𝐹 ‘ 𝑀 ) } |
31 |
|
unss2 |
⊢ ( { ∅ } ⊆ { ∅ , ( 𝐹 ‘ 𝑀 ) } → ( ran + ∪ { ∅ } ) ⊆ ( ran + ∪ { ∅ , ( 𝐹 ‘ 𝑀 ) } ) ) |
32 |
30 31
|
ax-mp |
⊢ ( ran + ∪ { ∅ } ) ⊆ ( ran + ∪ { ∅ , ( 𝐹 ‘ 𝑀 ) } ) |
33 |
|
fvrn0 |
⊢ ( + ‘ 〈 ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) , ( 𝐹 ‘ ( 𝑧 + 1 ) ) 〉 ) ∈ ( ran + ∪ { ∅ } ) |
34 |
32 33
|
sselii |
⊢ ( + ‘ 〈 ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) , ( 𝐹 ‘ ( 𝑧 + 1 ) ) 〉 ) ∈ ( ran + ∪ { ∅ , ( 𝐹 ‘ 𝑀 ) } ) |
35 |
29 34
|
eqeltri |
⊢ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ∈ ( ran + ∪ { ∅ , ( 𝐹 ‘ 𝑀 ) } ) |
36 |
35
|
a1i |
⊢ ( ( 𝑧 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) ∈ ( ran + ∪ { ∅ , ( 𝐹 ‘ 𝑀 ) } ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ∈ ( ran + ∪ { ∅ , ( 𝐹 ‘ 𝑀 ) } ) ) |
37 |
28 36
|
eqeltrd |
⊢ ( ( 𝑧 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) ∈ ( ran + ∪ { ∅ , ( 𝐹 ‘ 𝑀 ) } ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ∈ ( ran + ∪ { ∅ , ( 𝐹 ‘ 𝑀 ) } ) ) |
38 |
37
|
ex |
⊢ ( 𝑧 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) ∈ ( ran + ∪ { ∅ , ( 𝐹 ‘ 𝑀 ) } ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑧 + 1 ) ) ∈ ( ran + ∪ { ∅ , ( 𝐹 ‘ 𝑀 ) } ) ) ) |
39 |
14 16 18 20 26 38
|
uzind4 |
⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ∈ ( ran + ∪ { ∅ , ( 𝐹 ‘ 𝑀 ) } ) ) |
40 |
39
|
rgen |
⊢ ∀ 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ∈ ( ran + ∪ { ∅ , ( 𝐹 ‘ 𝑀 ) } ) |
41 |
|
fnfvrnss |
⊢ ( ( seq 𝑀 ( + , 𝐹 ) Fn ( ℤ≥ ‘ 𝑀 ) ∧ ∀ 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ∈ ( ran + ∪ { ∅ , ( 𝐹 ‘ 𝑀 ) } ) ) → ran seq 𝑀 ( + , 𝐹 ) ⊆ ( ran + ∪ { ∅ , ( 𝐹 ‘ 𝑀 ) } ) ) |
42 |
4 40 41
|
mp2an |
⊢ ran seq 𝑀 ( + , 𝐹 ) ⊆ ( ran + ∪ { ∅ , ( 𝐹 ‘ 𝑀 ) } ) |
43 |
12 42
|
ssexi |
⊢ ran seq 𝑀 ( + , 𝐹 ) ∈ V |
44 |
|
funexw |
⊢ ( ( Fun seq 𝑀 ( + , 𝐹 ) ∧ dom seq 𝑀 ( + , 𝐹 ) ∈ V ∧ ran seq 𝑀 ( + , 𝐹 ) ∈ V ) → seq 𝑀 ( + , 𝐹 ) ∈ V ) |
45 |
6 9 43 44
|
mp3an |
⊢ seq 𝑀 ( + , 𝐹 ) ∈ V |