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 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ∈ 𝑆 )
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 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑊 ∖ { ∅ } ) ∧ 𝑏 ∈ ( 𝑊 ∖ { ∅ } ) ) ) → ( 𝐹 ‘ 𝑎 ) ∈ 𝑆 )
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 eqtrid ⊢ ( 𝜑 → ℕ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 ⟶ 𝑆 )