This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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