Metamath Proof Explorer


Theorem seqexw

Description: Weak version of seqex that holds without ax-rep . A sequence builder exists when its binary operation input exists and its starting index is an integer. (Contributed by Rohan Ridenour, 14-Aug-2023)

Ref Expression
Hypotheses seqexw.1
|- .+ e. _V
seqexw.2
|- M e. ZZ
Assertion seqexw
|- seq M ( .+ , F ) e. _V

Proof

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