Theorem 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	⊢ ( 𝜑 → 𝑆 ∈ V )
	sseqval.2	⊢ ( 𝜑 → 𝑀 ∈ Word 𝑆 )
	sseqval.3	⊢ 𝑊 = ( Word 𝑆 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ) )
	sseqval.4	⊢ ( 𝜑 → 𝐹 : 𝑊 ⟶ 𝑆 )
Assertion	sseqval	⊢ ( 𝜑 → ( 𝑀 seqstr 𝐹 ) = ( 𝑀 ∪ ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		sseqval.1	⊢ ( 𝜑 → 𝑆 ∈ V )
2		sseqval.2	⊢ ( 𝜑 → 𝑀 ∈ Word 𝑆 )
3		sseqval.3	⊢ 𝑊 = ( Word 𝑆 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ) )
4		sseqval.4	⊢ ( 𝜑 → 𝐹 : 𝑊 ⟶ 𝑆 )
5		df-sseq	⊢ seqstr = ( 𝑚 ∈ V , 𝑓 ∈ V ↦ ( 𝑚 ∪ ( lastS ∘ seq ( ♯ ‘ 𝑚 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝑓 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑚 ++ ⟨“ ( 𝑓 ‘ 𝑚 ) ”⟩ ) } ) ) ) ) )
6	5	a1i	⊢ ( 𝜑 → seqstr = ( 𝑚 ∈ V , 𝑓 ∈ V ↦ ( 𝑚 ∪ ( lastS ∘ seq ( ♯ ‘ 𝑚 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝑓 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑚 ++ ⟨“ ( 𝑓 ‘ 𝑚 ) ”⟩ ) } ) ) ) ) ) )
7		simprl	⊢ ( ( 𝜑 ∧ ( 𝑚 = 𝑀 ∧ 𝑓 = 𝐹 ) ) → 𝑚 = 𝑀 )
8	7	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑚 = 𝑀 ∧ 𝑓 = 𝐹 ) ) → ( ♯ ‘ 𝑚 ) = ( ♯ ‘ 𝑀 ) )
9		simp1rr	⊢ ( ( ( 𝜑 ∧ ( 𝑚 = 𝑀 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑥 ∈ V ∧ 𝑦 ∈ V ) → 𝑓 = 𝐹 )
10	9	fveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑚 = 𝑀 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
11	10	s1eqd	⊢ ( ( ( 𝜑 ∧ ( 𝑚 = 𝑀 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ⟨“ ( 𝑓 ‘ 𝑥 ) ”⟩ = ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ )
12	11	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑚 = 𝑀 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 ++ ⟨“ ( 𝑓 ‘ 𝑥 ) ”⟩ ) = ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) )
13	12	mpoeq3dva	⊢ ( ( 𝜑 ∧ ( 𝑚 = 𝑀 ∧ 𝑓 = 𝐹 ) ) → ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝑓 ‘ 𝑥 ) ”⟩ ) ) = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) )
14		simprr	⊢ ( ( 𝜑 ∧ ( 𝑚 = 𝑀 ∧ 𝑓 = 𝐹 ) ) → 𝑓 = 𝐹 )
15	14 7	fveq12d	⊢ ( ( 𝜑 ∧ ( 𝑚 = 𝑀 ∧ 𝑓 = 𝐹 ) ) → ( 𝑓 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑀 ) )
16	15	s1eqd	⊢ ( ( 𝜑 ∧ ( 𝑚 = 𝑀 ∧ 𝑓 = 𝐹 ) ) → ⟨“ ( 𝑓 ‘ 𝑚 ) ”⟩ = ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ )
17	7 16	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑚 = 𝑀 ∧ 𝑓 = 𝐹 ) ) → ( 𝑚 ++ ⟨“ ( 𝑓 ‘ 𝑚 ) ”⟩ ) = ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) )
18	17	sneqd	⊢ ( ( 𝜑 ∧ ( 𝑚 = 𝑀 ∧ 𝑓 = 𝐹 ) ) → { ( 𝑚 ++ ⟨“ ( 𝑓 ‘ 𝑚 ) ”⟩ ) } = { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } )
19	18	xpeq2d	⊢ ( ( 𝜑 ∧ ( 𝑚 = 𝑀 ∧ 𝑓 = 𝐹 ) ) → ( ℕ0 × { ( 𝑚 ++ ⟨“ ( 𝑓 ‘ 𝑚 ) ”⟩ ) } ) = ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) )
20	8 13 19	seqeq123d	⊢ ( ( 𝜑 ∧ ( 𝑚 = 𝑀 ∧ 𝑓 = 𝐹 ) ) → seq ( ♯ ‘ 𝑚 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝑓 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑚 ++ ⟨“ ( 𝑓 ‘ 𝑚 ) ”⟩ ) } ) ) = seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) )
21	20	coeq2d	⊢ ( ( 𝜑 ∧ ( 𝑚 = 𝑀 ∧ 𝑓 = 𝐹 ) ) → ( lastS ∘ seq ( ♯ ‘ 𝑚 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝑓 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑚 ++ ⟨“ ( 𝑓 ‘ 𝑚 ) ”⟩ ) } ) ) ) = ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) )
22	7 21	uneq12d	⊢ ( ( 𝜑 ∧ ( 𝑚 = 𝑀 ∧ 𝑓 = 𝐹 ) ) → ( 𝑚 ∪ ( lastS ∘ seq ( ♯ ‘ 𝑚 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝑓 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑚 ++ ⟨“ ( 𝑓 ‘ 𝑚 ) ”⟩ ) } ) ) ) ) = ( 𝑀 ∪ ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) ) )
23		elex	⊢ ( 𝑀 ∈ Word 𝑆 → 𝑀 ∈ V )
24	2 23	syl	⊢ ( 𝜑 → 𝑀 ∈ V )
25		wrdexg	⊢ ( 𝑆 ∈ V → Word 𝑆 ∈ V )
26		inex1g	⊢ ( Word 𝑆 ∈ V → ( Word 𝑆 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ) ) ∈ V )
27	1 25 26	3syl	⊢ ( 𝜑 → ( Word 𝑆 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ) ) ∈ V )
28	3 27	eqeltrid	⊢ ( 𝜑 → 𝑊 ∈ V )
29		fex	⊢ ( ( 𝐹 : 𝑊 ⟶ 𝑆 ∧ 𝑊 ∈ V ) → 𝐹 ∈ V )
30	4 28 29	syl2anc	⊢ ( 𝜑 → 𝐹 ∈ V )
31		df-lsw	⊢ lastS = ( 𝑥 ∈ V ↦ ( 𝑥 ‘ ( ( ♯ ‘ 𝑥 ) − 1 ) ) )
32	31	funmpt2	⊢ Fun lastS
33	32	a1i	⊢ ( 𝜑 → Fun lastS )
34		seqex	⊢ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ∈ V
35	34	a1i	⊢ ( 𝜑 → seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ∈ V )
36		cofunexg	⊢ ( ( Fun lastS ∧ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ∈ V ) → ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) ∈ V )
37	33 35 36	syl2anc	⊢ ( 𝜑 → ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) ∈ V )
38		unexg	⊢ ( ( 𝑀 ∈ V ∧ ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) ∈ V ) → ( 𝑀 ∪ ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) ) ∈ V )
39	24 37 38	syl2anc	⊢ ( 𝜑 → ( 𝑀 ∪ ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) ) ∈ V )
40	6 22 24 30 39	ovmpod	⊢ ( 𝜑 → ( 𝑀 seqstr 𝐹 ) = ( 𝑀 ∪ ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) ) )