pfx2 - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > pfx2		Structured version Visualization version GIF version

Theorem pfx2 40275

Description: A prefix of length 2. (Contributed by AV, 15-May-2020.)

**Assertion**
Ref	Expression
pfx2	⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑊)) → (𝑊 prefix 2) = ⟨“(𝑊‘0)(𝑊‘1)”⟩)

Proof of Theorem pfx2 Dummy variable 𝑖 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		2nn0 11186	. . . 4 ⊢ 2 ∈ ℕ₀
2	1	a1i 11	. . 3 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑊)) → 2 ∈ ℕ₀)
3		lencl 13179	. . . 4 ⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∈ ℕ₀)
4	3	adantr 480	. . 3 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑊)) → (#‘𝑊) ∈ ℕ₀)
5		simpr 476	. . 3 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑊)) → 2 ≤ (#‘𝑊))
6		elfz2nn0 12300	. . 3 ⊢ (2 ∈ (0...(#‘𝑊)) ↔ (2 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ₀ ∧ 2 ≤ (#‘𝑊)))
7	2, 4, 5, 6	syl3anbrc 1239	. 2 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑊)) → 2 ∈ (0...(#‘𝑊)))
8		pfxlen 40254	. . . 4 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) → (#‘(𝑊 prefix 2)) = 2)
9		s2len 13484	. . . . . . 7 ⊢ (#‘⟨“(𝑊‘0)(𝑊‘1)”⟩) = 2
10	9	eqcomi 2619	. . . . . 6 ⊢ 2 = (#‘⟨“(𝑊‘0)(𝑊‘1)”⟩)
11	10	a1i 11	. . . . 5 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) ∧ (#‘(𝑊 prefix 2)) = 2) → 2 = (#‘⟨“(𝑊‘0)(𝑊‘1)”⟩))
12		simpl 472	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) → 𝑊 ∈ Word 𝑉)
13		simpr 476	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) → 2 ∈ (0...(#‘𝑊)))
14		2nn 11062	. . . . . . . . . . . 12 ⊢ 2 ∈ ℕ
15		lbfzo0 12375	. . . . . . . . . . . 12 ⊢ (0 ∈ (0..^2) ↔ 2 ∈ ℕ)
16	14, 15	mpbir 220	. . . . . . . . . . 11 ⊢ 0 ∈ (0..^2)
17	16	a1i 11	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) → 0 ∈ (0..^2))
18	12, 13, 17	3jca 1235	. . . . . . . . 9 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) → (𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊)) ∧ 0 ∈ (0..^2)))
19	18	adantr 480	. . . . . . . 8 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) ∧ (#‘(𝑊 prefix 2)) = 2) → (𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊)) ∧ 0 ∈ (0..^2)))
20		pfxfv 40262	. . . . . . . 8 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊)) ∧ 0 ∈ (0..^2)) → ((𝑊 prefix 2)‘0) = (𝑊‘0))
21	19, 20	syl 17	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) ∧ (#‘(𝑊 prefix 2)) = 2) → ((𝑊 prefix 2)‘0) = (𝑊‘0))
22		fvex 6113	. . . . . . . 8 ⊢ (𝑊‘0) ∈ V
23		s2fv0 13482	. . . . . . . 8 ⊢ ((𝑊‘0) ∈ V → (⟨“(𝑊‘0)(𝑊‘1)”⟩‘0) = (𝑊‘0))
24	22, 23	ax-mp 5	. . . . . . 7 ⊢ (⟨“(𝑊‘0)(𝑊‘1)”⟩‘0) = (𝑊‘0)
25	21, 24	syl6eqr 2662	. . . . . 6 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) ∧ (#‘(𝑊 prefix 2)) = 2) → ((𝑊 prefix 2)‘0) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘0))
26		1nn0 11185	. . . . . . . . . 10 ⊢ 1 ∈ ℕ₀
27		1lt2 11071	. . . . . . . . . 10 ⊢ 1 < 2
28		elfzo0 12376	. . . . . . . . . 10 ⊢ (1 ∈ (0..^2) ↔ (1 ∈ ℕ₀ ∧ 2 ∈ ℕ ∧ 1 < 2))
29	26, 14, 27, 28	mpbir3an 1237	. . . . . . . . 9 ⊢ 1 ∈ (0..^2)
30		pfxfv 40262	. . . . . . . . 9 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊)) ∧ 1 ∈ (0..^2)) → ((𝑊 prefix 2)‘1) = (𝑊‘1))
31	29, 30	mp3an3 1405	. . . . . . . 8 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) → ((𝑊 prefix 2)‘1) = (𝑊‘1))
32		fvex 6113	. . . . . . . . 9 ⊢ (𝑊‘1) ∈ V
33		s2fv1 13483	. . . . . . . . 9 ⊢ ((𝑊‘1) ∈ V → (⟨“(𝑊‘0)(𝑊‘1)”⟩‘1) = (𝑊‘1))
34	32, 33	ax-mp 5	. . . . . . . 8 ⊢ (⟨“(𝑊‘0)(𝑊‘1)”⟩‘1) = (𝑊‘1)
35	31, 34	syl6eqr 2662	. . . . . . 7 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) → ((𝑊 prefix 2)‘1) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘1))
36	35	adantr 480	. . . . . 6 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) ∧ (#‘(𝑊 prefix 2)) = 2) → ((𝑊 prefix 2)‘1) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘1))
37		0nn0 11184	. . . . . . . . 9 ⊢ 0 ∈ ℕ₀
38	37, 26	pm3.2i 470	. . . . . . . 8 ⊢ (0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀)
39	38	a1i 11	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) ∧ (#‘(𝑊 prefix 2)) = 2) → (0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀))
40		fveq2 6103	. . . . . . . . 9 ⊢ (𝑖 = 0 → ((𝑊 prefix 2)‘𝑖) = ((𝑊 prefix 2)‘0))
41		fveq2 6103	. . . . . . . . 9 ⊢ (𝑖 = 0 → (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘0))
42	40, 41	eqeq12d 2625	. . . . . . . 8 ⊢ (𝑖 = 0 → (((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖) ↔ ((𝑊 prefix 2)‘0) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘0)))
43		fveq2 6103	. . . . . . . . 9 ⊢ (𝑖 = 1 → ((𝑊 prefix 2)‘𝑖) = ((𝑊 prefix 2)‘1))
44		fveq2 6103	. . . . . . . . 9 ⊢ (𝑖 = 1 → (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘1))
45	43, 44	eqeq12d 2625	. . . . . . . 8 ⊢ (𝑖 = 1 → (((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖) ↔ ((𝑊 prefix 2)‘1) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘1)))
46	42, 45	ralprg 4181	. . . . . . 7 ⊢ ((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) → (∀𝑖 ∈ {0, 1} ((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖) ↔ (((𝑊 prefix 2)‘0) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘0) ∧ ((𝑊 prefix 2)‘1) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘1))))
47	39, 46	syl 17	. . . . . 6 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) ∧ (#‘(𝑊 prefix 2)) = 2) → (∀𝑖 ∈ {0, 1} ((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖) ↔ (((𝑊 prefix 2)‘0) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘0) ∧ ((𝑊 prefix 2)‘1) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘1))))
48	25, 36, 47	mpbir2and 959	. . . . 5 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) ∧ (#‘(𝑊 prefix 2)) = 2) → ∀𝑖 ∈ {0, 1} ((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖))
49		eqeq1 2614	. . . . . . 7 ⊢ ((#‘(𝑊 prefix 2)) = 2 → ((#‘(𝑊 prefix 2)) = (#‘⟨“(𝑊‘0)(𝑊‘1)”⟩) ↔ 2 = (#‘⟨“(𝑊‘0)(𝑊‘1)”⟩)))
50		oveq2 6557	. . . . . . . . 9 ⊢ ((#‘(𝑊 prefix 2)) = 2 → (0..^(#‘(𝑊 prefix 2))) = (0..^2))
51		fzo0to2pr 12420	. . . . . . . . 9 ⊢ (0..^2) = {0, 1}
52	50, 51	syl6eq 2660	. . . . . . . 8 ⊢ ((#‘(𝑊 prefix 2)) = 2 → (0..^(#‘(𝑊 prefix 2))) = {0, 1})
53	52	raleqdv 3121	. . . . . . 7 ⊢ ((#‘(𝑊 prefix 2)) = 2 → (∀𝑖 ∈ (0..^(#‘(𝑊 prefix 2)))((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖) ↔ ∀𝑖 ∈ {0, 1} ((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖)))
54	49, 53	anbi12d 743	. . . . . 6 ⊢ ((#‘(𝑊 prefix 2)) = 2 → (((#‘(𝑊 prefix 2)) = (#‘⟨“(𝑊‘0)(𝑊‘1)”⟩) ∧ ∀𝑖 ∈ (0..^(#‘(𝑊 prefix 2)))((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖)) ↔ (2 = (#‘⟨“(𝑊‘0)(𝑊‘1)”⟩) ∧ ∀𝑖 ∈ {0, 1} ((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖))))
55	54	adantl 481	. . . . 5 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) ∧ (#‘(𝑊 prefix 2)) = 2) → (((#‘(𝑊 prefix 2)) = (#‘⟨“(𝑊‘0)(𝑊‘1)”⟩) ∧ ∀𝑖 ∈ (0..^(#‘(𝑊 prefix 2)))((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖)) ↔ (2 = (#‘⟨“(𝑊‘0)(𝑊‘1)”⟩) ∧ ∀𝑖 ∈ {0, 1} ((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖))))
56	11, 48, 55	mpbir2and 959	. . . 4 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) ∧ (#‘(𝑊 prefix 2)) = 2) → ((#‘(𝑊 prefix 2)) = (#‘⟨“(𝑊‘0)(𝑊‘1)”⟩) ∧ ∀𝑖 ∈ (0..^(#‘(𝑊 prefix 2)))((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖)))
57	8, 56	mpdan 699	. . 3 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) → ((#‘(𝑊 prefix 2)) = (#‘⟨“(𝑊‘0)(𝑊‘1)”⟩) ∧ ∀𝑖 ∈ (0..^(#‘(𝑊 prefix 2)))((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖)))
58		pfxcl 40249	. . . . 5 ⊢ (𝑊 ∈ Word 𝑉 → (𝑊 prefix 2) ∈ Word 𝑉)
59	58	adantr 480	. . . 4 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) → (𝑊 prefix 2) ∈ Word 𝑉)
60		simp2 1055	. . . . . . . . . 10 ⊢ ((2 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ₀ ∧ 2 ≤ (#‘𝑊)) → (#‘𝑊) ∈ ℕ₀)
61		1red 9934	. . . . . . . . . . . . . . 15 ⊢ ((#‘𝑊) ∈ ℕ₀ → 1 ∈ ℝ)
62		2re 10967	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ
63	62	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((#‘𝑊) ∈ ℕ₀ → 2 ∈ ℝ)
64		nn0re 11178	. . . . . . . . . . . . . . 15 ⊢ ((#‘𝑊) ∈ ℕ₀ → (#‘𝑊) ∈ ℝ)
65	61, 63, 64	3jca 1235	. . . . . . . . . . . . . 14 ⊢ ((#‘𝑊) ∈ ℕ₀ → (1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (#‘𝑊) ∈ ℝ))
66		ltleletr 10009	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (#‘𝑊) ∈ ℝ) → ((1 < 2 ∧ 2 ≤ (#‘𝑊)) → 1 ≤ (#‘𝑊)))
67	65, 66	syl 17	. . . . . . . . . . . . 13 ⊢ ((#‘𝑊) ∈ ℕ₀ → ((1 < 2 ∧ 2 ≤ (#‘𝑊)) → 1 ≤ (#‘𝑊)))
68	27, 67	mpani 708	. . . . . . . . . . . 12 ⊢ ((#‘𝑊) ∈ ℕ₀ → (2 ≤ (#‘𝑊) → 1 ≤ (#‘𝑊)))
69	68	imp 444	. . . . . . . . . . 11 ⊢ (((#‘𝑊) ∈ ℕ₀ ∧ 2 ≤ (#‘𝑊)) → 1 ≤ (#‘𝑊))
70	69	3adant1 1072	. . . . . . . . . 10 ⊢ ((2 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ₀ ∧ 2 ≤ (#‘𝑊)) → 1 ≤ (#‘𝑊))
71	60, 70	jca 553	. . . . . . . . 9 ⊢ ((2 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ₀ ∧ 2 ≤ (#‘𝑊)) → ((#‘𝑊) ∈ ℕ₀ ∧ 1 ≤ (#‘𝑊)))
72		elnnnn0c 11215	. . . . . . . . 9 ⊢ ((#‘𝑊) ∈ ℕ ↔ ((#‘𝑊) ∈ ℕ₀ ∧ 1 ≤ (#‘𝑊)))
73	71, 72	sylibr 223	. . . . . . . 8 ⊢ ((2 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ₀ ∧ 2 ≤ (#‘𝑊)) → (#‘𝑊) ∈ ℕ)
74	6, 73	sylbi 206	. . . . . . 7 ⊢ (2 ∈ (0...(#‘𝑊)) → (#‘𝑊) ∈ ℕ)
75		lbfzo0 12375	. . . . . . 7 ⊢ (0 ∈ (0..^(#‘𝑊)) ↔ (#‘𝑊) ∈ ℕ)
76	74, 75	sylibr 223	. . . . . 6 ⊢ (2 ∈ (0...(#‘𝑊)) → 0 ∈ (0..^(#‘𝑊)))
77		wrdsymbcl 13173	. . . . . 6 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 0 ∈ (0..^(#‘𝑊))) → (𝑊‘0) ∈ 𝑉)
78	76, 77	sylan2 490	. . . . 5 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) → (𝑊‘0) ∈ 𝑉)
79	26	a1i 11	. . . . . . 7 ⊢ (2 ∈ (0...(#‘𝑊)) → 1 ∈ ℕ₀)
80	65	adantl 481	. . . . . . . . . . 11 ⊢ ((2 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ₀) → (1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (#‘𝑊) ∈ ℝ))
81		ltletr 10008	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (#‘𝑊) ∈ ℝ) → ((1 < 2 ∧ 2 ≤ (#‘𝑊)) → 1 < (#‘𝑊)))
82	80, 81	syl 17	. . . . . . . . . 10 ⊢ ((2 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ₀) → ((1 < 2 ∧ 2 ≤ (#‘𝑊)) → 1 < (#‘𝑊)))
83	27, 82	mpani 708	. . . . . . . . 9 ⊢ ((2 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ₀) → (2 ≤ (#‘𝑊) → 1 < (#‘𝑊)))
84	83	3impia 1253	. . . . . . . 8 ⊢ ((2 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ₀ ∧ 2 ≤ (#‘𝑊)) → 1 < (#‘𝑊))
85	6, 84	sylbi 206	. . . . . . 7 ⊢ (2 ∈ (0...(#‘𝑊)) → 1 < (#‘𝑊))
86		elfzo0 12376	. . . . . . 7 ⊢ (1 ∈ (0..^(#‘𝑊)) ↔ (1 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ ∧ 1 < (#‘𝑊)))
87	79, 74, 85, 86	syl3anbrc 1239	. . . . . 6 ⊢ (2 ∈ (0...(#‘𝑊)) → 1 ∈ (0..^(#‘𝑊)))
88		wrdsymbcl 13173	. . . . . 6 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 1 ∈ (0..^(#‘𝑊))) → (𝑊‘1) ∈ 𝑉)
89	87, 88	sylan2 490	. . . . 5 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) → (𝑊‘1) ∈ 𝑉)
90	78, 89	s2cld 13466	. . . 4 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) → ⟨“(𝑊‘0)(𝑊‘1)”⟩ ∈ Word 𝑉)
91		eqwrd 13201	. . . 4 ⊢ (((𝑊 prefix 2) ∈ Word 𝑉 ∧ ⟨“(𝑊‘0)(𝑊‘1)”⟩ ∈ Word 𝑉) → ((𝑊 prefix 2) = ⟨“(𝑊‘0)(𝑊‘1)”⟩ ↔ ((#‘(𝑊 prefix 2)) = (#‘⟨“(𝑊‘0)(𝑊‘1)”⟩) ∧ ∀𝑖 ∈ (0..^(#‘(𝑊 prefix 2)))((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖))))
92	59, 90, 91	syl2anc 691	. . 3 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) → ((𝑊 prefix 2) = ⟨“(𝑊‘0)(𝑊‘1)”⟩ ↔ ((#‘(𝑊 prefix 2)) = (#‘⟨“(𝑊‘0)(𝑊‘1)”⟩) ∧ ∀𝑖 ∈ (0..^(#‘(𝑊 prefix 2)))((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖))))
93	57, 92	mpbird 246	. 2 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(#‘𝑊))) → (𝑊 prefix 2) = ⟨“(𝑊‘0)(𝑊‘1)”⟩)
94	7, 93	syldan 486	1 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑊)) → (𝑊 prefix 2) = ⟨“(𝑊‘0)(𝑊‘1)”⟩)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ∀wral 2896 Vcvv 3173 {cpr 4127 class class class wbr 4583 ‘cfv 5804 (class class class)co 6549 ℝcr 9814 0cc0 9815 1c1 9816 < clt 9953 ≤ cle 9954 ℕcn 10897 2c2 10947 ℕ₀cn0 11169 ...cfz 12197 ..^cfzo 12334 #chash 12979 Word cword 13146 ⟨“cs2 13437 prefix cpfx 40244

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-oadd 7451 df-er 7629 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-card 8648 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-nn 10898 df-2 10956 df-n0 11170 df-z 11255 df-uz 11564 df-fz 12198 df-fzo 12335 df-hash 12980 df-word 13154 df-concat 13156 df-s1 13157 df-substr 13158 df-s2 13444 df-pfx 40245

This theorem is referenced by: (None)

W3C validator