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	$$⊢\underset{\dot{}}{+}\in \mathrm{V}$$
	seqexw.2	$$⊢M\in \mathbb{Z}$$
Assertion	seqexw	$$⊢seqM\left(\underset{\dot{}}{+},F\right)\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		seqexw.1	$$⊢\underset{\dot{}}{+}\in \mathrm{V}$$
2		seqexw.2	$$⊢M\in \mathbb{Z}$$
3		seqfn	$$⊢M\in \mathbb{Z}\to seqM\left(\underset{\dot{}}{+},F\right)Fn{\mathbb{Z}}_{\ge M}$$
4	2 3	ax-mp	$$⊢seqM\left(\underset{\dot{}}{+},F\right)Fn{\mathbb{Z}}_{\ge M}$$
5		fnfun	$$⊢seqM\left(\underset{\dot{}}{+},F\right)Fn{\mathbb{Z}}_{\ge M}\to \mathrm{Fun}seqM\left(\underset{\dot{}}{+},F\right)$$
6	4 5	ax-mp	$$⊢\mathrm{Fun}seqM\left(\underset{\dot{}}{+},F\right)$$
7		fndm	$$⊢seqM\left(\underset{\dot{}}{+},F\right)Fn{\mathbb{Z}}_{\ge M}\to \mathrm{dom}seqM\left(\underset{\dot{}}{+},F\right)={\mathbb{Z}}_{\ge M}$$
8	4 7	ax-mp	$$⊢\mathrm{dom}seqM\left(\underset{\dot{}}{+},F\right)={\mathbb{Z}}_{\ge M}$$
9		fvex	$$⊢{\mathbb{Z}}_{\ge M}\in \mathrm{V}$$
10	8 9	eqeltri	$$⊢\mathrm{dom}seqM\left(\underset{\dot{}}{+},F\right)\in \mathrm{V}$$
11	1	rnex	$$⊢\mathrm{ran}\underset{\dot{}}{+}\in \mathrm{V}$$
12		prex	$$⊢\left\{\varnothing ,F\left(M\right)\right\}\in \mathrm{V}$$
13	11 12	unex	$$⊢\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing ,F\left(M\right)\right\}\in \mathrm{V}$$
14		fveq2	$$⊢y=M\to seqM\left(\underset{\dot{}}{+},F\right)\left(y\right)=seqM\left(\underset{\dot{}}{+},F\right)\left(M\right)$$
15	14	eleq1d	$$⊢y=M\to \left(seqM\left(\underset{\dot{}}{+},F\right)\left(y\right)\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing ,F\left(M\right)\right\}\right)\leftrightarrow seqM\left(\underset{\dot{}}{+},F\right)\left(M\right)\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing ,F\left(M\right)\right\}\right)\right)$$
16		fveq2	$$⊢y=z\to seqM\left(\underset{\dot{}}{+},F\right)\left(y\right)=seqM\left(\underset{\dot{}}{+},F\right)\left(z\right)$$
17	16	eleq1d	$$⊢y=z\to \left(seqM\left(\underset{\dot{}}{+},F\right)\left(y\right)\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing ,F\left(M\right)\right\}\right)\leftrightarrow seqM\left(\underset{\dot{}}{+},F\right)\left(z\right)\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing ,F\left(M\right)\right\}\right)\right)$$
18		fveq2	$$⊢y=z+1\to seqM\left(\underset{\dot{}}{+},F\right)\left(y\right)=seqM\left(\underset{\dot{}}{+},F\right)\left(z+1\right)$$
19	18	eleq1d	$$⊢y=z+1\to \left(seqM\left(\underset{\dot{}}{+},F\right)\left(y\right)\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing ,F\left(M\right)\right\}\right)\leftrightarrow seqM\left(\underset{\dot{}}{+},F\right)\left(z+1\right)\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing ,F\left(M\right)\right\}\right)\right)$$
20		fveq2	$$⊢y=x\to seqM\left(\underset{\dot{}}{+},F\right)\left(y\right)=seqM\left(\underset{\dot{}}{+},F\right)\left(x\right)$$
21	20	eleq1d	$$⊢y=x\to \left(seqM\left(\underset{\dot{}}{+},F\right)\left(y\right)\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing ,F\left(M\right)\right\}\right)\leftrightarrow seqM\left(\underset{\dot{}}{+},F\right)\left(x\right)\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing ,F\left(M\right)\right\}\right)\right)$$
22		seq1	$$⊢M\in \mathbb{Z}\to seqM\left(\underset{\dot{}}{+},F\right)\left(M\right)=F\left(M\right)$$
23		ssun2	$$⊢\left\{\varnothing ,F\left(M\right)\right\}\subseteq \mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing ,F\left(M\right)\right\}$$
24		fvex	$$⊢F\left(M\right)\in \mathrm{V}$$
25	24	prid2	$$⊢F\left(M\right)\in \left\{\varnothing ,F\left(M\right)\right\}$$
26	23 25	sselii	$$⊢F\left(M\right)\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing ,F\left(M\right)\right\}\right)$$
27	22 26	eqeltrdi	$$⊢M\in \mathbb{Z}\to seqM\left(\underset{\dot{}}{+},F\right)\left(M\right)\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing ,F\left(M\right)\right\}\right)$$
28		seqp1	$$⊢z\in {\mathbb{Z}}_{\ge M}\to seqM\left(\underset{\dot{}}{+},F\right)\left(z+1\right)=seqM\left(\underset{\dot{}}{+},F\right)\left(z\right)\underset{\dot{}}{+}F\left(z+1\right)$$
29	28	adantr	$$⊢\left(z\in {\mathbb{Z}}_{\ge M}\wedge seqM\left(\underset{\dot{}}{+},F\right)\left(z\right)\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing ,F\left(M\right)\right\}\right)\right)\to seqM\left(\underset{\dot{}}{+},F\right)\left(z+1\right)=seqM\left(\underset{\dot{}}{+},F\right)\left(z\right)\underset{\dot{}}{+}F\left(z+1\right)$$
30		df-ov	$$⊢seqM\left(\underset{\dot{}}{+},F\right)\left(z\right)\underset{\dot{}}{+}F\left(z+1\right)=\underset{\dot{}}{+}\left(⟨seqM\left(\underset{\dot{}}{+},F\right)\left(z\right),F\left(z+1\right)⟩\right)$$
31		snsspr1	$$⊢\left\{\varnothing \right\}\subseteq \left\{\varnothing ,F\left(M\right)\right\}$$
32		unss2	$$⊢\left\{\varnothing \right\}\subseteq \left\{\varnothing ,F\left(M\right)\right\}\to \mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing \right\}\subseteq \mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing ,F\left(M\right)\right\}$$
33	31 32	ax-mp	$$⊢\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing \right\}\subseteq \mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing ,F\left(M\right)\right\}$$
34		fvrn0	$$⊢\underset{\dot{}}{+}\left(⟨seqM\left(\underset{\dot{}}{+},F\right)\left(z\right),F\left(z+1\right)⟩\right)\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing \right\}\right)$$
35	33 34	sselii	$$⊢\underset{\dot{}}{+}\left(⟨seqM\left(\underset{\dot{}}{+},F\right)\left(z\right),F\left(z+1\right)⟩\right)\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing ,F\left(M\right)\right\}\right)$$
36	30 35	eqeltri	$$⊢seqM\left(\underset{\dot{}}{+},F\right)\left(z\right)\underset{\dot{}}{+}F\left(z+1\right)\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing ,F\left(M\right)\right\}\right)$$
37	36	a1i	$$⊢\left(z\in {\mathbb{Z}}_{\ge M}\wedge seqM\left(\underset{\dot{}}{+},F\right)\left(z\right)\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing ,F\left(M\right)\right\}\right)\right)\to seqM\left(\underset{\dot{}}{+},F\right)\left(z\right)\underset{\dot{}}{+}F\left(z+1\right)\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing ,F\left(M\right)\right\}\right)$$
38	29 37	eqeltrd	$$⊢\left(z\in {\mathbb{Z}}_{\ge M}\wedge seqM\left(\underset{\dot{}}{+},F\right)\left(z\right)\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing ,F\left(M\right)\right\}\right)\right)\to seqM\left(\underset{\dot{}}{+},F\right)\left(z+1\right)\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing ,F\left(M\right)\right\}\right)$$
39	38	ex	$$⊢z\in {\mathbb{Z}}_{\ge M}\to \left(seqM\left(\underset{\dot{}}{+},F\right)\left(z\right)\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing ,F\left(M\right)\right\}\right)\to seqM\left(\underset{\dot{}}{+},F\right)\left(z+1\right)\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing ,F\left(M\right)\right\}\right)\right)$$
40	15 17 19 21 27 39	uzind4	$$⊢x\in {\mathbb{Z}}_{\ge M}\to seqM\left(\underset{\dot{}}{+},F\right)\left(x\right)\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing ,F\left(M\right)\right\}\right)$$
41	40	rgen	$$⊢\forall x\in {\mathbb{Z}}_{\ge M}seqM\left(\underset{\dot{}}{+},F\right)\left(x\right)\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing ,F\left(M\right)\right\}\right)$$
42		fnfvrnss	$$⊢\left(seqM\left(\underset{\dot{}}{+},F\right)Fn{\mathbb{Z}}_{\ge M}\wedge \forall x\in {\mathbb{Z}}_{\ge M}seqM\left(\underset{\dot{}}{+},F\right)\left(x\right)\in \left(\mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing ,F\left(M\right)\right\}\right)\right)\to \mathrm{ran}seqM\left(\underset{\dot{}}{+},F\right)\subseteq \mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing ,F\left(M\right)\right\}$$
43	4 41 42	mp2an	$$⊢\mathrm{ran}seqM\left(\underset{\dot{}}{+},F\right)\subseteq \mathrm{ran}\underset{\dot{}}{+}\cup \left\{\varnothing ,F\left(M\right)\right\}$$
44	13 43	ssexi	$$⊢\mathrm{ran}seqM\left(\underset{\dot{}}{+},F\right)\in \mathrm{V}$$
45		funexw	$$⊢\left(\mathrm{Fun}seqM\left(\underset{\dot{}}{+},F\right)\wedge \mathrm{dom}seqM\left(\underset{\dot{}}{+},F\right)\in \mathrm{V}\wedge \mathrm{ran}seqM\left(\underset{\dot{}}{+},F\right)\in \mathrm{V}\right)\to seqM\left(\underset{\dot{}}{+},F\right)\in \mathrm{V}$$
46	6 10 44 45	mp3an	$$⊢seqM\left(\underset{\dot{}}{+},F\right)\in \mathrm{V}$$