Theorem 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	⊢ ( 𝜑 → 𝑆 ∈ V )
	sseqval.2	⊢ ( 𝜑 → 𝑀 ∈ Word 𝑆 )
	sseqval.3	⊢ 𝑊 = ( Word 𝑆 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ) )
	sseqval.4	⊢ ( 𝜑 → 𝐹 : 𝑊 ⟶ 𝑆 )
	sseqfv1.4	⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑀 ) ) )
Assertion	sseqfv1	⊢ ( 𝜑 → ( ( 𝑀 seqstr 𝐹 ) ‘ 𝑁 ) = ( 𝑀 ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		sseqval.1	⊢ ( 𝜑 → 𝑆 ∈ V )
2		sseqval.2	⊢ ( 𝜑 → 𝑀 ∈ Word 𝑆 )
3		sseqval.3	⊢ 𝑊 = ( Word 𝑆 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ) )
4		sseqval.4	⊢ ( 𝜑 → 𝐹 : 𝑊 ⟶ 𝑆 )
5		sseqfv1.4	⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑀 ) ) )
6	1 2 3 4	sseqval	⊢ ( 𝜑 → ( 𝑀 seqstr 𝐹 ) = ( 𝑀 ∪ ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) ) )
7	6	fveq1d	⊢ ( 𝜑 → ( ( 𝑀 seqstr 𝐹 ) ‘ 𝑁 ) = ( ( 𝑀 ∪ ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) ) ‘ 𝑁 ) )
8		wrdfn	⊢ ( 𝑀 ∈ Word 𝑆 → 𝑀 Fn ( 0 ..^ ( ♯ ‘ 𝑀 ) ) )
9	2 8	syl	⊢ ( 𝜑 → 𝑀 Fn ( 0 ..^ ( ♯ ‘ 𝑀 ) ) )
10		fvex	⊢ ( 𝑥 ‘ ( ( ♯ ‘ 𝑥 ) − 1 ) ) ∈ V
11		df-lsw	⊢ lastS = ( 𝑥 ∈ V ↦ ( 𝑥 ‘ ( ( ♯ ‘ 𝑥 ) − 1 ) ) )
12	10 11	fnmpti	⊢ lastS Fn V
13	12	a1i	⊢ ( 𝜑 → lastS Fn V )
14		lencl	⊢ ( 𝑀 ∈ Word 𝑆 → ( ♯ ‘ 𝑀 ) ∈ ℕ0 )
15	2 14	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝑀 ) ∈ ℕ0 )
16	15	nn0zd	⊢ ( 𝜑 → ( ♯ ‘ 𝑀 ) ∈ ℤ )
17		seqfn	⊢ ( ( ♯ ‘ 𝑀 ) ∈ ℤ → seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) Fn ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) )
18	16 17	syl	⊢ ( 𝜑 → seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) Fn ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) )
19		ssv	⊢ ran seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ⊆ V
20	19	a1i	⊢ ( 𝜑 → ran seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ⊆ V )
21		fnco	⊢ ( ( lastS Fn V ∧ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) Fn ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ∧ ran seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ⊆ V ) → ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) Fn ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) )
22	13 18 20 21	syl3anc	⊢ ( 𝜑 → ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) Fn ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) )
23		fzouzdisj	⊢ ( ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ∩ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ) = ∅
24	23	a1i	⊢ ( 𝜑 → ( ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ∩ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ) = ∅ )
25		fvun1	⊢ ( ( 𝑀 Fn ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ∧ ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) Fn ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ∧ ( ( ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ∩ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ) = ∅ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ) ) → ( ( 𝑀 ∪ ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) ) ‘ 𝑁 ) = ( 𝑀 ‘ 𝑁 ) )
26	9 22 24 5 25	syl112anc	⊢ ( 𝜑 → ( ( 𝑀 ∪ ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) ) ‘ 𝑁 ) = ( 𝑀 ‘ 𝑁 ) )
27	7 26	eqtrd	⊢ ( 𝜑 → ( ( 𝑀 seqstr 𝐹 ) ‘ 𝑁 ) = ( 𝑀 ‘ 𝑁 ) )