sseqfn

Description: A strong recursive sequence is a function over the nonnegative integers. (Contributed by Thierry Arnoux, 23-Apr-2019)

	Ref	Expression
Hypotheses	sseqval.1	$⊢ φ \to S \in V$
	sseqval.2	$⊢ φ \to M \in Word S$
	sseqval.3	$⊢ W = Word S \cap {\|.\|}^{-1} [ℤ_{\geq \|M\|}]$
	sseqval.4	$⊢ φ \to F : W ⟶ S$
Assertion	sseqfn	$⊢ φ \to (M {seq}_{str} F) Fn ℕ_{0}$

Proof

Step	Hyp	Ref	Expression
1		sseqval.1	$⊢ φ \to S \in V$
2		sseqval.2	$⊢ φ \to M \in Word S$
3		sseqval.3	$⊢ W = Word S \cap {\|.\|}^{-1} [ℤ_{\geq \|M\|}]$
4		sseqval.4	$⊢ φ \to F : W ⟶ S$
5		wrdfn	$⊢ M \in Word S \to M Fn (0 ..^\|M\|)$
6	2 5	syl	$⊢ φ \to M Fn (0 ..^\|M\|)$
7		fvex	$⊢ x (\|x\| - 1) \in V$
8		df-lsw	$⊢ lastS = (x \in V ⟼ x (\|x\| - 1))$
9	7 8	fnmpti	$⊢ lastS Fn V$
10	9	a1i	$⊢ φ \to lastS Fn V$
11		lencl	$⊢ M \in Word S \to \|M\| \in ℕ_{0}$
12	11	nn0zd	$⊢ M \in Word S \to \|M\| \in ℤ$
13		seqfn	$⊢ \|M\| \in ℤ \to seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})) Fn ℤ_{\geq \|M\|}$
14	2 12 13	3syl	$⊢ φ \to seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})) Fn ℤ_{\geq \|M\|}$
15		ssv	$⊢ ran seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})) \subseteq V$
16	15	a1i	$⊢ φ \to ran seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})) \subseteq V$
17		fnco	$⊢ (lastS Fn V \land seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})) Fn ℤ_{\geq \|M\|} \land ran seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})) \subseteq V) \to (lastS \circ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\}))) Fn ℤ_{\geq \|M\|}$
18	10 14 16 17	syl3anc	$⊢ φ \to (lastS \circ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\}))) Fn ℤ_{\geq \|M\|}$
19		fzouzdisj	$⊢ (0 ..^\|M\|) \cap ℤ_{\geq \|M\|} = \emptyset$
20	19	a1i	$⊢ φ \to (0 ..^\|M\|) \cap ℤ_{\geq \|M\|} = \emptyset$
21	6 18 20	fnund	$⊢ φ \to (M \cup (lastS \circ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})))) Fn ((0 ..^\|M\|) \cup ℤ_{\geq \|M\|})$
22	1 2 3 4	sseqval	$⊢ φ \to M {seq}_{str} F = M \cup (lastS \circ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})))$
23		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
24		elnn0uz	$⊢ \|M\| \in ℕ_{0} \leftrightarrow \|M\| \in ℤ_{\geq 0}$
25		fzouzsplit	$⊢ \|M\| \in ℤ_{\geq 0} \to ℤ_{\geq 0} = (0 ..^\|M\|) \cup ℤ_{\geq \|M\|}$
26	24 25	sylbi	$⊢ \|M\| \in ℕ_{0} \to ℤ_{\geq 0} = (0 ..^\|M\|) \cup ℤ_{\geq \|M\|}$
27	2 11 26	3syl	$⊢ φ \to ℤ_{\geq 0} = (0 ..^\|M\|) \cup ℤ_{\geq \|M\|}$
28	23 27	eqtrid	$⊢ φ \to ℕ_{0} = (0 ..^\|M\|) \cup ℤ_{\geq \|M\|}$
29	22 28	fneq12d	$⊢ φ \to ((M {seq}_{str} F) Fn ℕ_{0} \leftrightarrow (M \cup (lastS \circ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})))) Fn ((0 ..^\|M\|) \cup ℤ_{\geq \|M\|}))$
30	21 29	mpbird	$⊢ φ \to (M {seq}_{str} F) Fn ℕ_{0}$

Metamath Proof Explorer

Theorem sseqfn

Proof