sseqval

Description: Value of the strong sequence builder function. The set W represents here the words of length greater than or equal to the lenght of the initial sequence M . (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$
Assertion	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) ”⟩\})))$

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		df-sseq	$⊢ {seq}_{str} = (m \in V, f \in V ⟼ m \cup (lastS \circ seq \|m\| ((x \in V, y \in V ⟼ x ++ ⟨“ f (x) ”⟩), (ℕ_{0} \times \{m ++ ⟨“ f (m) ”⟩\}))))$
6	5	a1i	$⊢ φ \to {seq}_{str} = (m \in V, f \in V ⟼ m \cup (lastS \circ seq \|m\| ((x \in V, y \in V ⟼ x ++ ⟨“ f (x) ”⟩), (ℕ_{0} \times \{m ++ ⟨“ f (m) ”⟩\}))))$
7		simprl	$⊢ (φ \land (m = M \land f = F)) \to m = M$
8	7	fveq2d	$⊢ (φ \land (m = M \land f = F)) \to \|m\| = \|M\|$
9		simp1rr	$⊢ ((φ \land (m = M \land f = F)) \land x \in V \land y \in V) \to f = F$
10	9	fveq1d	$⊢ ((φ \land (m = M \land f = F)) \land x \in V \land y \in V) \to f (x) = F (x)$
11	10	s1eqd	$⊢ ((φ \land (m = M \land f = F)) \land x \in V \land y \in V) \to ⟨“ f (x) ”⟩ = ⟨“ F (x) ”⟩$
12	11	oveq2d	$⊢ ((φ \land (m = M \land f = F)) \land x \in V \land y \in V) \to x ++ ⟨“ f (x) ”⟩ = x ++ ⟨“ F (x) ”⟩$
13	12	mpoeq3dva	$⊢ (φ \land (m = M \land f = F)) \to (x \in V, y \in V ⟼ x ++ ⟨“ f (x) ”⟩) = (x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩)$
14		simprr	$⊢ (φ \land (m = M \land f = F)) \to f = F$
15	14 7	fveq12d	$⊢ (φ \land (m = M \land f = F)) \to f (m) = F (M)$
16	15	s1eqd	$⊢ (φ \land (m = M \land f = F)) \to ⟨“ f (m) ”⟩ = ⟨“ F (M) ”⟩$
17	7 16	oveq12d	$⊢ (φ \land (m = M \land f = F)) \to m ++ ⟨“ f (m) ”⟩ = M ++ ⟨“ F (M) ”⟩$
18	17	sneqd	$⊢ (φ \land (m = M \land f = F)) \to \{m ++ ⟨“ f (m) ”⟩\} = \{M ++ ⟨“ F (M) ”⟩\}$
19	18	xpeq2d	$⊢ (φ \land (m = M \land f = F)) \to ℕ_{0} \times \{m ++ ⟨“ f (m) ”⟩\} = ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\}$
20	8 13 19	seqeq123d	$⊢ (φ \land (m = M \land f = F)) \to seq \|m\| ((x \in V, y \in V ⟼ x ++ ⟨“ f (x) ”⟩), (ℕ_{0} \times \{m ++ ⟨“ f (m) ”⟩\})) = seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\}))$
21	20	coeq2d	$⊢ (φ \land (m = M \land f = F)) \to lastS \circ seq \|m\| ((x \in V, y \in V ⟼ x ++ ⟨“ f (x) ”⟩), (ℕ_{0} \times \{m ++ ⟨“ f (m) ”⟩\})) = lastS \circ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\}))$
22	7 21	uneq12d	$⊢ (φ \land (m = M \land f = F)) \to m \cup (lastS \circ seq \|m\| ((x \in V, y \in V ⟼ x ++ ⟨“ f (x) ”⟩), (ℕ_{0} \times \{m ++ ⟨“ f (m) ”⟩\}))) = M \cup (lastS \circ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})))$
23		elex	$⊢ M \in Word S \to M \in V$
24	2 23	syl	$⊢ φ \to M \in V$
25		wrdexg	$⊢ S \in V \to Word S \in V$
26		inex1g	$⊢ Word S \in V \to Word S \cap {\|.\|}^{-1} [ℤ_{\geq \|M\|}] \in V$
27	1 25 26	3syl	$⊢ φ \to Word S \cap {\|.\|}^{-1} [ℤ_{\geq \|M\|}] \in V$
28	3 27	eqeltrid	$⊢ φ \to W \in V$
29	4 28	fexd	$⊢ φ \to F \in V$
30		df-lsw	$⊢ lastS = (x \in V ⟼ x (\|x\| - 1))$
31	30	funmpt2	$⊢ Fun lastS$
32	31	a1i	$⊢ φ \to Fun lastS$
33		seqex	$⊢ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})) \in V$
34	33	a1i	$⊢ φ \to seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})) \in V$
35		cofunexg	$⊢ (Fun lastS \land seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})) \in V) \to lastS \circ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})) \in V$
36	32 34 35	syl2anc	$⊢ φ \to lastS \circ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})) \in V$
37		unexg	$⊢ (M \in V \land lastS \circ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\})) \in V) \to M \cup (lastS \circ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\}))) \in V$
38	24 36 37	syl2anc	$⊢ φ \to M \cup (lastS \circ seq \|M\| ((x \in V, y \in V ⟼ x ++ ⟨“ F (x) ”⟩), (ℕ_{0} \times \{M ++ ⟨“ F (M) ”⟩\}))) \in V$
39	6 22 24 29 38	ovmpod	$⊢ φ \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) ”⟩\})))$

Metamath Proof Explorer

Theorem sseqval

Proof