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	4 28	fexd	⊢ ( 𝜑 → 𝐹 ∈ V )
30		df-lsw	⊢ lastS = ( 𝑥 ∈ V ↦ ( 𝑥 ‘ ( ( ♯ ‘ 𝑥 ) − 1 ) ) )
31	30	funmpt2	⊢ Fun lastS
32	31	a1i	⊢ ( 𝜑 → Fun lastS )
33		seqex	⊢ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ∈ V
34	33	a1i	⊢ ( 𝜑 → seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ∈ V )
35		cofunexg	⊢ ( ( Fun lastS ∧ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ∈ V ) → ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) ∈ V )
36	32 34 35	syl2anc	⊢ ( 𝜑 → ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) ∈ V )
37		unexg	⊢ ( ( 𝑀 ∈ V ∧ ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) ∈ V ) → ( 𝑀 ∪ ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) ) ∈ V )
38	24 36 37	syl2anc	⊢ ( 𝜑 → ( 𝑀 ∪ ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) ) ∈ V )
39	6 22 24 29 38	ovmpod	⊢ ( 𝜑 → ( 𝑀 seqstr 𝐹 ) = ( 𝑀 ∪ ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) ) )