Metamath Proof Explorer


Theorem sseqf

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

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

Proof

Step Hyp Ref Expression
1 sseqval.1 ( 𝜑𝑆 ∈ V )
2 sseqval.2 ( 𝜑𝑀 ∈ Word 𝑆 )
3 sseqval.3 𝑊 = ( Word 𝑆 ∩ ( ♯ “ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) )
4 sseqval.4 ( 𝜑𝐹 : 𝑊𝑆 )
5 wrdf ( 𝑀 ∈ Word 𝑆𝑀 : ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ⟶ 𝑆 )
6 2 5 syl ( 𝜑𝑀 : ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ⟶ 𝑆 )
7 vex 𝑤 ∈ V
8 7 a1i ( ( 𝜑𝑤 ∈ ( 𝑊 ∖ { ∅ } ) ) → 𝑤 ∈ V )
9 fvex ( 𝑥 ‘ ( ( ♯ ‘ 𝑥 ) − 1 ) ) ∈ V
10 df-lsw lastS = ( 𝑥 ∈ V ↦ ( 𝑥 ‘ ( ( ♯ ‘ 𝑥 ) − 1 ) ) )
11 9 10 dmmpti dom lastS = V
12 8 11 eleqtrrdi ( ( 𝜑𝑤 ∈ ( 𝑊 ∖ { ∅ } ) ) → 𝑤 ∈ dom lastS )
13 eldifsn ( 𝑤 ∈ ( 𝑊 ∖ { ∅ } ) ↔ ( 𝑤𝑊𝑤 ≠ ∅ ) )
14 inss1 ( Word 𝑆 ∩ ( ♯ “ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) ) ⊆ Word 𝑆
15 3 14 eqsstri 𝑊 ⊆ Word 𝑆
16 15 sseli ( 𝑤𝑊𝑤 ∈ Word 𝑆 )
17 lswcl ( ( 𝑤 ∈ Word 𝑆𝑤 ≠ ∅ ) → ( lastS ‘ 𝑤 ) ∈ 𝑆 )
18 16 17 sylan ( ( 𝑤𝑊𝑤 ≠ ∅ ) → ( lastS ‘ 𝑤 ) ∈ 𝑆 )
19 13 18 sylbi ( 𝑤 ∈ ( 𝑊 ∖ { ∅ } ) → ( lastS ‘ 𝑤 ) ∈ 𝑆 )
20 19 adantl ( ( 𝜑𝑤 ∈ ( 𝑊 ∖ { ∅ } ) ) → ( lastS ‘ 𝑤 ) ∈ 𝑆 )
21 12 20 jca ( ( 𝜑𝑤 ∈ ( 𝑊 ∖ { ∅ } ) ) → ( 𝑤 ∈ dom lastS ∧ ( lastS ‘ 𝑤 ) ∈ 𝑆 ) )
22 21 ralrimiva ( 𝜑 → ∀ 𝑤 ∈ ( 𝑊 ∖ { ∅ } ) ( 𝑤 ∈ dom lastS ∧ ( lastS ‘ 𝑤 ) ∈ 𝑆 ) )
23 9 10 fnmpti lastS Fn V
24 fnfun ( lastS Fn V → Fun lastS )
25 ffvresb ( Fun lastS → ( ( lastS ↾ ( 𝑊 ∖ { ∅ } ) ) : ( 𝑊 ∖ { ∅ } ) ⟶ 𝑆 ↔ ∀ 𝑤 ∈ ( 𝑊 ∖ { ∅ } ) ( 𝑤 ∈ dom lastS ∧ ( lastS ‘ 𝑤 ) ∈ 𝑆 ) ) )
26 23 24 25 mp2b ( ( lastS ↾ ( 𝑊 ∖ { ∅ } ) ) : ( 𝑊 ∖ { ∅ } ) ⟶ 𝑆 ↔ ∀ 𝑤 ∈ ( 𝑊 ∖ { ∅ } ) ( 𝑤 ∈ dom lastS ∧ ( lastS ‘ 𝑤 ) ∈ 𝑆 ) )
27 22 26 sylibr ( 𝜑 → ( lastS ↾ ( 𝑊 ∖ { ∅ } ) ) : ( 𝑊 ∖ { ∅ } ) ⟶ 𝑆 )
28 eqid ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) = ( ℤ ‘ ( ♯ ‘ 𝑀 ) )
29 lencl ( 𝑀 ∈ Word 𝑆 → ( ♯ ‘ 𝑀 ) ∈ ℕ0 )
30 29 nn0zd ( 𝑀 ∈ Word 𝑆 → ( ♯ ‘ 𝑀 ) ∈ ℤ )
31 2 30 syl ( 𝜑 → ( ♯ ‘ 𝑀 ) ∈ ℤ )
32 ovex ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) ∈ V
33 simpr ( ( 𝜑𝑎 ∈ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) → 𝑎 ∈ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) )
34 2 29 syl ( 𝜑 → ( ♯ ‘ 𝑀 ) ∈ ℕ0 )
35 34 adantr ( ( 𝜑𝑎 ∈ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) → ( ♯ ‘ 𝑀 ) ∈ ℕ0 )
36 elnn0uz ( ( ♯ ‘ 𝑀 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝑀 ) ∈ ( ℤ ‘ 0 ) )
37 35 36 sylib ( ( 𝜑𝑎 ∈ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) → ( ♯ ‘ 𝑀 ) ∈ ( ℤ ‘ 0 ) )
38 uztrn ( ( 𝑎 ∈ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ∧ ( ♯ ‘ 𝑀 ) ∈ ( ℤ ‘ 0 ) ) → 𝑎 ∈ ( ℤ ‘ 0 ) )
39 33 37 38 syl2anc ( ( 𝜑𝑎 ∈ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) → 𝑎 ∈ ( ℤ ‘ 0 ) )
40 nn0uz 0 = ( ℤ ‘ 0 )
41 39 40 eleqtrrdi ( ( 𝜑𝑎 ∈ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) → 𝑎 ∈ ℕ0 )
42 fvconst2g ( ( ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) ∈ V ∧ 𝑎 ∈ ℕ0 ) → ( ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) } ) ‘ 𝑎 ) = ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) )
43 32 41 42 sylancr ( ( 𝜑𝑎 ∈ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) → ( ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) } ) ‘ 𝑎 ) = ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) )
44 1 2 3 4 sseqmw ( 𝜑𝑀𝑊 )
45 4 44 ffvelrnd ( 𝜑 → ( 𝐹𝑀 ) ∈ 𝑆 )
46 45 s1cld ( 𝜑 → ⟨“ ( 𝐹𝑀 ) ”⟩ ∈ Word 𝑆 )
47 ccatcl ( ( 𝑀 ∈ Word 𝑆 ∧ ⟨“ ( 𝐹𝑀 ) ”⟩ ∈ Word 𝑆 ) → ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) ∈ Word 𝑆 )
48 2 46 47 syl2anc ( 𝜑 → ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) ∈ Word 𝑆 )
49 32 a1i ( 𝜑 → ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) ∈ V )
50 ccatws1len ( 𝑀 ∈ Word 𝑆 → ( ♯ ‘ ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) ) = ( ( ♯ ‘ 𝑀 ) + 1 ) )
51 2 50 syl ( 𝜑 → ( ♯ ‘ ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) ) = ( ( ♯ ‘ 𝑀 ) + 1 ) )
52 uzid ( ( ♯ ‘ 𝑀 ) ∈ ℤ → ( ♯ ‘ 𝑀 ) ∈ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) )
53 peano2uz ( ( ♯ ‘ 𝑀 ) ∈ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) → ( ( ♯ ‘ 𝑀 ) + 1 ) ∈ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) )
54 31 52 53 3syl ( 𝜑 → ( ( ♯ ‘ 𝑀 ) + 1 ) ∈ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) )
55 51 54 eqeltrd ( 𝜑 → ( ♯ ‘ ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) ) ∈ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) )
56 hashf ♯ : V ⟶ ( ℕ0 ∪ { +∞ } )
57 ffn ( ♯ : V ⟶ ( ℕ0 ∪ { +∞ } ) → ♯ Fn V )
58 elpreima ( ♯ Fn V → ( ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) ∈ ( ♯ “ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) ↔ ( ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) ∈ V ∧ ( ♯ ‘ ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) ) ∈ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) ) )
59 56 57 58 mp2b ( ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) ∈ ( ♯ “ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) ↔ ( ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) ∈ V ∧ ( ♯ ‘ ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) ) ∈ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) )
60 49 55 59 sylanbrc ( 𝜑 → ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) ∈ ( ♯ “ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) )
61 48 60 elind ( 𝜑 → ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) ∈ ( Word 𝑆 ∩ ( ♯ “ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) ) )
62 61 3 eleqtrrdi ( 𝜑 → ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) ∈ 𝑊 )
63 62 adantr ( ( 𝜑𝑎 ∈ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) → ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) ∈ 𝑊 )
64 ccatws1n0 ( 𝑀 ∈ Word 𝑆 → ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) ≠ ∅ )
65 2 64 syl ( 𝜑 → ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) ≠ ∅ )
66 65 adantr ( ( 𝜑𝑎 ∈ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) → ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) ≠ ∅ )
67 eldifsn ( ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) ∈ ( 𝑊 ∖ { ∅ } ) ↔ ( ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) ∈ 𝑊 ∧ ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) ≠ ∅ ) )
68 63 66 67 sylanbrc ( ( 𝜑𝑎 ∈ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) → ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) ∈ ( 𝑊 ∖ { ∅ } ) )
69 43 68 eqeltrd ( ( 𝜑𝑎 ∈ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) → ( ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) } ) ‘ 𝑎 ) ∈ ( 𝑊 ∖ { ∅ } ) )
70 eqidd ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) ∧ 𝑏 ∈ ( 𝑊 ∖ { ∅ } ) ) ) → ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹𝑥 ) ”⟩ ) ) = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹𝑥 ) ”⟩ ) ) )
71 simprl ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) ∧ 𝑏 ∈ ( 𝑊 ∖ { ∅ } ) ) ) ∧ ( 𝑥 = 𝑎𝑦 = 𝑏 ) ) → 𝑥 = 𝑎 )
72 71 fveq2d ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) ∧ 𝑏 ∈ ( 𝑊 ∖ { ∅ } ) ) ) ∧ ( 𝑥 = 𝑎𝑦 = 𝑏 ) ) → ( 𝐹𝑥 ) = ( 𝐹𝑎 ) )
73 72 s1eqd ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) ∧ 𝑏 ∈ ( 𝑊 ∖ { ∅ } ) ) ) ∧ ( 𝑥 = 𝑎𝑦 = 𝑏 ) ) → ⟨“ ( 𝐹𝑥 ) ”⟩ = ⟨“ ( 𝐹𝑎 ) ”⟩ )
74 71 73 oveq12d ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) ∧ 𝑏 ∈ ( 𝑊 ∖ { ∅ } ) ) ) ∧ ( 𝑥 = 𝑎𝑦 = 𝑏 ) ) → ( 𝑥 ++ ⟨“ ( 𝐹𝑥 ) ”⟩ ) = ( 𝑎 ++ ⟨“ ( 𝐹𝑎 ) ”⟩ ) )
75 vex 𝑎 ∈ V
76 75 a1i ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) ∧ 𝑏 ∈ ( 𝑊 ∖ { ∅ } ) ) ) → 𝑎 ∈ V )
77 vex 𝑏 ∈ V
78 77 a1i ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) ∧ 𝑏 ∈ ( 𝑊 ∖ { ∅ } ) ) ) → 𝑏 ∈ V )
79 ovex ( 𝑎 ++ ⟨“ ( 𝐹𝑎 ) ”⟩ ) ∈ V
80 79 a1i ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) ∧ 𝑏 ∈ ( 𝑊 ∖ { ∅ } ) ) ) → ( 𝑎 ++ ⟨“ ( 𝐹𝑎 ) ”⟩ ) ∈ V )
81 70 74 76 78 80 ovmpod ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) ∧ 𝑏 ∈ ( 𝑊 ∖ { ∅ } ) ) ) → ( 𝑎 ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹𝑥 ) ”⟩ ) ) 𝑏 ) = ( 𝑎 ++ ⟨“ ( 𝐹𝑎 ) ”⟩ ) )
82 eldifi ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) → 𝑎𝑊 )
83 82 ad2antrl ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) ∧ 𝑏 ∈ ( 𝑊 ∖ { ∅ } ) ) ) → 𝑎𝑊 )
84 15 83 sselid ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) ∧ 𝑏 ∈ ( 𝑊 ∖ { ∅ } ) ) ) → 𝑎 ∈ Word 𝑆 )
85 4 adantr ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) ∧ 𝑏 ∈ ( 𝑊 ∖ { ∅ } ) ) ) → 𝐹 : 𝑊𝑆 )
86 85 83 ffvelrnd ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) ∧ 𝑏 ∈ ( 𝑊 ∖ { ∅ } ) ) ) → ( 𝐹𝑎 ) ∈ 𝑆 )
87 86 s1cld ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) ∧ 𝑏 ∈ ( 𝑊 ∖ { ∅ } ) ) ) → ⟨“ ( 𝐹𝑎 ) ”⟩ ∈ Word 𝑆 )
88 ccatcl ( ( 𝑎 ∈ Word 𝑆 ∧ ⟨“ ( 𝐹𝑎 ) ”⟩ ∈ Word 𝑆 ) → ( 𝑎 ++ ⟨“ ( 𝐹𝑎 ) ”⟩ ) ∈ Word 𝑆 )
89 84 87 88 syl2anc ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) ∧ 𝑏 ∈ ( 𝑊 ∖ { ∅ } ) ) ) → ( 𝑎 ++ ⟨“ ( 𝐹𝑎 ) ”⟩ ) ∈ Word 𝑆 )
90 15 82 sselid ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) → 𝑎 ∈ Word 𝑆 )
91 90 ad2antrl ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) ∧ 𝑏 ∈ ( 𝑊 ∖ { ∅ } ) ) ) → 𝑎 ∈ Word 𝑆 )
92 ccatws1len ( 𝑎 ∈ Word 𝑆 → ( ♯ ‘ ( 𝑎 ++ ⟨“ ( 𝐹𝑎 ) ”⟩ ) ) = ( ( ♯ ‘ 𝑎 ) + 1 ) )
93 91 92 syl ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) ∧ 𝑏 ∈ ( 𝑊 ∖ { ∅ } ) ) ) → ( ♯ ‘ ( 𝑎 ++ ⟨“ ( 𝐹𝑎 ) ”⟩ ) ) = ( ( ♯ ‘ 𝑎 ) + 1 ) )
94 83 3 eleqtrdi ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) ∧ 𝑏 ∈ ( 𝑊 ∖ { ∅ } ) ) ) → 𝑎 ∈ ( Word 𝑆 ∩ ( ♯ “ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) ) )
95 94 elin2d ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) ∧ 𝑏 ∈ ( 𝑊 ∖ { ∅ } ) ) ) → 𝑎 ∈ ( ♯ “ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) )
96 elpreima ( ♯ Fn V → ( 𝑎 ∈ ( ♯ “ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) ↔ ( 𝑎 ∈ V ∧ ( ♯ ‘ 𝑎 ) ∈ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) ) )
97 56 57 96 mp2b ( 𝑎 ∈ ( ♯ “ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) ↔ ( 𝑎 ∈ V ∧ ( ♯ ‘ 𝑎 ) ∈ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) )
98 95 97 sylib ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) ∧ 𝑏 ∈ ( 𝑊 ∖ { ∅ } ) ) ) → ( 𝑎 ∈ V ∧ ( ♯ ‘ 𝑎 ) ∈ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) )
99 peano2uz ( ( ♯ ‘ 𝑎 ) ∈ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) → ( ( ♯ ‘ 𝑎 ) + 1 ) ∈ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) )
100 98 99 simpl2im ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) ∧ 𝑏 ∈ ( 𝑊 ∖ { ∅ } ) ) ) → ( ( ♯ ‘ 𝑎 ) + 1 ) ∈ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) )
101 93 100 eqeltrd ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) ∧ 𝑏 ∈ ( 𝑊 ∖ { ∅ } ) ) ) → ( ♯ ‘ ( 𝑎 ++ ⟨“ ( 𝐹𝑎 ) ”⟩ ) ) ∈ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) )
102 elpreima ( ♯ Fn V → ( ( 𝑎 ++ ⟨“ ( 𝐹𝑎 ) ”⟩ ) ∈ ( ♯ “ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) ↔ ( ( 𝑎 ++ ⟨“ ( 𝐹𝑎 ) ”⟩ ) ∈ V ∧ ( ♯ ‘ ( 𝑎 ++ ⟨“ ( 𝐹𝑎 ) ”⟩ ) ) ∈ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) ) )
103 56 57 102 mp2b ( ( 𝑎 ++ ⟨“ ( 𝐹𝑎 ) ”⟩ ) ∈ ( ♯ “ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) ↔ ( ( 𝑎 ++ ⟨“ ( 𝐹𝑎 ) ”⟩ ) ∈ V ∧ ( ♯ ‘ ( 𝑎 ++ ⟨“ ( 𝐹𝑎 ) ”⟩ ) ) ∈ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) )
104 80 101 103 sylanbrc ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) ∧ 𝑏 ∈ ( 𝑊 ∖ { ∅ } ) ) ) → ( 𝑎 ++ ⟨“ ( 𝐹𝑎 ) ”⟩ ) ∈ ( ♯ “ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) )
105 89 104 elind ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) ∧ 𝑏 ∈ ( 𝑊 ∖ { ∅ } ) ) ) → ( 𝑎 ++ ⟨“ ( 𝐹𝑎 ) ”⟩ ) ∈ ( Word 𝑆 ∩ ( ♯ “ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) ) )
106 105 3 eleqtrrdi ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) ∧ 𝑏 ∈ ( 𝑊 ∖ { ∅ } ) ) ) → ( 𝑎 ++ ⟨“ ( 𝐹𝑎 ) ”⟩ ) ∈ 𝑊 )
107 ccatws1n0 ( 𝑎 ∈ Word 𝑆 → ( 𝑎 ++ ⟨“ ( 𝐹𝑎 ) ”⟩ ) ≠ ∅ )
108 91 107 syl ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) ∧ 𝑏 ∈ ( 𝑊 ∖ { ∅ } ) ) ) → ( 𝑎 ++ ⟨“ ( 𝐹𝑎 ) ”⟩ ) ≠ ∅ )
109 eldifsn ( ( 𝑎 ++ ⟨“ ( 𝐹𝑎 ) ”⟩ ) ∈ ( 𝑊 ∖ { ∅ } ) ↔ ( ( 𝑎 ++ ⟨“ ( 𝐹𝑎 ) ”⟩ ) ∈ 𝑊 ∧ ( 𝑎 ++ ⟨“ ( 𝐹𝑎 ) ”⟩ ) ≠ ∅ ) )
110 106 108 109 sylanbrc ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) ∧ 𝑏 ∈ ( 𝑊 ∖ { ∅ } ) ) ) → ( 𝑎 ++ ⟨“ ( 𝐹𝑎 ) ”⟩ ) ∈ ( 𝑊 ∖ { ∅ } ) )
111 81 110 eqeltrd ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) ∧ 𝑏 ∈ ( 𝑊 ∖ { ∅ } ) ) ) → ( 𝑎 ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹𝑥 ) ”⟩ ) ) 𝑏 ) ∈ ( 𝑊 ∖ { ∅ } ) )
112 28 31 69 111 seqf ( 𝜑 → seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) } ) ) : ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ⟶ ( 𝑊 ∖ { ∅ } ) )
113 fco2 ( ( ( lastS ↾ ( 𝑊 ∖ { ∅ } ) ) : ( 𝑊 ∖ { ∅ } ) ⟶ 𝑆 ∧ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) } ) ) : ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ⟶ ( 𝑊 ∖ { ∅ } ) ) → ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) } ) ) ) : ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ⟶ 𝑆 )
114 27 112 113 syl2anc ( 𝜑 → ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) } ) ) ) : ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ⟶ 𝑆 )
115 fzouzdisj ( ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ∩ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) = ∅
116 115 a1i ( 𝜑 → ( ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ∩ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) = ∅ )
117 fun ( ( ( 𝑀 : ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ⟶ 𝑆 ∧ ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) } ) ) ) : ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ⟶ 𝑆 ) ∧ ( ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ∩ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) = ∅ ) → ( 𝑀 ∪ ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) } ) ) ) ) : ( ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ∪ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) ⟶ ( 𝑆𝑆 ) )
118 6 114 116 117 syl21anc ( 𝜑 → ( 𝑀 ∪ ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) } ) ) ) ) : ( ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ∪ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) ⟶ ( 𝑆𝑆 ) )
119 1 2 3 4 sseqval ( 𝜑 → ( 𝑀 seqstr 𝐹 ) = ( 𝑀 ∪ ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) } ) ) ) ) )
120 fzouzsplit ( ( ♯ ‘ 𝑀 ) ∈ ( ℤ ‘ 0 ) → ( ℤ ‘ 0 ) = ( ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ∪ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) )
121 36 120 sylbi ( ( ♯ ‘ 𝑀 ) ∈ ℕ0 → ( ℤ ‘ 0 ) = ( ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ∪ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) )
122 2 29 121 3syl ( 𝜑 → ( ℤ ‘ 0 ) = ( ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ∪ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) )
123 40 122 syl5eq ( 𝜑 → ℕ0 = ( ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ∪ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) )
124 unidm ( 𝑆𝑆 ) = 𝑆
125 124 a1i ( 𝜑 → ( 𝑆𝑆 ) = 𝑆 )
126 125 eqcomd ( 𝜑𝑆 = ( 𝑆𝑆 ) )
127 119 123 126 feq123d ( 𝜑 → ( ( 𝑀 seqstr 𝐹 ) : ℕ0𝑆 ↔ ( 𝑀 ∪ ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹𝑀 ) ”⟩ ) } ) ) ) ) : ( ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ∪ ( ℤ ‘ ( ♯ ‘ 𝑀 ) ) ) ⟶ ( 𝑆𝑆 ) ) )
128 118 127 mpbird ( 𝜑 → ( 𝑀 seqstr 𝐹 ) : ℕ0𝑆 )