Metamath Proof Explorer


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 φ S V
sseqval.2 φ M Word S
sseqval.3 W = Word S . -1 M
sseqval.4 φ F : W S
Assertion sseqfn φ M seq str F Fn 0

Proof

Step Hyp Ref Expression
1 sseqval.1 φ S V
2 sseqval.2 φ M Word S
3 sseqval.3 W = Word S . -1 M
4 sseqval.4 φ F : W S
5 wrdfn M Word S M Fn 0 ..^ M
6 2 5 syl φ M Fn 0 ..^ M
7 fvex x x 1 V
8 df-lsw lastS = x V x x 1
9 7 8 fnmpti lastS Fn V
10 9 a1i φ lastS Fn V
11 lencl M Word S M 0
12 11 nn0zd M Word S M
13 seqfn M seq M x V , y V x ++ ⟨“ F x ”⟩ 0 × M ++ ⟨“ F M ”⟩ Fn M
14 2 12 13 3syl φ seq M x V , y V x ++ ⟨“ F x ”⟩ 0 × M ++ ⟨“ F M ”⟩ Fn M
15 ssv ran seq M x V , y V x ++ ⟨“ F x ”⟩ 0 × M ++ ⟨“ F M ”⟩ V
16 15 a1i φ ran seq M x V , y V x ++ ⟨“ F x ”⟩ 0 × M ++ ⟨“ F M ”⟩ V
17 fnco lastS Fn V seq M x V , y V x ++ ⟨“ F x ”⟩ 0 × M ++ ⟨“ F M ”⟩ Fn M ran seq M x V , y V x ++ ⟨“ F x ”⟩ 0 × M ++ ⟨“ F M ”⟩ V lastS seq M x V , y V x ++ ⟨“ F x ”⟩ 0 × M ++ ⟨“ F M ”⟩ Fn M
18 10 14 16 17 syl3anc φ lastS seq M x V , y V x ++ ⟨“ F x ”⟩ 0 × M ++ ⟨“ F M ”⟩ Fn M
19 fzouzdisj 0 ..^ M M =
20 19 a1i φ 0 ..^ M M =
21 fnun M Fn 0 ..^ M lastS seq M x V , y V x ++ ⟨“ F x ”⟩ 0 × M ++ ⟨“ F M ”⟩ Fn M 0 ..^ M M = M lastS seq M x V , y V x ++ ⟨“ F x ”⟩ 0 × M ++ ⟨“ F M ”⟩ Fn 0 ..^ M M
22 6 18 20 21 syl21anc φ M lastS seq M x V , y V x ++ ⟨“ F x ”⟩ 0 × M ++ ⟨“ F M ”⟩ Fn 0 ..^ M M
23 1 2 3 4 sseqval φ M seq str F = M lastS seq M x V , y V x ++ ⟨“ F x ”⟩ 0 × M ++ ⟨“ F M ”⟩
24 nn0uz 0 = 0
25 elnn0uz M 0 M 0
26 fzouzsplit M 0 0 = 0 ..^ M M
27 25 26 sylbi M 0 0 = 0 ..^ M M
28 2 11 27 3syl φ 0 = 0 ..^ M M
29 24 28 syl5eq φ 0 = 0 ..^ M M
30 23 29 fneq12d φ M seq str F Fn 0 M lastS seq M x V , y V x ++ ⟨“ F x ”⟩ 0 × M ++ ⟨“ F M ”⟩ Fn 0 ..^ M M
31 22 30 mpbird φ M seq str F Fn 0