sseqfv1

Description: Value of the strong sequence builder function at one of its initial values. (Contributed by Thierry Arnoux, 21-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$
	sseqfv1.4	$⊢ φ \to N \in (0 ..^\|M\|)$
Assertion	sseqfv1	$⊢ φ \to (M {seq}_{str} F) (N) = M (N)$

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		sseqfv1.4	$⊢ φ \to N \in (0 ..^\|M\|)$
6	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) ”⟩\})))$
7	6	fveq1d	$⊢ φ \to (M {seq}_{str} F) (N) = (M \cup (lastS \circ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})))) (N)$
8		wrdfn	$⊢ M \in Word S \to M Fn (0 ..^\|M\|)$
9	2 8	syl	$⊢ φ \to M Fn (0 ..^\|M\|)$
10		fvex	$⊢ x (\|x\| - 1) \in V$
11		df-lsw	$⊢ lastS = (x \in V ⟼ x (\|x\| - 1))$
12	10 11	fnmpti	$⊢ lastS Fn V$
13	12	a1i	$⊢ φ \to lastS Fn V$
14		lencl	$⊢ M \in Word S \to \|M\| \in ℕ_{0}$
15	2 14	syl	$⊢ φ \to \|M\| \in ℕ_{0}$
16	15	nn0zd	$⊢ φ \to \|M\| \in ℤ$
17		seqfn	$⊢ \|M\| \in ℤ \to seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})) Fn ℤ_{\geq \|M\|}$
18	16 17	syl	$⊢ φ \to seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})) Fn ℤ_{\geq \|M\|}$
19		ssv	$⊢ ran seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})) \subseteq V$
20	19	a1i	$⊢ φ \to ran seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})) \subseteq V$
21		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\|}$
22	13 18 20 21	syl3anc	$⊢ φ \to (lastS \circ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\}))) Fn ℤ_{\geq \|M\|}$
23		fzouzdisj	$⊢ (0 ..^\|M\|) \cap ℤ_{\geq \|M\|} = \emptyset$
24	23	a1i	$⊢ φ \to (0 ..^\|M\|) \cap ℤ_{\geq \|M\|} = \emptyset$
25		fvun1	$⊢ (M Fn (0 ..^\|M\|) \land (lastS \circ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\}))) Fn ℤ_{\geq \|M\|} \land ((0 ..^\|M\|) \cap ℤ_{\geq \|M\|} = \emptyset \land N \in (0 ..^\|M\|))) \to (M \cup (lastS \circ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})))) (N) = M (N)$
26	9 22 24 5 25	syl112anc	$⊢ φ \to (M \cup (lastS \circ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})))) (N) = M (N)$
27	7 26	eqtrd	$⊢ φ \to (M {seq}_{str} F) (N) = M (N)$

Metamath Proof Explorer

Theorem sseqfv1

Proof