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