sseqfv2

Description: Value of the strong sequence builder function. (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$
	sseqfv2.4	$⊢ φ \to N \in ℤ_{\geq \|M\|}$
Assertion	sseqfv2	$⊢ φ \to (M {seq}_{str} F) (N) = lastS (seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (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		sseqfv2.4	$⊢ φ \to N \in ℤ_{\geq \|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		fvun2	$⊢ (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 ℤ_{\geq \|M\|})) \to (M \cup (lastS \circ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})))) (N) = (lastS \circ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (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) = (lastS \circ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\}))) (N)$
27		fnfun	$⊢ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})) Fn ℤ_{\geq \|M\|} \to Fun seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\}))$
28	18 27	syl	$⊢ φ \to Fun seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\}))$
29		fvexd	$⊢ φ \to (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\}) (\|M\|) \in V$
30		ovexd	$⊢ (φ \land (a \in V \land b \in V)) \to a (x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩) b \in V$
31		eqid	$⊢ ℤ_{\geq \|M\|} = ℤ_{\geq \|M\|}$
32		fvexd	$⊢ (φ \land a \in ℤ_{\geq (\|M\| + 1)}) \to (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\}) (a) \in V$
33	29 30 31 16 32	seqf2	$⊢ φ \to seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})) : ℤ_{\geq \|M\|} ⟶ V$
34	33	fdmd	$⊢ φ \to dom seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})) = ℤ_{\geq \|M\|}$
35	5 34	eleqtrrd	$⊢ φ \to N \in dom seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\}))$
36		fvco	$⊢ (Fun seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})) \land N \in dom seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\}))) \to (lastS \circ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\}))) (N) = lastS (seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})) (N))$
37	28 35 36	syl2anc	$⊢ φ \to (lastS \circ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\}))) (N) = lastS (seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})) (N))$
38	7 26 37	3eqtrd	$⊢ φ \to (M {seq}_{str} F) (N) = lastS (seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})) (N))$

Metamath Proof Explorer

Theorem sseqfv2

Proof