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 ⊢ φ → S ∈ V
sseqval.2 ⊢ φ → M ∈ Word S
sseqval.3 ⊢ W = Word S ∩ . -1 ℤ ≥ M
sseqval.4 ⊢ φ → F : W ⟶ S
sseqfv2.4 ⊢ φ → N ∈ ℤ ≥ M
Assertion sseqfv2 ⊢ φ → M seq str F ⁡ N = lastS ⁡ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ N

Proof

Step Hyp Ref Expression
1 sseqval.1 ⊢ φ → S ∈ V
2 sseqval.2 ⊢ φ → M ∈ Word S
3 sseqval.3 ⊢ W = Word S ∩ . -1 ℤ ≥ M
4 sseqval.4 ⊢ φ → F : W ⟶ S
5 sseqfv2.4 ⊢ φ → N ∈ ℤ ≥ M
6 1 2 3 4 sseqval ⊢ φ → M seq str F = M ∪ lastS ∘ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩
7 6 fveq1d ⊢ φ → M seq str F ⁡ N = M ∪ lastS ∘ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ N
8 wrdfn ⊢ M ∈ Word S → M Fn 0 ..^ M
9 2 8 syl ⊢ φ → M Fn 0 ..^ M
10 fvex ⊢ x ⁡ x − 1 ∈ V
11 df-lsw ⊢ lastS = x ∈ V ⟼ x ⁡ x − 1
12 10 11 fnmpti ⊢ lastS Fn V
13 12 a1i ⊢ φ → lastS Fn V
14 lencl ⊢ M ∈ Word S → M ∈ ℕ 0
15 2 14 syl ⊢ φ → M ∈ ℕ 0
16 15 nn0zd ⊢ φ → M ∈ ℤ
17 seqfn ⊢ M ∈ ℤ → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ Fn ℤ ≥ M
18 16 17 syl ⊢ φ → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ Fn ℤ ≥ M
19 ssv ⊢ ran ⁡ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⊆ V
20 19 a1i ⊢ φ → ran ⁡ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⊆ V
21 fnco ⊢ lastS Fn V ∧ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ Fn ℤ ≥ M ∧ ran ⁡ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⊆ V → lastS ∘ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ Fn ℤ ≥ M
22 13 18 20 21 syl3anc ⊢ φ → lastS ∘ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ Fn ℤ ≥ M
23 fzouzdisj ⊢ 0 ..^ M ∩ ℤ ≥ M = ∅
24 23 a1i ⊢ φ → 0 ..^ M ∩ ℤ ≥ M = ∅
25 fvun2 ⊢ M Fn 0 ..^ M ∧ lastS ∘ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ Fn ℤ ≥ M ∧ 0 ..^ M ∩ ℤ ≥ M = ∅ ∧ N ∈ ℤ ≥ M → M ∪ lastS ∘ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ N = lastS ∘ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ N
26 9 22 24 5 25 syl112anc ⊢ φ → M ∪ lastS ∘ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ N = lastS ∘ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ N
27 fnfun ⊢ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ Fn ℤ ≥ M → Fun ⁡ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩
28 18 27 syl ⊢ φ → Fun ⁡ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩
29 fvexd ⊢ φ → ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ M ∈ V
30 ovexd ⊢ φ ∧ a ∈ V ∧ b ∈ V → a x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ b ∈ V
31 eqid ⊢ ℤ ≥ M = ℤ ≥ M
32 fvexd ⊢ φ ∧ a ∈ ℤ ≥ M + 1 → ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ a ∈ V
33 29 30 31 16 32 seqf2 ⊢ φ → seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ : ℤ ≥ M ⟶ V
34 33 fdmd ⊢ φ → dom ⁡ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ = ℤ ≥ M
35 5 34 eleqtrrd ⊢ φ → N ∈ dom ⁡ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩
36 fvco ⊢ Fun ⁡ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ∧ N ∈ dom ⁡ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ → lastS ∘ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ N = lastS ⁡ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ N
37 28 35 36 syl2anc ⊢ φ → lastS ∘ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ N = lastS ⁡ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ N
38 7 26 37 3eqtrd ⊢ φ → M seq str F ⁡ N = lastS ⁡ seq M x ∈ V , y ∈ V ⟼ x ++ ⟨“ F ⁡ x ”⟩ ℕ 0 × M ++ ⟨“ F ⁡ M ”⟩ ⁡ N