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 + ∈ V
seqexw.2 𝑀 ∈ ℤ
Assertion seqexw seq 𝑀 ( + , 𝐹 ) ∈ V

Proof

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