Theorem seqexw 13386

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

Hypotheses

Ref	Expression
seqexw.1	⊢ + ∈ V
seqexw.2	⊢ 𝑀 ∈ ℤ

Assertion

Ref	Expression
seqexw	⊢ seq𝑀( + , 𝐹) ∈ V

Proof of Theorem seqexw

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		seqexw.2	. . . 4 ⊢ 𝑀 ∈ ℤ
2		seqfn 13382	. . . 4 ⊢ (𝑀 ∈ ℤ → seq𝑀( + , 𝐹) Fn (ℤ≥‘𝑀))
3	1, 2	ax-mp 5	. . 3 ⊢ seq𝑀( + , 𝐹) Fn (ℤ≥‘𝑀)
4		fnfun 6453	. . 3 ⊢ (seq𝑀( + , 𝐹) Fn (ℤ≥‘𝑀) → Fun seq𝑀( + , 𝐹))
5	3, 4	ax-mp 5	. 2 ⊢ Fun seq𝑀( + , 𝐹)
6		fndm 6455	. . . 4 ⊢ (seq𝑀( + , 𝐹) Fn (ℤ≥‘𝑀) → dom seq𝑀( + , 𝐹) = (ℤ≥‘𝑀))
7	3, 6	ax-mp 5	. . 3 ⊢ dom seq𝑀( + , 𝐹) = (ℤ≥‘𝑀)
8		fvex 6683	. . 3 ⊢ (ℤ≥‘𝑀) ∈ V
9	7, 8	eqeltri 2909	. 2 ⊢ dom seq𝑀( + , 𝐹) ∈ V
10		seqexw.1	. . . . 5 ⊢ + ∈ V
11	10	rnex 7617	. . . 4 ⊢ ran + ∈ V
12		prex 5333	. . . 4 ⊢ {∅, (𝐹‘𝑀)} ∈ V
13	11, 12	unex 7469	. . 3 ⊢ (ran + ∪ {∅, (𝐹‘𝑀)}) ∈ V
14		fveq2 6670	. . . . . . 7 ⊢ (𝑦 = 𝑀 → (seq𝑀( + , 𝐹)‘𝑦) = (seq𝑀( + , 𝐹)‘𝑀))
15	14	eleq1d 2897	. . . . . 6 ⊢ (𝑦 = 𝑀 → ((seq𝑀( + , 𝐹)‘𝑦) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}) ↔ (seq𝑀( + , 𝐹)‘𝑀) ∈ (ran + ∪ {∅, (𝐹‘𝑀)})))
16		fveq2 6670	. . . . . . 7 ⊢ (𝑦 = 𝑧 → (seq𝑀( + , 𝐹)‘𝑦) = (seq𝑀( + , 𝐹)‘𝑧))
17	16	eleq1d 2897	. . . . . 6 ⊢ (𝑦 = 𝑧 → ((seq𝑀( + , 𝐹)‘𝑦) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}) ↔ (seq𝑀( + , 𝐹)‘𝑧) ∈ (ran + ∪ {∅, (𝐹‘𝑀)})))
18		fveq2 6670	. . . . . . 7 ⊢ (𝑦 = (𝑧 + 1) → (seq𝑀( + , 𝐹)‘𝑦) = (seq𝑀( + , 𝐹)‘(𝑧 + 1)))
19	18	eleq1d 2897	. . . . . 6 ⊢ (𝑦 = (𝑧 + 1) → ((seq𝑀( + , 𝐹)‘𝑦) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}) ↔ (seq𝑀( + , 𝐹)‘(𝑧 + 1)) ∈ (ran + ∪ {∅, (𝐹‘𝑀)})))
20		fveq2 6670	. . . . . . 7 ⊢ (𝑦 = 𝑥 → (seq𝑀( + , 𝐹)‘𝑦) = (seq𝑀( + , 𝐹)‘𝑥))
21	20	eleq1d 2897	. . . . . 6 ⊢ (𝑦 = 𝑥 → ((seq𝑀( + , 𝐹)‘𝑦) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}) ↔ (seq𝑀( + , 𝐹)‘𝑥) ∈ (ran + ∪ {∅, (𝐹‘𝑀)})))
22		seq1 13383	. . . . . . 7 ⊢ (𝑀 ∈ ℤ → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀))
23		ssun2 4149	. . . . . . . 8 ⊢ {∅, (𝐹‘𝑀)} ⊆ (ran + ∪ {∅, (𝐹‘𝑀)})
24		fvex 6683	. . . . . . . . 9 ⊢ (𝐹‘𝑀) ∈ V
25	24	prid2 4699	. . . . . . . 8 ⊢ (𝐹‘𝑀) ∈ {∅, (𝐹‘𝑀)}
26	23, 25	sselii 3964	. . . . . . 7 ⊢ (𝐹‘𝑀) ∈ (ran + ∪ {∅, (𝐹‘𝑀)})
27	22, 26	eqeltrdi 2921	. . . . . 6 ⊢ (𝑀 ∈ ℤ → (seq𝑀( + , 𝐹)‘𝑀) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}))
28		seqp1 13385	. . . . . . . . 9 ⊢ (𝑧 ∈ (ℤ≥‘𝑀) → (seq𝑀( + , 𝐹)‘(𝑧 + 1)) = ((seq𝑀( + , 𝐹)‘𝑧) + (𝐹‘(𝑧 + 1))))
29	28	adantr 483	. . . . . . . 8 ⊢ ((𝑧 ∈ (ℤ≥‘𝑀) ∧ (seq𝑀( + , 𝐹)‘𝑧) ∈ (ran + ∪ {∅, (𝐹‘𝑀)})) → (seq𝑀( + , 𝐹)‘(𝑧 + 1)) = ((seq𝑀( + , 𝐹)‘𝑧) + (𝐹‘(𝑧 + 1))))
30		df-ov 7159	. . . . . . . . . 10 ⊢ ((seq𝑀( + , 𝐹)‘𝑧) + (𝐹‘(𝑧 + 1))) = ( + ‘⟨(seq𝑀( + , 𝐹)‘𝑧), (𝐹‘(𝑧 + 1))⟩)
31		snsspr1 4747	. . . . . . . . . . . 12 ⊢ {∅} ⊆ {∅, (𝐹‘𝑀)}
32		unss2 4157	. . . . . . . . . . . 12 ⊢ ({∅} ⊆ {∅, (𝐹‘𝑀)} → (ran + ∪ {∅}) ⊆ (ran + ∪ {∅, (𝐹‘𝑀)}))
33	31, 32	ax-mp 5	. . . . . . . . . . 11 ⊢ (ran + ∪ {∅}) ⊆ (ran + ∪ {∅, (𝐹‘𝑀)})
34		fvrn0 6698	. . . . . . . . . . 11 ⊢ ( + ‘⟨(seq𝑀( + , 𝐹)‘𝑧), (𝐹‘(𝑧 + 1))⟩) ∈ (ran + ∪ {∅})
35	33, 34	sselii 3964	. . . . . . . . . 10 ⊢ ( + ‘⟨(seq𝑀( + , 𝐹)‘𝑧), (𝐹‘(𝑧 + 1))⟩) ∈ (ran + ∪ {∅, (𝐹‘𝑀)})
36	30, 35	eqeltri 2909	. . . . . . . . 9 ⊢ ((seq𝑀( + , 𝐹)‘𝑧) + (𝐹‘(𝑧 + 1))) ∈ (ran + ∪ {∅, (𝐹‘𝑀)})
37	36	a1i 11	. . . . . . . 8 ⊢ ((𝑧 ∈ (ℤ≥‘𝑀) ∧ (seq𝑀( + , 𝐹)‘𝑧) ∈ (ran + ∪ {∅, (𝐹‘𝑀)})) → ((seq𝑀( + , 𝐹)‘𝑧) + (𝐹‘(𝑧 + 1))) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}))
38	29, 37	eqeltrd 2913	. . . . . . 7 ⊢ ((𝑧 ∈ (ℤ≥‘𝑀) ∧ (seq𝑀( + , 𝐹)‘𝑧) ∈ (ran + ∪ {∅, (𝐹‘𝑀)})) → (seq𝑀( + , 𝐹)‘(𝑧 + 1)) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}))
39	38	ex 415	. . . . . 6 ⊢ (𝑧 ∈ (ℤ≥‘𝑀) → ((seq𝑀( + , 𝐹)‘𝑧) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}) → (seq𝑀( + , 𝐹)‘(𝑧 + 1)) ∈ (ran + ∪ {∅, (𝐹‘𝑀)})))
40	15, 17, 19, 21, 27, 39	uzind4 12307	. . . . 5 ⊢ (𝑥 ∈ (ℤ≥‘𝑀) → (seq𝑀( + , 𝐹)‘𝑥) ∈ (ran + ∪ {∅, (𝐹‘𝑀)}))
41	40	rgen 3148	. . . 4 ⊢ ∀𝑥 ∈ (ℤ≥‘𝑀)(seq𝑀( + , 𝐹)‘𝑥) ∈ (ran + ∪ {∅, (𝐹‘𝑀)})
42		fnfvrnss 6884	. . . 4 ⊢ ((seq𝑀( + , 𝐹) Fn (ℤ≥‘𝑀) ∧ ∀𝑥 ∈ (ℤ≥‘𝑀)(seq𝑀( + , 𝐹)‘𝑥) ∈ (ran + ∪ {∅, (𝐹‘𝑀)})) → ran seq𝑀( + , 𝐹) ⊆ (ran + ∪ {∅, (𝐹‘𝑀)}))
43	3, 41, 42	mp2an 690	. . 3 ⊢ ran seq𝑀( + , 𝐹) ⊆ (ran + ∪ {∅, (𝐹‘𝑀)})
44	13, 43	ssexi 5226	. 2 ⊢ ran seq𝑀( + , 𝐹) ∈ V
45		funexw 7653	. 2 ⊢ ((Fun seq𝑀( + , 𝐹) ∧ dom seq𝑀( + , 𝐹) ∈ V ∧ ran seq𝑀( + , 𝐹) ∈ V) → seq𝑀( + , 𝐹) ∈ V)
46	5, 9, 44, 45	mp3an 1457	1 ⊢ seq𝑀( + , 𝐹) ∈ V

Syntax hints:   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∀wral 3138  Vcvv 3494   ∪ cun 3934   ⊆ wss 3936  ∅c0 4291  {csn 4567  {cpr 4569  ⟨cop 4573  dom cdm 5555  ran crn 5556  Fun wfun 6349   Fn wfn 6350  ‘cfv 6355  (class class class)co 7156  1c1 10538   + caddc 10540  ℤcz 11982  ℤ_≥cuz 12244  seqcseq 13370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-cnex 10593  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7581  df-2nd 7690  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-nn 11639  df-n0 11899  df-z 11983  df-uz 12245  df-seq 13371

This theorem is referenced by:  mulgfval  18226