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 
|- ( ph -> S e. _V )
sseqval.2 
|- ( ph -> M e. Word S )
sseqval.3 
|- W = ( Word S i^i ( `' # " ( ZZ>= ` ( # ` M ) ) ) )
sseqval.4 
|- ( ph -> F : W --> S )
Assertion sseqfn 
|- ( ph -> ( M seqstr F ) Fn NN0 )

Proof

Step Hyp Ref Expression
1 sseqval.1 
 |-  ( ph -> S e. _V )
2 sseqval.2 
 |-  ( ph -> M e. Word S )
3 sseqval.3 
 |-  W = ( Word S i^i ( `' # " ( ZZ>= ` ( # ` M ) ) ) )
4 sseqval.4 
 |-  ( ph -> F : W --> S )
5 wrdfn 
 |-  ( M e. Word S -> M Fn ( 0 ..^ ( # ` M ) ) )
6 2 5 syl 
 |-  ( ph -> M Fn ( 0 ..^ ( # ` M ) ) )
7 fvex 
 |-  ( x ` ( ( # ` x ) - 1 ) ) e. _V
8 df-lsw 
 |-  lastS = ( x e. _V |-> ( x ` ( ( # ` x ) - 1 ) ) )
9 7 8 fnmpti 
 |-  lastS Fn _V
10 9 a1i 
 |-  ( ph -> lastS Fn _V )
11 lencl 
 |-  ( M e. Word S -> ( # ` M ) e. NN0 )
12 11 nn0zd 
 |-  ( M e. Word S -> ( # ` M ) e. ZZ )
13 seqfn 
 |-  ( ( # ` M ) e. ZZ -> seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) Fn ( ZZ>= ` ( # ` M ) ) )
14 2 12 13 3syl 
 |-  ( ph -> seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) Fn ( ZZ>= ` ( # ` M ) ) )
15 ssv 
 |-  ran seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) C_ _V
16 15 a1i 
 |-  ( ph -> ran seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) C_ _V )
17 fnco 
 |-  ( ( lastS Fn _V /\ seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) Fn ( ZZ>= ` ( # ` M ) ) /\ ran seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) C_ _V ) -> ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) Fn ( ZZ>= ` ( # ` M ) ) )
18 10 14 16 17 syl3anc 
 |-  ( ph -> ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) Fn ( ZZ>= ` ( # ` M ) ) )
19 fzouzdisj 
 |-  ( ( 0 ..^ ( # ` M ) ) i^i ( ZZ>= ` ( # ` M ) ) ) = (/)
20 19 a1i 
 |-  ( ph -> ( ( 0 ..^ ( # ` M ) ) i^i ( ZZ>= ` ( # ` M ) ) ) = (/) )
21 6 18 20 fnund 
 |-  ( ph -> ( M u. ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) ) Fn ( ( 0 ..^ ( # ` M ) ) u. ( ZZ>= ` ( # ` M ) ) ) )
22 1 2 3 4 sseqval 
 |-  ( ph -> ( M seqstr F ) = ( M u. ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) ) )
23 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
24 elnn0uz 
 |-  ( ( # ` M ) e. NN0 <-> ( # ` M ) e. ( ZZ>= ` 0 ) )
25 fzouzsplit 
 |-  ( ( # ` M ) e. ( ZZ>= ` 0 ) -> ( ZZ>= ` 0 ) = ( ( 0 ..^ ( # ` M ) ) u. ( ZZ>= ` ( # ` M ) ) ) )
26 24 25 sylbi 
 |-  ( ( # ` M ) e. NN0 -> ( ZZ>= ` 0 ) = ( ( 0 ..^ ( # ` M ) ) u. ( ZZ>= ` ( # ` M ) ) ) )
27 2 11 26 3syl 
 |-  ( ph -> ( ZZ>= ` 0 ) = ( ( 0 ..^ ( # ` M ) ) u. ( ZZ>= ` ( # ` M ) ) ) )
28 23 27 eqtrid 
 |-  ( ph -> NN0 = ( ( 0 ..^ ( # ` M ) ) u. ( ZZ>= ` ( # ` M ) ) ) )
29 22 28 fneq12d 
 |-  ( ph -> ( ( M seqstr F ) Fn NN0 <-> ( M u. ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) ) Fn ( ( 0 ..^ ( # ` M ) ) u. ( ZZ>= ` ( # ` M ) ) ) ) )
30 21 29 mpbird 
 |-  ( ph -> ( M seqstr F ) Fn NN0 )