sseqp1 - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > sseqp1		Structured version Visualization version GIF version

Theorem sseqp1 30457

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

**Hypotheses**
Ref	Expression
sseqval.1	⊢ (𝜑 → 𝑆 ∈ V)
sseqval.2	⊢ (𝜑 → 𝑀 ∈ Word 𝑆)
sseqval.3	⊢ 𝑊 = (Word 𝑆 ∩ (^◡# “ (ℤ_≥‘(#‘𝑀))))
sseqval.4	⊢ (𝜑 → 𝐹:𝑊⟶𝑆)
sseqfv2.4	⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(#‘𝑀)))

**Assertion**
Ref	Expression
sseqp1	⊢ (𝜑 → ((𝑀seq_str𝐹)‘𝑁) = (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑁))))

Proof of Theorem sseqp1 Dummy variables 𝑥 𝑦 𝑎 𝑏 𝑖 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sseqval.1	. . 3 ⊢ (𝜑 → 𝑆 ∈ V)
2		sseqval.2	. . 3 ⊢ (𝜑 → 𝑀 ∈ Word 𝑆)
3		sseqval.3	. . 3 ⊢ 𝑊 = (Word 𝑆 ∩ (^◡# “ (ℤ_≥‘(#‘𝑀))))
4		sseqval.4	. . 3 ⊢ (𝜑 → 𝐹:𝑊⟶𝑆)
5		sseqfv2.4	. . 3 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(#‘𝑀)))
6	1, 2, 3, 4, 5	sseqfv2 30456	. 2 ⊢ (𝜑 → ((𝑀seq_str𝐹)‘𝑁) = ( lastS ‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑁)))
7		fveq2 6191	. . . . . . 7 ⊢ (𝑖 = (#‘𝑀) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑖) = (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘(#‘𝑀)))
8		oveq2 6658	. . . . . . . . 9 ⊢ (𝑖 = (#‘𝑀) → (0..^𝑖) = (0..^(#‘𝑀)))
9	8	reseq2d 5396	. . . . . . . 8 ⊢ (𝑖 = (#‘𝑀) → ((𝑀seq_str𝐹) ↾ (0..^𝑖)) = ((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀))))
10	9	fveq2d 6195	. . . . . . . . 9 ⊢ (𝑖 = (#‘𝑀) → (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖))) = (𝐹‘((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀)))))
11	10	s1eqd 13381	. . . . . . . 8 ⊢ (𝑖 = (#‘𝑀) → ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩ = ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀))))”⟩)
12	9, 11	oveq12d 6668	. . . . . . 7 ⊢ (𝑖 = (#‘𝑀) → (((𝑀seq_str𝐹) ↾ (0..^𝑖)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩) = (((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀))) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀))))”⟩))
13	7, 12	eqeq12d 2637	. . . . . 6 ⊢ (𝑖 = (#‘𝑀) → ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑖) = (((𝑀seq_str𝐹) ↾ (0..^𝑖)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩) ↔ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘(#‘𝑀)) = (((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀))) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀))))”⟩)))
14	13	imbi2d 330	. . . . 5 ⊢ (𝑖 = (#‘𝑀) → ((𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑖) = (((𝑀seq_str𝐹) ↾ (0..^𝑖)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩)) ↔ (𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘(#‘𝑀)) = (((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀))) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀))))”⟩))))
15		fveq2 6191	. . . . . . 7 ⊢ (𝑖 = 𝑛 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑖) = (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛))
16		oveq2 6658	. . . . . . . . 9 ⊢ (𝑖 = 𝑛 → (0..^𝑖) = (0..^𝑛))
17	16	reseq2d 5396	. . . . . . . 8 ⊢ (𝑖 = 𝑛 → ((𝑀seq_str𝐹) ↾ (0..^𝑖)) = ((𝑀seq_str𝐹) ↾ (0..^𝑛)))
18	17	fveq2d 6195	. . . . . . . . 9 ⊢ (𝑖 = 𝑛 → (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖))) = (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛))))
19	18	s1eqd 13381	. . . . . . . 8 ⊢ (𝑖 = 𝑛 → ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩ = ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)
20	17, 19	oveq12d 6668	. . . . . . 7 ⊢ (𝑖 = 𝑛 → (((𝑀seq_str𝐹) ↾ (0..^𝑖)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩))
21	15, 20	eqeq12d 2637	. . . . . 6 ⊢ (𝑖 = 𝑛 → ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑖) = (((𝑀seq_str𝐹) ↾ (0..^𝑖)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩) ↔ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)))
22	21	imbi2d 330	. . . . 5 ⊢ (𝑖 = 𝑛 → ((𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑖) = (((𝑀seq_str𝐹) ↾ (0..^𝑖)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩)) ↔ (𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩))))
23		fveq2 6191	. . . . . . 7 ⊢ (𝑖 = (𝑛 + 1) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑖) = (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘(𝑛 + 1)))
24		oveq2 6658	. . . . . . . . 9 ⊢ (𝑖 = (𝑛 + 1) → (0..^𝑖) = (0..^(𝑛 + 1)))
25	24	reseq2d 5396	. . . . . . . 8 ⊢ (𝑖 = (𝑛 + 1) → ((𝑀seq_str𝐹) ↾ (0..^𝑖)) = ((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))))
26	25	fveq2d 6195	. . . . . . . . 9 ⊢ (𝑖 = (𝑛 + 1) → (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖))) = (𝐹‘((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1)))))
27	26	s1eqd 13381	. . . . . . . 8 ⊢ (𝑖 = (𝑛 + 1) → ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩ = ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))))”⟩)
28	25, 27	oveq12d 6668	. . . . . . 7 ⊢ (𝑖 = (𝑛 + 1) → (((𝑀seq_str𝐹) ↾ (0..^𝑖)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩) = (((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))))”⟩))
29	23, 28	eqeq12d 2637	. . . . . 6 ⊢ (𝑖 = (𝑛 + 1) → ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑖) = (((𝑀seq_str𝐹) ↾ (0..^𝑖)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩) ↔ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘(𝑛 + 1)) = (((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))))”⟩)))
30	29	imbi2d 330	. . . . 5 ⊢ (𝑖 = (𝑛 + 1) → ((𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑖) = (((𝑀seq_str𝐹) ↾ (0..^𝑖)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩)) ↔ (𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘(𝑛 + 1)) = (((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))))”⟩))))
31		fveq2 6191	. . . . . . 7 ⊢ (𝑖 = 𝑁 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑖) = (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑁))
32		oveq2 6658	. . . . . . . . 9 ⊢ (𝑖 = 𝑁 → (0..^𝑖) = (0..^𝑁))
33	32	reseq2d 5396	. . . . . . . 8 ⊢ (𝑖 = 𝑁 → ((𝑀seq_str𝐹) ↾ (0..^𝑖)) = ((𝑀seq_str𝐹) ↾ (0..^𝑁)))
34	33	fveq2d 6195	. . . . . . . . 9 ⊢ (𝑖 = 𝑁 → (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖))) = (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑁))))
35	34	s1eqd 13381	. . . . . . . 8 ⊢ (𝑖 = 𝑁 → ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩ = ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑁)))”⟩)
36	33, 35	oveq12d 6668	. . . . . . 7 ⊢ (𝑖 = 𝑁 → (((𝑀seq_str𝐹) ↾ (0..^𝑖)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩) = (((𝑀seq_str𝐹) ↾ (0..^𝑁)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑁)))”⟩))
37	31, 36	eqeq12d 2637	. . . . . 6 ⊢ (𝑖 = 𝑁 → ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑖) = (((𝑀seq_str𝐹) ↾ (0..^𝑖)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩) ↔ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑁) = (((𝑀seq_str𝐹) ↾ (0..^𝑁)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑁)))”⟩)))
38	37	imbi2d 330	. . . . 5 ⊢ (𝑖 = 𝑁 → ((𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑖) = (((𝑀seq_str𝐹) ↾ (0..^𝑖)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩)) ↔ (𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑁) = (((𝑀seq_str𝐹) ↾ (0..^𝑁)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑁)))”⟩))))
39		ovex 6678	. . . . . . . 8 ⊢ (𝑀 ++ ⟨“(𝐹‘𝑀)”⟩) ∈ V
40		lencl 13324	. . . . . . . . 9 ⊢ (𝑀 ∈ Word 𝑆 → (#‘𝑀) ∈ ℕ₀)
41	2, 40	syl 17	. . . . . . . 8 ⊢ (𝜑 → (#‘𝑀) ∈ ℕ₀)
42		fvconst2g 6467	. . . . . . . 8 ⊢ (((𝑀 ++ ⟨“(𝐹‘𝑀)”⟩) ∈ V ∧ (#‘𝑀) ∈ ℕ₀) → ((ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)})‘(#‘𝑀)) = (𝑀 ++ ⟨“(𝐹‘𝑀)”⟩))
43	39, 41, 42	sylancr 695	. . . . . . 7 ⊢ (𝜑 → ((ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)})‘(#‘𝑀)) = (𝑀 ++ ⟨“(𝐹‘𝑀)”⟩))
44	40	nn0zd 11480	. . . . . . . 8 ⊢ (𝑀 ∈ Word 𝑆 → (#‘𝑀) ∈ ℤ)
45		seq1 12814	. . . . . . . 8 ⊢ ((#‘𝑀) ∈ ℤ → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘(#‘𝑀)) = ((ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)})‘(#‘𝑀)))
46	2, 44, 45	3syl 18	. . . . . . 7 ⊢ (𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘(#‘𝑀)) = ((ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)})‘(#‘𝑀)))
47	1, 2, 3, 4	sseqfres 30455	. . . . . . . 8 ⊢ (𝜑 → ((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀))) = 𝑀)
48	47	fveq2d 6195	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀)))) = (𝐹‘𝑀))
49	48	s1eqd 13381	. . . . . . . 8 ⊢ (𝜑 → ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀))))”⟩ = ⟨“(𝐹‘𝑀)”⟩)
50	47, 49	oveq12d 6668	. . . . . . 7 ⊢ (𝜑 → (((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀))) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀))))”⟩) = (𝑀 ++ ⟨“(𝐹‘𝑀)”⟩))
51	43, 46, 50	3eqtr4d 2666	. . . . . 6 ⊢ (𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘(#‘𝑀)) = (((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀))) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀))))”⟩))
52	51	a1i 11	. . . . 5 ⊢ ((#‘𝑀) ∈ ℤ → (𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘(#‘𝑀)) = (((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀))) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀))))”⟩)))
53		seqp1 12816	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (ℤ_≥‘(#‘𝑀)) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘(𝑛 + 1)) = ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛)(𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩))((ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)})‘(𝑛 + 1))))
54	53	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘(𝑛 + 1)) = ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛)(𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩))((ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)})‘(𝑛 + 1))))
55		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑎 → 𝑥 = 𝑎)
56		fveq2 6191	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑎 → (𝐹‘𝑥) = (𝐹‘𝑎))
57	56	s1eqd 13381	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑎 → ⟨“(𝐹‘𝑥)”⟩ = ⟨“(𝐹‘𝑎)”⟩)
58	55, 57	oveq12d 6668	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑎 → (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩) = (𝑎 ++ ⟨“(𝐹‘𝑎)”⟩))
59		eqidd 2623	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑏 → (𝑎 ++ ⟨“(𝐹‘𝑎)”⟩) = (𝑎 ++ ⟨“(𝐹‘𝑎)”⟩))
60	58, 59	cbvmpt2v 6735	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)) = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ++ ⟨“(𝐹‘𝑎)”⟩))
61	60	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)) = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ++ ⟨“(𝐹‘𝑎)”⟩)))
62		simprl 794	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (𝑎 = (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) ∧ 𝑏 = ((ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)})‘(𝑛 + 1)))) → 𝑎 = (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛))
63	62	fveq2d 6195	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (𝑎 = (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) ∧ 𝑏 = ((ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)})‘(𝑛 + 1)))) → (𝐹‘𝑎) = (𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛)))
64	63	s1eqd 13381	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (𝑎 = (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) ∧ 𝑏 = ((ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)})‘(𝑛 + 1)))) → ⟨“(𝐹‘𝑎)”⟩ = ⟨“(𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛))”⟩)
65	62, 64	oveq12d 6668	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (𝑎 = (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) ∧ 𝑏 = ((ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)})‘(𝑛 + 1)))) → (𝑎 ++ ⟨“(𝐹‘𝑎)”⟩) = ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) ++ ⟨“(𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛))”⟩))
66		fvexd 6203	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) ∈ V)
67		fvexd 6203	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → ((ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)})‘(𝑛 + 1)) ∈ V)
68		ovex 6678	. . . . . . . . . . . . 13 ⊢ ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) ++ ⟨“(𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛))”⟩) ∈ V
69	68	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) ++ ⟨“(𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛))”⟩) ∈ V)
70	61, 65, 66, 67, 69	ovmpt2d 6788	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛)(𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩))((ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)})‘(𝑛 + 1))) = ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) ++ ⟨“(𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛))”⟩))
71	54, 70	eqtrd 2656	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘(𝑛 + 1)) = ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) ++ ⟨“(𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛))”⟩))
72	71	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘(𝑛 + 1)) = ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) ++ ⟨“(𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛))”⟩))
73	1	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → 𝑆 ∈ V)
74	2	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → 𝑀 ∈ Word 𝑆)
75	4	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → 𝐹:𝑊⟶𝑆)
76		simpr 477	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → 𝑛 ∈ (ℤ_≥‘(#‘𝑀)))
77	73, 74, 3, 75, 76	sseqfv2 30456	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → ((𝑀seq_str𝐹)‘𝑛) = ( lastS ‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛)))
78	77	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)) → ((𝑀seq_str𝐹)‘𝑛) = ( lastS ‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛)))
79		simpr 477	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩))
80	79	fveq2d 6195	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)) → ( lastS ‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛)) = ( lastS ‘(((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)))
81	1, 2, 3, 4	sseqf 30454	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑀seq_str𝐹):ℕ₀⟶𝑆)
82		fzo0ssnn0 12548	. . . . . . . . . . . . . . . . . . 19 ⊢ (0..^𝑛) ⊆ ℕ₀
83		fssres 6070	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀seq_str𝐹):ℕ₀⟶𝑆 ∧ (0..^𝑛) ⊆ ℕ₀) → ((𝑀seq_str𝐹) ↾ (0..^𝑛)):(0..^𝑛)⟶𝑆)
84	81, 82, 83	sylancl 694	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑀seq_str𝐹) ↾ (0..^𝑛)):(0..^𝑛)⟶𝑆)
85		iswrdi 13309	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀seq_str𝐹) ↾ (0..^𝑛)):(0..^𝑛)⟶𝑆 → ((𝑀seq_str𝐹) ↾ (0..^𝑛)) ∈ Word 𝑆)
86	84, 85	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑀seq_str𝐹) ↾ (0..^𝑛)) ∈ Word 𝑆)
87	86	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → ((𝑀seq_str𝐹) ↾ (0..^𝑛)) ∈ Word 𝑆)
88		elex 3212	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ∈ Word 𝑆 → ((𝑀seq_str𝐹) ↾ (0..^𝑛)) ∈ V)
89	87, 88	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → ((𝑀seq_str𝐹) ↾ (0..^𝑛)) ∈ V)
90	81	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → (𝑀seq_str𝐹):ℕ₀⟶𝑆)
91		eluznn0 11757	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((#‘𝑀) ∈ ℕ₀ ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → 𝑛 ∈ ℕ₀)
92	41, 91	sylan 488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → 𝑛 ∈ ℕ₀)
93	73, 90, 92	subiwrdlen 30448	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → (#‘((𝑀seq_str𝐹) ↾ (0..^𝑛))) = 𝑛)
94	93, 76	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → (#‘((𝑀seq_str𝐹) ↾ (0..^𝑛))) ∈ (ℤ_≥‘(#‘𝑀)))
95		hashf 13125	. . . . . . . . . . . . . . . . . . . . 21 ⊢ #:V⟶(ℕ₀ ∪ {+∞})
96		ffn 6045	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (#:V⟶(ℕ₀ ∪ {+∞}) → # Fn V)
97		elpreima 6337	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (# Fn V → (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ∈ (^◡# “ (ℤ_≥‘(#‘𝑀))) ↔ (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ∈ V ∧ (#‘((𝑀seq_str𝐹) ↾ (0..^𝑛))) ∈ (ℤ_≥‘(#‘𝑀)))))
98	95, 96, 97	mp2b 10	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ∈ (^◡# “ (ℤ_≥‘(#‘𝑀))) ↔ (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ∈ V ∧ (#‘((𝑀seq_str𝐹) ↾ (0..^𝑛))) ∈ (ℤ_≥‘(#‘𝑀))))
99	89, 94, 98	sylanbrc 698	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → ((𝑀seq_str𝐹) ↾ (0..^𝑛)) ∈ (^◡# “ (ℤ_≥‘(#‘𝑀))))
100	87, 99	elind 3798	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → ((𝑀seq_str𝐹) ↾ (0..^𝑛)) ∈ (Word 𝑆 ∩ (^◡# “ (ℤ_≥‘(#‘𝑀)))))
101	100, 3	syl6eleqr 2712	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → ((𝑀seq_str𝐹) ↾ (0..^𝑛)) ∈ 𝑊)
102	75, 101	ffvelrnd 6360	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛))) ∈ 𝑆)
103		lswccats1 13411	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑀seq_str𝐹) ↾ (0..^𝑛)) ∈ Word 𝑆 ∧ (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛))) ∈ 𝑆) → ( lastS ‘(((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)) = (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛))))
104	87, 102, 103	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → ( lastS ‘(((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)) = (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛))))
105	104	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)) → ( lastS ‘(((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)) = (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛))))
106	78, 80, 105	3eqtrrd 2661	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)) → (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛))) = ((𝑀seq_str𝐹)‘𝑛))
107	106	s1eqd 13381	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)) → ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩ = ⟨“((𝑀seq_str𝐹)‘𝑛)”⟩)
108	107	oveq2d 6666	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)) → (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“((𝑀seq_str𝐹)‘𝑛)”⟩))
109	73, 90, 92	iwrdsplit 30449	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → ((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“((𝑀seq_str𝐹)‘𝑛)”⟩))
110	109	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)) → ((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“((𝑀seq_str𝐹)‘𝑛)”⟩))
111	108, 79, 110	3eqtr4d 2666	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = ((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))))
112	111	fveq2d 6195	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)) → (𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛)) = (𝐹‘((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1)))))
113	112	s1eqd 13381	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)) → ⟨“(𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛))”⟩ = ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))))”⟩)
114	111, 113	oveq12d 6668	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)) → ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) ++ ⟨“(𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛))”⟩) = (((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))))”⟩))
115	72, 114	eqtrd 2656	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘(𝑛 + 1)) = (((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))))”⟩))
116	115	ex 450	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘(𝑛 + 1)) = (((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))))”⟩)))
117	116	expcom 451	. . . . . 6 ⊢ (𝑛 ∈ (ℤ_≥‘(#‘𝑀)) → (𝜑 → ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘(𝑛 + 1)) = (((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))))”⟩))))
118	117	a2d 29	. . . . 5 ⊢ (𝑛 ∈ (ℤ_≥‘(#‘𝑀)) → ((𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)) → (𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘(𝑛 + 1)) = (((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))))”⟩))))
119	14, 22, 30, 38, 52, 118	uzind4 11746	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘(#‘𝑀)) → (𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑁) = (((𝑀seq_str𝐹) ↾ (0..^𝑁)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑁)))”⟩)))
120	5, 119	mpcom 38	. . 3 ⊢ (𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑁) = (((𝑀seq_str𝐹) ↾ (0..^𝑁)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑁)))”⟩))
121	120	fveq2d 6195	. 2 ⊢ (𝜑 → ( lastS ‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑁)) = ( lastS ‘(((𝑀seq_str𝐹) ↾ (0..^𝑁)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑁)))”⟩)))
122		fzo0ssnn0 12548	. . . . 5 ⊢ (0..^𝑁) ⊆ ℕ₀
123		fssres 6070	. . . . 5 ⊢ (((𝑀seq_str𝐹):ℕ₀⟶𝑆 ∧ (0..^𝑁) ⊆ ℕ₀) → ((𝑀seq_str𝐹) ↾ (0..^𝑁)):(0..^𝑁)⟶𝑆)
124	81, 122, 123	sylancl 694	. . . 4 ⊢ (𝜑 → ((𝑀seq_str𝐹) ↾ (0..^𝑁)):(0..^𝑁)⟶𝑆)
125		iswrdi 13309	. . . 4 ⊢ (((𝑀seq_str𝐹) ↾ (0..^𝑁)):(0..^𝑁)⟶𝑆 → ((𝑀seq_str𝐹) ↾ (0..^𝑁)) ∈ Word 𝑆)
126	124, 125	syl 17	. . 3 ⊢ (𝜑 → ((𝑀seq_str𝐹) ↾ (0..^𝑁)) ∈ Word 𝑆)
127		elex 3212	. . . . . . . 8 ⊢ (((𝑀seq_str𝐹) ↾ (0..^𝑁)) ∈ Word 𝑆 → ((𝑀seq_str𝐹) ↾ (0..^𝑁)) ∈ V)
128	126, 127	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑀seq_str𝐹) ↾ (0..^𝑁)) ∈ V)
129		eluznn0 11757	. . . . . . . . . 10 ⊢ (((#‘𝑀) ∈ ℕ₀ ∧ 𝑁 ∈ (ℤ_≥‘(#‘𝑀))) → 𝑁 ∈ ℕ₀)
130	41, 5, 129	syl2anc 693	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
131	1, 81, 130	subiwrdlen 30448	. . . . . . . 8 ⊢ (𝜑 → (#‘((𝑀seq_str𝐹) ↾ (0..^𝑁))) = 𝑁)
132	131, 5	eqeltrd 2701	. . . . . . 7 ⊢ (𝜑 → (#‘((𝑀seq_str𝐹) ↾ (0..^𝑁))) ∈ (ℤ_≥‘(#‘𝑀)))
133		elpreima 6337	. . . . . . . 8 ⊢ (# Fn V → (((𝑀seq_str𝐹) ↾ (0..^𝑁)) ∈ (^◡# “ (ℤ_≥‘(#‘𝑀))) ↔ (((𝑀seq_str𝐹) ↾ (0..^𝑁)) ∈ V ∧ (#‘((𝑀seq_str𝐹) ↾ (0..^𝑁))) ∈ (ℤ_≥‘(#‘𝑀)))))
134	95, 96, 133	mp2b 10	. . . . . . 7 ⊢ (((𝑀seq_str𝐹) ↾ (0..^𝑁)) ∈ (^◡# “ (ℤ_≥‘(#‘𝑀))) ↔ (((𝑀seq_str𝐹) ↾ (0..^𝑁)) ∈ V ∧ (#‘((𝑀seq_str𝐹) ↾ (0..^𝑁))) ∈ (ℤ_≥‘(#‘𝑀))))
135	128, 132, 134	sylanbrc 698	. . . . . 6 ⊢ (𝜑 → ((𝑀seq_str𝐹) ↾ (0..^𝑁)) ∈ (^◡# “ (ℤ_≥‘(#‘𝑀))))
136	126, 135	elind 3798	. . . . 5 ⊢ (𝜑 → ((𝑀seq_str𝐹) ↾ (0..^𝑁)) ∈ (Word 𝑆 ∩ (^◡# “ (ℤ_≥‘(#‘𝑀)))))
137	136, 3	syl6eleqr 2712	. . . 4 ⊢ (𝜑 → ((𝑀seq_str𝐹) ↾ (0..^𝑁)) ∈ 𝑊)
138	4, 137	ffvelrnd 6360	. . 3 ⊢ (𝜑 → (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑁))) ∈ 𝑆)
139		lswccats1 13411	. . 3 ⊢ ((((𝑀seq_str𝐹) ↾ (0..^𝑁)) ∈ Word 𝑆 ∧ (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑁))) ∈ 𝑆) → ( lastS ‘(((𝑀seq_str𝐹) ↾ (0..^𝑁)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑁)))”⟩)) = (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑁))))
140	126, 138, 139	syl2anc 693	. 2 ⊢ (𝜑 → ( lastS ‘(((𝑀seq_str𝐹) ↾ (0..^𝑁)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑁)))”⟩)) = (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑁))))
141	6, 121, 140	3eqtrd 2660	1 ⊢ (𝜑 → ((𝑀seq_str𝐹)‘𝑁) = (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑁))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 = wceq 1483 ∈ wcel 1990 Vcvv 3200 ∪ cun 3572 ∩ cin 3573 ⊆ wss 3574 {csn 4177 × cxp 5112 ^◡ccnv 5113 ↾ cres 5116 “ cima 5117 Fn wfn 5883 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 ↦ cmpt2 6652 0cc0 9936 1c1 9937 + caddc 9939 +∞cpnf 10071 ℕ₀cn0 11292 ℤcz 11377 ℤ_≥cuz 11687 ..^cfzo 12465 seqcseq 12801 #chash 13117 Word cword 13291 lastS clsw 13292 ++ cconcat 13293 ⟨“cs1 13294 seq_strcsseq 30445

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-n0 11293 df-xnn0 11364 df-z 11378 df-uz 11688 df-rp 11833 df-fz 12327 df-fzo 12466 df-seq 12802 df-hash 13118 df-word 13299 df-lsw 13300 df-concat 13301 df-s1 13302 df-substr 13303 df-sseq 30446

This theorem is referenced by: fibp1 30463

W3C validator