Theorem sseqfn

Description: A strong recursive sequence is a function over the nonnegative integers. (Contributed by Thierry Arnoux, 23-Apr-2019)

	Ref	Expression
Hypotheses	sseqval.1	⊢ ( 𝜑 → 𝑆 ∈ V )
	sseqval.2	⊢ ( 𝜑 → 𝑀 ∈ Word 𝑆 )
	sseqval.3	⊢ 𝑊 = ( Word 𝑆 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ) )
	sseqval.4	⊢ ( 𝜑 → 𝐹 : 𝑊 ⟶ 𝑆 )
Assertion	sseqfn	⊢ ( 𝜑 → ( 𝑀 seqstr 𝐹 ) Fn ℕ0 )

Proof

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