# 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 ${⊢}{\phi }\to {S}\in \mathrm{V}$
sseqval.2 ${⊢}{\phi }\to {M}\in \mathrm{Word}{S}$
sseqval.3 ${⊢}{W}=\mathrm{Word}{S}\cap {\left|.\right|}^{-1}\left[{ℤ}_{\ge \left|{M}\right|}\right]$
sseqval.4 ${⊢}{\phi }\to {F}:{W}⟶{S}$
Assertion sseqfn ${⊢}{\phi }\to \left({M}{\mathrm{seq}}_{str}{F}\right)Fn{ℕ}_{0}$

### Proof

Step Hyp Ref Expression
1 sseqval.1 ${⊢}{\phi }\to {S}\in \mathrm{V}$
2 sseqval.2 ${⊢}{\phi }\to {M}\in \mathrm{Word}{S}$
3 sseqval.3 ${⊢}{W}=\mathrm{Word}{S}\cap {\left|.\right|}^{-1}\left[{ℤ}_{\ge \left|{M}\right|}\right]$
4 sseqval.4 ${⊢}{\phi }\to {F}:{W}⟶{S}$
5 wrdfn ${⊢}{M}\in \mathrm{Word}{S}\to {M}Fn\left(0..^\left|{M}\right|\right)$
6 2 5 syl ${⊢}{\phi }\to {M}Fn\left(0..^\left|{M}\right|\right)$
7 fvex ${⊢}{x}\left(\left|{x}\right|-1\right)\in \mathrm{V}$
8 df-lsw ${⊢}\mathrm{lastS}=\left({x}\in \mathrm{V}⟼{x}\left(\left|{x}\right|-1\right)\right)$
9 7 8 fnmpti ${⊢}\mathrm{lastS}Fn\mathrm{V}$
10 9 a1i ${⊢}{\phi }\to \mathrm{lastS}Fn\mathrm{V}$
11 lencl ${⊢}{M}\in \mathrm{Word}{S}\to \left|{M}\right|\in {ℕ}_{0}$
12 11 nn0zd ${⊢}{M}\in \mathrm{Word}{S}\to \left|{M}\right|\in ℤ$
13 seqfn ${⊢}\left|{M}\right|\in ℤ\to seq\left|{M}\right|\left(\left({x}\in \mathrm{V},{y}\in \mathrm{V}⟼{x}\mathrm{++}⟨“{F}\left({x}\right)”⟩\right),\left({ℕ}_{0}×\left\{{M}\mathrm{++}⟨“{F}\left({M}\right)”⟩\right\}\right)\right)Fn{ℤ}_{\ge \left|{M}\right|}$
14 2 12 13 3syl ${⊢}{\phi }\to seq\left|{M}\right|\left(\left({x}\in \mathrm{V},{y}\in \mathrm{V}⟼{x}\mathrm{++}⟨“{F}\left({x}\right)”⟩\right),\left({ℕ}_{0}×\left\{{M}\mathrm{++}⟨“{F}\left({M}\right)”⟩\right\}\right)\right)Fn{ℤ}_{\ge \left|{M}\right|}$
15 ssv ${⊢}\mathrm{ran}seq\left|{M}\right|\left(\left({x}\in \mathrm{V},{y}\in \mathrm{V}⟼{x}\mathrm{++}⟨“{F}\left({x}\right)”⟩\right),\left({ℕ}_{0}×\left\{{M}\mathrm{++}⟨“{F}\left({M}\right)”⟩\right\}\right)\right)\subseteq \mathrm{V}$
16 15 a1i ${⊢}{\phi }\to \mathrm{ran}seq\left|{M}\right|\left(\left({x}\in \mathrm{V},{y}\in \mathrm{V}⟼{x}\mathrm{++}⟨“{F}\left({x}\right)”⟩\right),\left({ℕ}_{0}×\left\{{M}\mathrm{++}⟨“{F}\left({M}\right)”⟩\right\}\right)\right)\subseteq \mathrm{V}$
17 fnco ${⊢}\left(\mathrm{lastS}Fn\mathrm{V}\wedge seq\left|{M}\right|\left(\left({x}\in \mathrm{V},{y}\in \mathrm{V}⟼{x}\mathrm{++}⟨“{F}\left({x}\right)”⟩\right),\left({ℕ}_{0}×\left\{{M}\mathrm{++}⟨“{F}\left({M}\right)”⟩\right\}\right)\right)Fn{ℤ}_{\ge \left|{M}\right|}\wedge \mathrm{ran}seq\left|{M}\right|\left(\left({x}\in \mathrm{V},{y}\in \mathrm{V}⟼{x}\mathrm{++}⟨“{F}\left({x}\right)”⟩\right),\left({ℕ}_{0}×\left\{{M}\mathrm{++}⟨“{F}\left({M}\right)”⟩\right\}\right)\right)\subseteq \mathrm{V}\right)\to \left(\mathrm{lastS}\circ seq\left|{M}\right|\left(\left({x}\in \mathrm{V},{y}\in \mathrm{V}⟼{x}\mathrm{++}⟨“{F}\left({x}\right)”⟩\right),\left({ℕ}_{0}×\left\{{M}\mathrm{++}⟨“{F}\left({M}\right)”⟩\right\}\right)\right)\right)Fn{ℤ}_{\ge \left|{M}\right|}$
18 10 14 16 17 syl3anc ${⊢}{\phi }\to \left(\mathrm{lastS}\circ seq\left|{M}\right|\left(\left({x}\in \mathrm{V},{y}\in \mathrm{V}⟼{x}\mathrm{++}⟨“{F}\left({x}\right)”⟩\right),\left({ℕ}_{0}×\left\{{M}\mathrm{++}⟨“{F}\left({M}\right)”⟩\right\}\right)\right)\right)Fn{ℤ}_{\ge \left|{M}\right|}$
19 fzouzdisj ${⊢}\left(0..^\left|{M}\right|\right)\cap {ℤ}_{\ge \left|{M}\right|}=\varnothing$
20 19 a1i ${⊢}{\phi }\to \left(0..^\left|{M}\right|\right)\cap {ℤ}_{\ge \left|{M}\right|}=\varnothing$
21 fnun ${⊢}\left(\left({M}Fn\left(0..^\left|{M}\right|\right)\wedge \left(\mathrm{lastS}\circ seq\left|{M}\right|\left(\left({x}\in \mathrm{V},{y}\in \mathrm{V}⟼{x}\mathrm{++}⟨“{F}\left({x}\right)”⟩\right),\left({ℕ}_{0}×\left\{{M}\mathrm{++}⟨“{F}\left({M}\right)”⟩\right\}\right)\right)\right)Fn{ℤ}_{\ge \left|{M}\right|}\right)\wedge \left(0..^\left|{M}\right|\right)\cap {ℤ}_{\ge \left|{M}\right|}=\varnothing \right)\to \left({M}\cup \left(\mathrm{lastS}\circ seq\left|{M}\right|\left(\left({x}\in \mathrm{V},{y}\in \mathrm{V}⟼{x}\mathrm{++}⟨“{F}\left({x}\right)”⟩\right),\left({ℕ}_{0}×\left\{{M}\mathrm{++}⟨“{F}\left({M}\right)”⟩\right\}\right)\right)\right)\right)Fn\left(\left(0..^\left|{M}\right|\right)\cup {ℤ}_{\ge \left|{M}\right|}\right)$
22 6 18 20 21 syl21anc ${⊢}{\phi }\to \left({M}\cup \left(\mathrm{lastS}\circ seq\left|{M}\right|\left(\left({x}\in \mathrm{V},{y}\in \mathrm{V}⟼{x}\mathrm{++}⟨“{F}\left({x}\right)”⟩\right),\left({ℕ}_{0}×\left\{{M}\mathrm{++}⟨“{F}\left({M}\right)”⟩\right\}\right)\right)\right)\right)Fn\left(\left(0..^\left|{M}\right|\right)\cup {ℤ}_{\ge \left|{M}\right|}\right)$
23 1 2 3 4 sseqval ${⊢}{\phi }\to {M}{\mathrm{seq}}_{str}{F}={M}\cup \left(\mathrm{lastS}\circ seq\left|{M}\right|\left(\left({x}\in \mathrm{V},{y}\in \mathrm{V}⟼{x}\mathrm{++}⟨“{F}\left({x}\right)”⟩\right),\left({ℕ}_{0}×\left\{{M}\mathrm{++}⟨“{F}\left({M}\right)”⟩\right\}\right)\right)\right)$
24 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
25 elnn0uz ${⊢}\left|{M}\right|\in {ℕ}_{0}↔\left|{M}\right|\in {ℤ}_{\ge 0}$
26 fzouzsplit ${⊢}\left|{M}\right|\in {ℤ}_{\ge 0}\to {ℤ}_{\ge 0}=\left(0..^\left|{M}\right|\right)\cup {ℤ}_{\ge \left|{M}\right|}$
27 25 26 sylbi ${⊢}\left|{M}\right|\in {ℕ}_{0}\to {ℤ}_{\ge 0}=\left(0..^\left|{M}\right|\right)\cup {ℤ}_{\ge \left|{M}\right|}$
28 2 11 27 3syl ${⊢}{\phi }\to {ℤ}_{\ge 0}=\left(0..^\left|{M}\right|\right)\cup {ℤ}_{\ge \left|{M}\right|}$
29 24 28 syl5eq ${⊢}{\phi }\to {ℕ}_{0}=\left(0..^\left|{M}\right|\right)\cup {ℤ}_{\ge \left|{M}\right|}$
30 23 29 fneq12d ${⊢}{\phi }\to \left(\left({M}{\mathrm{seq}}_{str}{F}\right)Fn{ℕ}_{0}↔\left({M}\cup \left(\mathrm{lastS}\circ seq\left|{M}\right|\left(\left({x}\in \mathrm{V},{y}\in \mathrm{V}⟼{x}\mathrm{++}⟨“{F}\left({x}\right)”⟩\right),\left({ℕ}_{0}×\left\{{M}\mathrm{++}⟨“{F}\left({M}\right)”⟩\right\}\right)\right)\right)\right)Fn\left(\left(0..^\left|{M}\right|\right)\cup {ℤ}_{\ge \left|{M}\right|}\right)\right)$
31 22 30 mpbird ${⊢}{\phi }\to \left({M}{\mathrm{seq}}_{str}{F}\right)Fn{ℕ}_{0}$