Metamath Proof Explorer

Theorem sseqfv1

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

Ref Expression
Hypotheses sseqval.1 ⊢φ→S∈V
sseqval.2 ⊢φ→M∈WordS
sseqval.3 ⊢W=WordS∩.-1ℤ≥M
sseqval.4 ⊢φ→F:W⟶S
sseqfv1.4 ⊢φ→N∈0..^M
Assertion sseqfv1 ⊢φ→MseqstrF⁡N=M⁡N

Proof

Step Hyp Ref Expression
1 sseqval.1 ⊢φ→S∈V
2 sseqval.2 ⊢φ→M∈WordS
3 sseqval.3 ⊢W=WordS∩.-1ℤ≥M
4 sseqval.4 ⊢φ→F:W⟶S
5 sseqfv1.4 ⊢φ→N∈0..^M
6 1 2 3 4 sseqval ⊢φ→MseqstrF=M∪lastS∘seqMx∈V,y∈V⟼x++⟨“F⁡x”⟩ℕ0×M++⟨“F⁡M”⟩
7 6 fveq1d ⊢φ→MseqstrF⁡N=M∪lastS∘seqMx∈V,y∈V⟼x++⟨“F⁡x”⟩ℕ0×M++⟨“F⁡M”⟩⁡N
8 wrdfn ⊢M∈WordS→MFn0..^M
9 2 8 syl ⊢φ→MFn0..^M
10 fvex ⊢x⁡x−1∈V
11 df-lsw ⊢lastS=x∈V⟼x⁡x−1
12 10 11 fnmpti ⊢lastSFnV
13 12 a1i ⊢φ→lastSFnV
14 lencl ⊢M∈WordS→M∈ℕ0
15 2 14 syl ⊢φ→M∈ℕ0
16 15 nn0zd ⊢φ→M∈ℤ
17 seqfn ⊢M∈ℤ→seqMx∈V,y∈V⟼x++⟨“F⁡x”⟩ℕ0×M++⟨“F⁡M”⟩Fnℤ≥M
18 16 17 syl ⊢φ→seqMx∈V,y∈V⟼x++⟨“F⁡x”⟩ℕ0×M++⟨“F⁡M”⟩Fnℤ≥M
19 ssv ⊢ran⁡seqMx∈V,y∈V⟼x++⟨“F⁡x”⟩ℕ0×M++⟨“F⁡M”⟩⊆V
20 19 a1i ⊢φ→ran⁡seqMx∈V,y∈V⟼x++⟨“F⁡x”⟩ℕ0×M++⟨“F⁡M”⟩⊆V
21 fnco ⊢lastSFnV∧seqMx∈V,y∈V⟼x++⟨“F⁡x”⟩ℕ0×M++⟨“F⁡M”⟩Fnℤ≥M∧ran⁡seqMx∈V,y∈V⟼x++⟨“F⁡x”⟩ℕ0×M++⟨“F⁡M”⟩⊆V→lastS∘seqMx∈V,y∈V⟼x++⟨“F⁡x”⟩ℕ0×M++⟨“F⁡M”⟩Fnℤ≥M
22 13 18 20 21 syl3anc ⊢φ→lastS∘seqMx∈V,y∈V⟼x++⟨“F⁡x”⟩ℕ0×M++⟨“F⁡M”⟩Fnℤ≥M
23 fzouzdisj ⊢0..^M∩ℤ≥M=∅
24 23 a1i ⊢φ→0..^M∩ℤ≥M=∅
25 fvun1 ⊢MFn0..^M∧lastS∘seqMx∈V,y∈V⟼x++⟨“F⁡x”⟩ℕ0×M++⟨“F⁡M”⟩Fnℤ≥M∧0..^M∩ℤ≥M=∅∧N∈0..^M→M∪lastS∘seqMx∈V,y∈V⟼x++⟨“F⁡x”⟩ℕ0×M++⟨“F⁡M”⟩⁡N=M⁡N
26 9 22 24 5 25 syl112anc ⊢φ→M∪lastS∘seqMx∈V,y∈V⟼x++⟨“F⁡x”⟩ℕ0×M++⟨“F⁡M”⟩⁡N=M⁡N
27 7 26 eqtrd ⊢φ→MseqstrF⁡N=M⁡N