Metamath Proof Explorer

Theorem sseqfv2

Description: Value of the strong sequence builder function. (Contributed by Thierry Arnoux, 21-Apr-2019)

Ref Expression
Hypotheses sseqval.1 ⊢ ( 𝜑 → 𝑆 ∈ V )
sseqval.2 ⊢ ( 𝜑 → 𝑀 ∈ Word 𝑆 )
sseqval.3 ⊢ 𝑊 = ( Word 𝑆 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ) )
sseqval.4 ⊢ ( 𝜑 → 𝐹 : 𝑊 ⟶ 𝑆 )
sseqfv2.4 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) )
Assertion sseqfv2 ( 𝜑 → ( ( 𝑀 seqstr 𝐹 ) ‘ 𝑁 ) = ( lastS ‘ ( seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 sseqval.1 ⊢ ( 𝜑 → 𝑆 ∈ V )
2 sseqval.2 ⊢ ( 𝜑 → 𝑀 ∈ Word 𝑆 )
3 sseqval.3 ⊢ 𝑊 = ( Word 𝑆 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ) )
4 sseqval.4 ⊢ ( 𝜑 → 𝐹 : 𝑊 ⟶ 𝑆 )
5 sseqfv2.4 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) )
6 1 2 3 4 sseqval ⊢ ( 𝜑 → ( 𝑀 seqstr 𝐹 ) = ( 𝑀 ∪ ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) ) )
7 6 fveq1d ⊢ ( 𝜑 → ( ( 𝑀 seqstr 𝐹 ) ‘ 𝑁 ) = ( ( 𝑀 ∪ ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) ) ‘ 𝑁 ) )
8 wrdfn ⊢ ( 𝑀 ∈ Word 𝑆 → 𝑀 Fn ( 0 ..^ ( ♯ ‘ 𝑀 ) ) )
9 2 8 syl ⊢ ( 𝜑 → 𝑀 Fn ( 0 ..^ ( ♯ ‘ 𝑀 ) ) )
10 fvex ⊢ ( 𝑥 ‘ ( ( ♯ ‘ 𝑥 ) − 1 ) ) ∈ V
11 df-lsw ⊢ lastS = ( 𝑥 ∈ V ↦ ( 𝑥 ‘ ( ( ♯ ‘ 𝑥 ) − 1 ) ) )
12 10 11 fnmpti ⊢ lastS Fn V
13 12 a1i ⊢ ( 𝜑 → lastS Fn V )
14 lencl ⊢ ( 𝑀 ∈ Word 𝑆 → ( ♯ ‘ 𝑀 ) ∈ ℕ0 )
15 2 14 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑀 ) ∈ ℕ0 )
16 15 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ 𝑀 ) ∈ ℤ )
17 seqfn ⊢ ( ( ♯ ‘ 𝑀 ) ∈ ℤ → seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) Fn ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) )
18 16 17 syl ⊢ ( 𝜑 → seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) Fn ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) )
19 ssv ⊢ ran seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ⊆ V
20 19 a1i ⊢ ( 𝜑 → ran seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ⊆ V )
21 fnco ⊢ ( ( lastS Fn V ∧ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) Fn ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ∧ ran seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ⊆ V ) → ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) Fn ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) )
22 13 18 20 21 syl3anc ⊢ ( 𝜑 → ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) Fn ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) )
23 fzouzdisj ⊢ ( ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ∩ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ) = ∅
24 23 a1i ⊢ ( 𝜑 → ( ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ∩ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ) = ∅ )
25 fvun2 ⊢ ( ( 𝑀 Fn ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ∧ ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) Fn ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ∧ ( ( ( 0 ..^ ( ♯ ‘ 𝑀 ) ) ∩ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ) = ∅ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ) ) → ( ( 𝑀 ∪ ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) ) ‘ 𝑁 ) = ( ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) ‘ 𝑁 ) )
26 9 22 24 5 25 syl112anc ⊢ ( 𝜑 → ( ( 𝑀 ∪ ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) ) ‘ 𝑁 ) = ( ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) ‘ 𝑁 ) )
27 fnfun ⊢ ( seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) Fn ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) → Fun seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) )
28 18 27 syl ⊢ ( 𝜑 → Fun seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) )
29 fvexd ⊢ ( 𝜑 → ( ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ‘ ( ♯ ‘ 𝑀 ) ) ∈ V )
30 ovexd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ V ∧ 𝑏 ∈ V ) ) → ( 𝑎 ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) 𝑏 ) ∈ V )
31 eqid ⊢ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) = ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) )
32 fvexd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝑀 ) + 1 ) ) ) → ( ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ‘ 𝑎 ) ∈ V )
33 29 30 31 16 32 seqf2 ⊢ ( 𝜑 → seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) : ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ⟶ V )
34 33 fdmd ⊢ ( 𝜑 → dom seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) = ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) )
35 5 34 eleqtrrd ⊢ ( 𝜑 → 𝑁 ∈ dom seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) )
36 fvco ⊢ ( ( Fun seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ∧ 𝑁 ∈ dom seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) → ( ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) ‘ 𝑁 ) = ( lastS ‘ ( seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ‘ 𝑁 ) ) )
37 28 35 36 syl2anc ⊢ ( 𝜑 → ( ( lastS ∘ seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ) ‘ 𝑁 ) = ( lastS ‘ ( seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ‘ 𝑁 ) ) )
38 7 26 37 3eqtrd ⊢ ( 𝜑 → ( ( 𝑀 seqstr 𝐹 ) ‘ 𝑁 ) = ( lastS ‘ ( seq ( ♯ ‘ 𝑀 ) ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ++ ⟨“ ( 𝐹 ‘ 𝑥 ) ”⟩ ) ) , ( ℕ0 × { ( 𝑀 ++ ⟨“ ( 𝐹 ‘ 𝑀 ) ”⟩ ) } ) ) ‘ 𝑁 ) ) )