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{˙}{+} \in V$
	seqexw.2	$⊢ M \in ℤ$
Assertion	seqexw	$⊢ seq M (\underset{˙}{+}, F) \in V$

Proof

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

Metamath Proof Explorer

Theorem seqexw

Proof