Step |
Hyp |
Ref |
Expression |
1 |
|
seqexw.1 |
|- .+ e. _V |
2 |
|
seqexw.2 |
|- M e. ZZ |
3 |
|
seqfn |
|- ( M e. ZZ -> seq M ( .+ , F ) Fn ( ZZ>= ` M ) ) |
4 |
2 3
|
ax-mp |
|- seq M ( .+ , F ) Fn ( ZZ>= ` M ) |
5 |
|
fnfun |
|- ( seq M ( .+ , F ) Fn ( ZZ>= ` M ) -> Fun seq M ( .+ , F ) ) |
6 |
4 5
|
ax-mp |
|- Fun seq M ( .+ , F ) |
7 |
4
|
fndmi |
|- dom seq M ( .+ , F ) = ( ZZ>= ` M ) |
8 |
|
fvex |
|- ( ZZ>= ` M ) e. _V |
9 |
7 8
|
eqeltri |
|- dom seq M ( .+ , F ) e. _V |
10 |
1
|
rnex |
|- ran .+ e. _V |
11 |
|
prex |
|- { (/) , ( F ` M ) } e. _V |
12 |
10 11
|
unex |
|- ( ran .+ u. { (/) , ( F ` M ) } ) e. _V |
13 |
|
fveq2 |
|- ( y = M -> ( seq M ( .+ , F ) ` y ) = ( seq M ( .+ , F ) ` M ) ) |
14 |
13
|
eleq1d |
|- ( y = M -> ( ( seq M ( .+ , F ) ` y ) e. ( ran .+ u. { (/) , ( F ` M ) } ) <-> ( seq M ( .+ , F ) ` M ) e. ( ran .+ u. { (/) , ( F ` M ) } ) ) ) |
15 |
|
fveq2 |
|- ( y = z -> ( seq M ( .+ , F ) ` y ) = ( seq M ( .+ , F ) ` z ) ) |
16 |
15
|
eleq1d |
|- ( y = z -> ( ( seq M ( .+ , F ) ` y ) e. ( ran .+ u. { (/) , ( F ` M ) } ) <-> ( seq M ( .+ , F ) ` z ) e. ( ran .+ u. { (/) , ( F ` M ) } ) ) ) |
17 |
|
fveq2 |
|- ( y = ( z + 1 ) -> ( seq M ( .+ , F ) ` y ) = ( seq M ( .+ , F ) ` ( z + 1 ) ) ) |
18 |
17
|
eleq1d |
|- ( y = ( z + 1 ) -> ( ( seq M ( .+ , F ) ` y ) e. ( ran .+ u. { (/) , ( F ` M ) } ) <-> ( seq M ( .+ , F ) ` ( z + 1 ) ) e. ( ran .+ u. { (/) , ( F ` M ) } ) ) ) |
19 |
|
fveq2 |
|- ( y = x -> ( seq M ( .+ , F ) ` y ) = ( seq M ( .+ , F ) ` x ) ) |
20 |
19
|
eleq1d |
|- ( y = x -> ( ( seq M ( .+ , F ) ` y ) e. ( ran .+ u. { (/) , ( F ` M ) } ) <-> ( seq M ( .+ , F ) ` x ) e. ( ran .+ u. { (/) , ( F ` M ) } ) ) ) |
21 |
|
seq1 |
|- ( M e. ZZ -> ( seq M ( .+ , F ) ` M ) = ( F ` M ) ) |
22 |
|
ssun2 |
|- { (/) , ( F ` M ) } C_ ( ran .+ u. { (/) , ( F ` M ) } ) |
23 |
|
fvex |
|- ( F ` M ) e. _V |
24 |
23
|
prid2 |
|- ( F ` M ) e. { (/) , ( F ` M ) } |
25 |
22 24
|
sselii |
|- ( F ` M ) e. ( ran .+ u. { (/) , ( F ` M ) } ) |
26 |
21 25
|
eqeltrdi |
|- ( M e. ZZ -> ( seq M ( .+ , F ) ` M ) e. ( ran .+ u. { (/) , ( F ` M ) } ) ) |
27 |
|
seqp1 |
|- ( z e. ( ZZ>= ` M ) -> ( seq M ( .+ , F ) ` ( z + 1 ) ) = ( ( seq M ( .+ , F ) ` z ) .+ ( F ` ( z + 1 ) ) ) ) |
28 |
27
|
adantr |
|- ( ( z e. ( ZZ>= ` M ) /\ ( seq M ( .+ , F ) ` z ) e. ( ran .+ u. { (/) , ( F ` M ) } ) ) -> ( seq M ( .+ , F ) ` ( z + 1 ) ) = ( ( seq M ( .+ , F ) ` z ) .+ ( F ` ( z + 1 ) ) ) ) |
29 |
|
df-ov |
|- ( ( seq M ( .+ , F ) ` z ) .+ ( F ` ( z + 1 ) ) ) = ( .+ ` <. ( seq M ( .+ , F ) ` z ) , ( F ` ( z + 1 ) ) >. ) |
30 |
|
snsspr1 |
|- { (/) } C_ { (/) , ( F ` M ) } |
31 |
|
unss2 |
|- ( { (/) } C_ { (/) , ( F ` M ) } -> ( ran .+ u. { (/) } ) C_ ( ran .+ u. { (/) , ( F ` M ) } ) ) |
32 |
30 31
|
ax-mp |
|- ( ran .+ u. { (/) } ) C_ ( ran .+ u. { (/) , ( F ` M ) } ) |
33 |
|
fvrn0 |
|- ( .+ ` <. ( seq M ( .+ , F ) ` z ) , ( F ` ( z + 1 ) ) >. ) e. ( ran .+ u. { (/) } ) |
34 |
32 33
|
sselii |
|- ( .+ ` <. ( seq M ( .+ , F ) ` z ) , ( F ` ( z + 1 ) ) >. ) e. ( ran .+ u. { (/) , ( F ` M ) } ) |
35 |
29 34
|
eqeltri |
|- ( ( seq M ( .+ , F ) ` z ) .+ ( F ` ( z + 1 ) ) ) e. ( ran .+ u. { (/) , ( F ` M ) } ) |
36 |
35
|
a1i |
|- ( ( z e. ( ZZ>= ` M ) /\ ( seq M ( .+ , F ) ` z ) e. ( ran .+ u. { (/) , ( F ` M ) } ) ) -> ( ( seq M ( .+ , F ) ` z ) .+ ( F ` ( z + 1 ) ) ) e. ( ran .+ u. { (/) , ( F ` M ) } ) ) |
37 |
28 36
|
eqeltrd |
|- ( ( z e. ( ZZ>= ` M ) /\ ( seq M ( .+ , F ) ` z ) e. ( ran .+ u. { (/) , ( F ` M ) } ) ) -> ( seq M ( .+ , F ) ` ( z + 1 ) ) e. ( ran .+ u. { (/) , ( F ` M ) } ) ) |
38 |
37
|
ex |
|- ( z e. ( ZZ>= ` M ) -> ( ( seq M ( .+ , F ) ` z ) e. ( ran .+ u. { (/) , ( F ` M ) } ) -> ( seq M ( .+ , F ) ` ( z + 1 ) ) e. ( ran .+ u. { (/) , ( F ` M ) } ) ) ) |
39 |
14 16 18 20 26 38
|
uzind4 |
|- ( x e. ( ZZ>= ` M ) -> ( seq M ( .+ , F ) ` x ) e. ( ran .+ u. { (/) , ( F ` M ) } ) ) |
40 |
39
|
rgen |
|- A. x e. ( ZZ>= ` M ) ( seq M ( .+ , F ) ` x ) e. ( ran .+ u. { (/) , ( F ` M ) } ) |
41 |
|
fnfvrnss |
|- ( ( seq M ( .+ , F ) Fn ( ZZ>= ` M ) /\ A. x e. ( ZZ>= ` M ) ( seq M ( .+ , F ) ` x ) e. ( ran .+ u. { (/) , ( F ` M ) } ) ) -> ran seq M ( .+ , F ) C_ ( ran .+ u. { (/) , ( F ` M ) } ) ) |
42 |
4 40 41
|
mp2an |
|- ran seq M ( .+ , F ) C_ ( ran .+ u. { (/) , ( F ` M ) } ) |
43 |
12 42
|
ssexi |
|- ran seq M ( .+ , F ) e. _V |
44 |
|
funexw |
|- ( ( Fun seq M ( .+ , F ) /\ dom seq M ( .+ , F ) e. _V /\ ran seq M ( .+ , F ) e. _V ) -> seq M ( .+ , F ) e. _V ) |
45 |
6 9 43 44
|
mp3an |
|- seq M ( .+ , F ) e. _V |