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 30585

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 30584	. 2 ⊢ (𝜑 → ((𝑀seq_str𝐹)‘𝑁) = ( lastS ‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑁)))
7		fveq2 6229	. . . . . . 7 ⊢ (𝑖 = (#‘𝑀) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑖) = (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘(#‘𝑀)))
8		oveq2 6698	. . . . . . . . 9 ⊢ (𝑖 = (#‘𝑀) → (0..^𝑖) = (0..^(#‘𝑀)))
9	8	reseq2d 5428	. . . . . . . 8 ⊢ (𝑖 = (#‘𝑀) → ((𝑀seq_str𝐹) ↾ (0..^𝑖)) = ((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀))))
10	9	fveq2d 6233	. . . . . . . . 9 ⊢ (𝑖 = (#‘𝑀) → (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖))) = (𝐹‘((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀)))))
11	10	s1eqd 13417	. . . . . . . 8 ⊢ (𝑖 = (#‘𝑀) → ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩ = ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀))))”⟩)
12	9, 11	oveq12d 6708	. . . . . . 7 ⊢ (𝑖 = (#‘𝑀) → (((𝑀seq_str𝐹) ↾ (0..^𝑖)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩) = (((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀))) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀))))”⟩))
13	7, 12	eqeq12d 2666	. . . . . 6 ⊢ (𝑖 = (#‘𝑀) → ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑖) = (((𝑀seq_str𝐹) ↾ (0..^𝑖)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩) ↔ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘(#‘𝑀)) = (((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀))) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀))))”⟩)))
14	13	imbi2d 329	. . . . 5 ⊢ (𝑖 = (#‘𝑀) → ((𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑖) = (((𝑀seq_str𝐹) ↾ (0..^𝑖)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩)) ↔ (𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘(#‘𝑀)) = (((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀))) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀))))”⟩))))
15		fveq2 6229	. . . . . . 7 ⊢ (𝑖 = 𝑛 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑖) = (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛))
16		oveq2 6698	. . . . . . . . 9 ⊢ (𝑖 = 𝑛 → (0..^𝑖) = (0..^𝑛))
17	16	reseq2d 5428	. . . . . . . 8 ⊢ (𝑖 = 𝑛 → ((𝑀seq_str𝐹) ↾ (0..^𝑖)) = ((𝑀seq_str𝐹) ↾ (0..^𝑛)))
18	17	fveq2d 6233	. . . . . . . . 9 ⊢ (𝑖 = 𝑛 → (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖))) = (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛))))
19	18	s1eqd 13417	. . . . . . . 8 ⊢ (𝑖 = 𝑛 → ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩ = ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)
20	17, 19	oveq12d 6708	. . . . . . 7 ⊢ (𝑖 = 𝑛 → (((𝑀seq_str𝐹) ↾ (0..^𝑖)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩))
21	15, 20	eqeq12d 2666	. . . . . 6 ⊢ (𝑖 = 𝑛 → ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑖) = (((𝑀seq_str𝐹) ↾ (0..^𝑖)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩) ↔ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)))
22	21	imbi2d 329	. . . . 5 ⊢ (𝑖 = 𝑛 → ((𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑖) = (((𝑀seq_str𝐹) ↾ (0..^𝑖)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩)) ↔ (𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩))))
23		fveq2 6229	. . . . . . 7 ⊢ (𝑖 = (𝑛 + 1) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑖) = (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘(𝑛 + 1)))
24		oveq2 6698	. . . . . . . . 9 ⊢ (𝑖 = (𝑛 + 1) → (0..^𝑖) = (0..^(𝑛 + 1)))
25	24	reseq2d 5428	. . . . . . . 8 ⊢ (𝑖 = (𝑛 + 1) → ((𝑀seq_str𝐹) ↾ (0..^𝑖)) = ((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))))
26	25	fveq2d 6233	. . . . . . . . 9 ⊢ (𝑖 = (𝑛 + 1) → (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖))) = (𝐹‘((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1)))))
27	26	s1eqd 13417	. . . . . . . 8 ⊢ (𝑖 = (𝑛 + 1) → ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩ = ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))))”⟩)
28	25, 27	oveq12d 6708	. . . . . . 7 ⊢ (𝑖 = (𝑛 + 1) → (((𝑀seq_str𝐹) ↾ (0..^𝑖)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩) = (((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))))”⟩))
29	23, 28	eqeq12d 2666	. . . . . 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 329	. . . . 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 6229	. . . . . . 7 ⊢ (𝑖 = 𝑁 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑖) = (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑁))
32		oveq2 6698	. . . . . . . . 9 ⊢ (𝑖 = 𝑁 → (0..^𝑖) = (0..^𝑁))
33	32	reseq2d 5428	. . . . . . . 8 ⊢ (𝑖 = 𝑁 → ((𝑀seq_str𝐹) ↾ (0..^𝑖)) = ((𝑀seq_str𝐹) ↾ (0..^𝑁)))
34	33	fveq2d 6233	. . . . . . . . 9 ⊢ (𝑖 = 𝑁 → (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖))) = (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑁))))
35	34	s1eqd 13417	. . . . . . . 8 ⊢ (𝑖 = 𝑁 → ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩ = ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑁)))”⟩)
36	33, 35	oveq12d 6708	. . . . . . 7 ⊢ (𝑖 = 𝑁 → (((𝑀seq_str𝐹) ↾ (0..^𝑖)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩) = (((𝑀seq_str𝐹) ↾ (0..^𝑁)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑁)))”⟩))
37	31, 36	eqeq12d 2666	. . . . . 6 ⊢ (𝑖 = 𝑁 → ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑖) = (((𝑀seq_str𝐹) ↾ (0..^𝑖)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩) ↔ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑁) = (((𝑀seq_str𝐹) ↾ (0..^𝑁)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑁)))”⟩)))
38	37	imbi2d 329	. . . . 5 ⊢ (𝑖 = 𝑁 → ((𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑖) = (((𝑀seq_str𝐹) ↾ (0..^𝑖)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑖)))”⟩)) ↔ (𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑁) = (((𝑀seq_str𝐹) ↾ (0..^𝑁)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑁)))”⟩))))
39		ovex 6718	. . . . . . . 8 ⊢ (𝑀 ++ ⟨“(𝐹‘𝑀)”⟩) ∈ V
40		lencl 13356	. . . . . . . . 9 ⊢ (𝑀 ∈ Word 𝑆 → (#‘𝑀) ∈ ℕ₀)
41	2, 40	syl 17	. . . . . . . 8 ⊢ (𝜑 → (#‘𝑀) ∈ ℕ₀)
42		fvconst2g 6508	. . . . . . . 8 ⊢ (((𝑀 ++ ⟨“(𝐹‘𝑀)”⟩) ∈ V ∧ (#‘𝑀) ∈ ℕ₀) → ((ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)})‘(#‘𝑀)) = (𝑀 ++ ⟨“(𝐹‘𝑀)”⟩))
43	39, 41, 42	sylancr 696	. . . . . . 7 ⊢ (𝜑 → ((ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)})‘(#‘𝑀)) = (𝑀 ++ ⟨“(𝐹‘𝑀)”⟩))
44	40	nn0zd 11518	. . . . . . . 8 ⊢ (𝑀 ∈ Word 𝑆 → (#‘𝑀) ∈ ℤ)
45		seq1 12854	. . . . . . . 8 ⊢ ((#‘𝑀) ∈ ℤ → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘(#‘𝑀)) = ((ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)})‘(#‘𝑀)))
46	2, 44, 45	3syl 18	. . . . . . 7 ⊢ (𝜑 → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘(#‘𝑀)) = ((ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)})‘(#‘𝑀)))
47	1, 2, 3, 4	sseqfres 30583	. . . . . . . 8 ⊢ (𝜑 → ((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀))) = 𝑀)
48	47	fveq2d 6233	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀)))) = (𝐹‘𝑀))
49	48	s1eqd 13417	. . . . . . . 8 ⊢ (𝜑 → ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀))))”⟩ = ⟨“(𝐹‘𝑀)”⟩)
50	47, 49	oveq12d 6708	. . . . . . 7 ⊢ (𝜑 → (((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀))) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^(#‘𝑀))))”⟩) = (𝑀 ++ ⟨“(𝐹‘𝑀)”⟩))
51	43, 46, 50	3eqtr4d 2695	. . . . . 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 12856	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (ℤ_≥‘(#‘𝑀)) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘(𝑛 + 1)) = ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛)(𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩))((ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)})‘(𝑛 + 1))))
54	53	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘(𝑛 + 1)) = ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛)(𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩))((ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)})‘(𝑛 + 1))))
55		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑎 → 𝑥 = 𝑎)
56		fveq2 6229	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑎 → (𝐹‘𝑥) = (𝐹‘𝑎))
57	56	s1eqd 13417	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑎 → ⟨“(𝐹‘𝑥)”⟩ = ⟨“(𝐹‘𝑎)”⟩)
58	55, 57	oveq12d 6708	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑎 → (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩) = (𝑎 ++ ⟨“(𝐹‘𝑎)”⟩))
59		eqidd 2652	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑏 → (𝑎 ++ ⟨“(𝐹‘𝑎)”⟩) = (𝑎 ++ ⟨“(𝐹‘𝑎)”⟩))
60	58, 59	cbvmpt2v 6777	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)) = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ++ ⟨“(𝐹‘𝑎)”⟩))
61	60	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)) = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ++ ⟨“(𝐹‘𝑎)”⟩)))
62		simprl 809	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (𝑎 = (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) ∧ 𝑏 = ((ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)})‘(𝑛 + 1)))) → 𝑎 = (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛))
63	62	fveq2d 6233	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (𝑎 = (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) ∧ 𝑏 = ((ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)})‘(𝑛 + 1)))) → (𝐹‘𝑎) = (𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛)))
64	63	s1eqd 13417	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (𝑎 = (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) ∧ 𝑏 = ((ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)})‘(𝑛 + 1)))) → ⟨“(𝐹‘𝑎)”⟩ = ⟨“(𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛))”⟩)
65	62, 64	oveq12d 6708	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (𝑎 = (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) ∧ 𝑏 = ((ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)})‘(𝑛 + 1)))) → (𝑎 ++ ⟨“(𝐹‘𝑎)”⟩) = ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) ++ ⟨“(𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛))”⟩))
66		fvexd 6241	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) ∈ V)
67		fvexd 6241	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → ((ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)})‘(𝑛 + 1)) ∈ V)
68		ovex 6718	. . . . . . . . . . . . 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 6830	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛)(𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩))((ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)})‘(𝑛 + 1))) = ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) ++ ⟨“(𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛))”⟩))
71	54, 70	eqtrd 2685	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘(𝑛 + 1)) = ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) ++ ⟨“(𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛))”⟩))
72	71	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘(𝑛 + 1)) = ((seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) ++ ⟨“(𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛))”⟩))
73	1	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → 𝑆 ∈ V)
74	2	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → 𝑀 ∈ Word 𝑆)
75	4	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → 𝐹:𝑊⟶𝑆)
76		simpr 476	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → 𝑛 ∈ (ℤ_≥‘(#‘𝑀)))
77	73, 74, 3, 75, 76	sseqfv2 30584	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → ((𝑀seq_str𝐹)‘𝑛) = ( lastS ‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛)))
78	77	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)) → ((𝑀seq_str𝐹)‘𝑛) = ( lastS ‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛)))
79		simpr 476	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩))
80	79	fveq2d 6233	. . . . . . . . . . . . . 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 30582	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑀seq_str𝐹):ℕ₀⟶𝑆)
82		fzo0ssnn0 12588	. . . . . . . . . . . . . . . . . . 19 ⊢ (0..^𝑛) ⊆ ℕ₀
83		fssres 6108	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀seq_str𝐹):ℕ₀⟶𝑆 ∧ (0..^𝑛) ⊆ ℕ₀) → ((𝑀seq_str𝐹) ↾ (0..^𝑛)):(0..^𝑛)⟶𝑆)
84	81, 82, 83	sylancl 695	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑀seq_str𝐹) ↾ (0..^𝑛)):(0..^𝑛)⟶𝑆)
85		iswrdi 13341	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀seq_str𝐹) ↾ (0..^𝑛)):(0..^𝑛)⟶𝑆 → ((𝑀seq_str𝐹) ↾ (0..^𝑛)) ∈ Word 𝑆)
86	84, 85	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑀seq_str𝐹) ↾ (0..^𝑛)) ∈ Word 𝑆)
87	86	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → ((𝑀seq_str𝐹) ↾ (0..^𝑛)) ∈ Word 𝑆)
88		elex 3243	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ∈ Word 𝑆 → ((𝑀seq_str𝐹) ↾ (0..^𝑛)) ∈ V)
89	87, 88	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → ((𝑀seq_str𝐹) ↾ (0..^𝑛)) ∈ V)
90	81	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → (𝑀seq_str𝐹):ℕ₀⟶𝑆)
91		eluznn0 11795	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((#‘𝑀) ∈ ℕ₀ ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → 𝑛 ∈ ℕ₀)
92	41, 91	sylan 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → 𝑛 ∈ ℕ₀)
93	73, 90, 92	subiwrdlen 30576	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → (#‘((𝑀seq_str𝐹) ↾ (0..^𝑛))) = 𝑛)
94	93, 76	eqeltrd 2730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → (#‘((𝑀seq_str𝐹) ↾ (0..^𝑛))) ∈ (ℤ_≥‘(#‘𝑀)))
95		hashf 13165	. . . . . . . . . . . . . . . . . . . . 21 ⊢ #:V⟶(ℕ₀ ∪ {+∞})
96		ffn 6083	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (#:V⟶(ℕ₀ ∪ {+∞}) → # Fn V)
97		elpreima 6377	. . . . . . . . . . . . . . . . . . . . 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 699	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → ((𝑀seq_str𝐹) ↾ (0..^𝑛)) ∈ (^◡# “ (ℤ_≥‘(#‘𝑀))))
100	87, 99	elind 3831	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → ((𝑀seq_str𝐹) ↾ (0..^𝑛)) ∈ (Word 𝑆 ∩ (^◡# “ (ℤ_≥‘(#‘𝑀)))))
101	100, 3	syl6eleqr 2741	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → ((𝑀seq_str𝐹) ↾ (0..^𝑛)) ∈ 𝑊)
102	75, 101	ffvelrnd 6400	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛))) ∈ 𝑆)
103		lswccats1 13456	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑀seq_str𝐹) ↾ (0..^𝑛)) ∈ Word 𝑆 ∧ (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛))) ∈ 𝑆) → ( lastS ‘(((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)) = (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛))))
104	87, 102, 103	syl2anc 694	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → ( lastS ‘(((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)) = (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛))))
105	104	adantr 480	. . . . . . . . . . . . . 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 2690	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)) → (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛))) = ((𝑀seq_str𝐹)‘𝑛))
107	106	s1eqd 13417	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)) → ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩ = ⟨“((𝑀seq_str𝐹)‘𝑛)”⟩)
108	107	oveq2d 6706	. . . . . . . . . . 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 30577	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) → ((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“((𝑀seq_str𝐹)‘𝑛)”⟩))
110	109	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)) → ((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“((𝑀seq_str𝐹)‘𝑛)”⟩))
111	108, 79, 110	3eqtr4d 2695	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)) → (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = ((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))))
112	111	fveq2d 6233	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)) → (𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛)) = (𝐹‘((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1)))))
113	112	s1eqd 13417	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(#‘𝑀))) ∧ (seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛) = (((𝑀seq_str𝐹) ↾ (0..^𝑛)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑛)))”⟩)) → ⟨“(𝐹‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑛))”⟩ = ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^(𝑛 + 1))))”⟩)
114	111, 113	oveq12d 6708	. . . . . . . . 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 2685	. . . . . . . 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 449	. . . . . . 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 450	. . . . . 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 11784	. . . 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 6233	. 2 ⊢ (𝜑 → ( lastS ‘(seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ₀ × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑁)) = ( lastS ‘(((𝑀seq_str𝐹) ↾ (0..^𝑁)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑁)))”⟩)))
122		fzo0ssnn0 12588	. . . . 5 ⊢ (0..^𝑁) ⊆ ℕ₀
123		fssres 6108	. . . . 5 ⊢ (((𝑀seq_str𝐹):ℕ₀⟶𝑆 ∧ (0..^𝑁) ⊆ ℕ₀) → ((𝑀seq_str𝐹) ↾ (0..^𝑁)):(0..^𝑁)⟶𝑆)
124	81, 122, 123	sylancl 695	. . . 4 ⊢ (𝜑 → ((𝑀seq_str𝐹) ↾ (0..^𝑁)):(0..^𝑁)⟶𝑆)
125		iswrdi 13341	. . . 4 ⊢ (((𝑀seq_str𝐹) ↾ (0..^𝑁)):(0..^𝑁)⟶𝑆 → ((𝑀seq_str𝐹) ↾ (0..^𝑁)) ∈ Word 𝑆)
126	124, 125	syl 17	. . 3 ⊢ (𝜑 → ((𝑀seq_str𝐹) ↾ (0..^𝑁)) ∈ Word 𝑆)
127		elex 3243	. . . . . . . 8 ⊢ (((𝑀seq_str𝐹) ↾ (0..^𝑁)) ∈ Word 𝑆 → ((𝑀seq_str𝐹) ↾ (0..^𝑁)) ∈ V)
128	126, 127	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑀seq_str𝐹) ↾ (0..^𝑁)) ∈ V)
129		eluznn0 11795	. . . . . . . . . 10 ⊢ (((#‘𝑀) ∈ ℕ₀ ∧ 𝑁 ∈ (ℤ_≥‘(#‘𝑀))) → 𝑁 ∈ ℕ₀)
130	41, 5, 129	syl2anc 694	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
131	1, 81, 130	subiwrdlen 30576	. . . . . . . 8 ⊢ (𝜑 → (#‘((𝑀seq_str𝐹) ↾ (0..^𝑁))) = 𝑁)
132	131, 5	eqeltrd 2730	. . . . . . 7 ⊢ (𝜑 → (#‘((𝑀seq_str𝐹) ↾ (0..^𝑁))) ∈ (ℤ_≥‘(#‘𝑀)))
133		elpreima 6377	. . . . . . . 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 699	. . . . . 6 ⊢ (𝜑 → ((𝑀seq_str𝐹) ↾ (0..^𝑁)) ∈ (^◡# “ (ℤ_≥‘(#‘𝑀))))
136	126, 135	elind 3831	. . . . 5 ⊢ (𝜑 → ((𝑀seq_str𝐹) ↾ (0..^𝑁)) ∈ (Word 𝑆 ∩ (^◡# “ (ℤ_≥‘(#‘𝑀)))))
137	136, 3	syl6eleqr 2741	. . . 4 ⊢ (𝜑 → ((𝑀seq_str𝐹) ↾ (0..^𝑁)) ∈ 𝑊)
138	4, 137	ffvelrnd 6400	. . 3 ⊢ (𝜑 → (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑁))) ∈ 𝑆)
139		lswccats1 13456	. . 3 ⊢ ((((𝑀seq_str𝐹) ↾ (0..^𝑁)) ∈ Word 𝑆 ∧ (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑁))) ∈ 𝑆) → ( lastS ‘(((𝑀seq_str𝐹) ↾ (0..^𝑁)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑁)))”⟩)) = (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑁))))
140	126, 138, 139	syl2anc 694	. 2 ⊢ (𝜑 → ( lastS ‘(((𝑀seq_str𝐹) ↾ (0..^𝑁)) ++ ⟨“(𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑁)))”⟩)) = (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑁))))
141	6, 121, 140	3eqtrd 2689	1 ⊢ (𝜑 → ((𝑀seq_str𝐹)‘𝑁) = (𝐹‘((𝑀seq_str𝐹) ↾ (0..^𝑁))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 = wceq 1523 ∈ wcel 2030 Vcvv 3231 ∪ cun 3605 ∩ cin 3606 ⊆ wss 3607 {csn 4210 × cxp 5141 ^◡ccnv 5142 ↾ cres 5145 “ cima 5146 Fn wfn 5921 ⟶wf 5922 ‘cfv 5926 (class class class)co 6690 ↦ cmpt2 6692 0cc0 9974 1c1 9975 + caddc 9977 +∞cpnf 10109 ℕ₀cn0 11330 ℤcz 11415 ℤ_≥cuz 11725 ..^cfzo 12504 seqcseq 12841 #chash 13157 Word cword 13323 lastS clsw 13324 ++ cconcat 13325 ⟨“cs1 13326 seq_strcsseq 30573

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-8 2032 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-rep 4804 ax-sep 4814 ax-nul 4822 ax-pow 4873 ax-pr 4936 ax-un 6991 ax-inf2 8576 ax-cnex 10030 ax-resscn 10031 ax-1cn 10032 ax-icn 10033 ax-addcl 10034 ax-addrcl 10035 ax-mulcl 10036 ax-mulrcl 10037 ax-mulcom 10038 ax-addass 10039 ax-mulass 10040 ax-distr 10041 ax-i2m1 10042 ax-1ne0 10043 ax-1rid 10044 ax-rnegex 10045 ax-rrecex 10046 ax-cnre 10047 ax-pre-lttri 10048 ax-pre-lttrn 10049 ax-pre-ltadd 10050 ax-pre-mulgt0 10051

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1055 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-eu 2502 df-mo 2503 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ne 2824 df-nel 2927 df-ral 2946 df-rex 2947 df-reu 2948 df-rab 2950 df-v 3233 df-sbc 3469 df-csb 3567 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-pss 3623 df-nul 3949 df-if 4120 df-pw 4193 df-sn 4211 df-pr 4213 df-tp 4215 df-op 4217 df-uni 4469 df-int 4508 df-iun 4554 df-br 4686 df-opab 4746 df-mpt 4763 df-tr 4786 df-id 5053 df-eprel 5058 df-po 5064 df-so 5065 df-fr 5102 df-we 5104 df-xp 5149 df-rel 5150 df-cnv 5151 df-co 5152 df-dm 5153 df-rn 5154 df-res 5155 df-ima 5156 df-pred 5718 df-ord 5764 df-on 5765 df-lim 5766 df-suc 5767 df-iota 5889 df-fun 5928 df-fn 5929 df-f 5930 df-f1 5931 df-fo 5932 df-f1o 5933 df-fv 5934 df-riota 6651 df-ov 6693 df-oprab 6694 df-mpt2 6695 df-om 7108 df-1st 7210 df-2nd 7211 df-wrecs 7452 df-recs 7513 df-rdg 7551 df-1o 7605 df-oadd 7609 df-er 7787 df-map 7901 df-pm 7902 df-en 7998 df-dom 7999 df-sdom 8000 df-fin 8001 df-card 8803 df-pnf 10114 df-mnf 10115 df-xr 10116 df-ltxr 10117 df-le 10118 df-sub 10306 df-neg 10307 df-nn 11059 df-n0 11331 df-xnn0 11402 df-z 11416 df-uz 11726 df-rp 11871 df-fz 12365 df-fzo 12505 df-seq 12842 df-hash 13158 df-word 13331 df-lsw 13332 df-concat 13333 df-s1 13334 df-substr 13335 df-sseq 30574

This theorem is referenced by: fibp1 30591

W3C validator