pfx2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > pfx2		Structured version Visualization version GIF version

Theorem pfx2 14900

Description: A prefix of length two. (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 12491	. . . 4 ⊢ 2 ∈ ℕ₀
2	1	a1i 11	. . 3 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑊)) → 2 ∈ ℕ₀)
3		lencl 14485	. . . 4 ⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℕ₀)
4	3	adantr 481	. . 3 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑊)) → (♯‘𝑊) ∈ ℕ₀)
5		simpr 485	. . 3 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑊)) → 2 ≤ (♯‘𝑊))
6		elfz2nn0 13594	. . 3 ⊢ (2 ∈ (0...(♯‘𝑊)) ↔ (2 ∈ ℕ₀ ∧ (♯‘𝑊) ∈ ℕ₀ ∧ 2 ≤ (♯‘𝑊)))
7	2, 4, 5, 6	syl3anbrc 1343	. 2 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑊)) → 2 ∈ (0...(♯‘𝑊)))
8		pfxlen 14635	. . . 4 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 prefix 2)) = 2)
9		s2len 14842	. . . . . . 7 ⊢ (♯‘⟨“(𝑊‘0)(𝑊‘1)”⟩) = 2
10	9	eqcomi 2741	. . . . . 6 ⊢ 2 = (♯‘⟨“(𝑊‘0)(𝑊‘1)”⟩)
11	10	a1i 11	. . . . 5 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) ∧ (♯‘(𝑊 prefix 2)) = 2) → 2 = (♯‘⟨“(𝑊‘0)(𝑊‘1)”⟩))
12		2nn 12287	. . . . . . . . . 10 ⊢ 2 ∈ ℕ
13		lbfzo0 13674	. . . . . . . . . 10 ⊢ (0 ∈ (0..^2) ↔ 2 ∈ ℕ)
14	12, 13	mpbir 230	. . . . . . . . 9 ⊢ 0 ∈ (0..^2)
15		pfxfv 14634	. . . . . . . . 9 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊)) ∧ 0 ∈ (0..^2)) → ((𝑊 prefix 2)‘0) = (𝑊‘0))
16	14, 15	mp3an3 1450	. . . . . . . 8 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) → ((𝑊 prefix 2)‘0) = (𝑊‘0))
17	16	adantr 481	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) ∧ (♯‘(𝑊 prefix 2)) = 2) → ((𝑊 prefix 2)‘0) = (𝑊‘0))
18		fvex 6904	. . . . . . . 8 ⊢ (𝑊‘0) ∈ V
19		s2fv0 14840	. . . . . . . 8 ⊢ ((𝑊‘0) ∈ V → (⟨“(𝑊‘0)(𝑊‘1)”⟩‘0) = (𝑊‘0))
20	18, 19	ax-mp 5	. . . . . . 7 ⊢ (⟨“(𝑊‘0)(𝑊‘1)”⟩‘0) = (𝑊‘0)
21	17, 20	eqtr4di 2790	. . . . . 6 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) ∧ (♯‘(𝑊 prefix 2)) = 2) → ((𝑊 prefix 2)‘0) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘0))
22		1nn0 12490	. . . . . . . . . 10 ⊢ 1 ∈ ℕ₀
23		1lt2 12385	. . . . . . . . . 10 ⊢ 1 < 2
24		elfzo0 13675	. . . . . . . . . 10 ⊢ (1 ∈ (0..^2) ↔ (1 ∈ ℕ₀ ∧ 2 ∈ ℕ ∧ 1 < 2))
25	22, 12, 23, 24	mpbir3an 1341	. . . . . . . . 9 ⊢ 1 ∈ (0..^2)
26		pfxfv 14634	. . . . . . . . 9 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊)) ∧ 1 ∈ (0..^2)) → ((𝑊 prefix 2)‘1) = (𝑊‘1))
27	25, 26	mp3an3 1450	. . . . . . . 8 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) → ((𝑊 prefix 2)‘1) = (𝑊‘1))
28		fvex 6904	. . . . . . . . 9 ⊢ (𝑊‘1) ∈ V
29		s2fv1 14841	. . . . . . . . 9 ⊢ ((𝑊‘1) ∈ V → (⟨“(𝑊‘0)(𝑊‘1)”⟩‘1) = (𝑊‘1))
30	28, 29	ax-mp 5	. . . . . . . 8 ⊢ (⟨“(𝑊‘0)(𝑊‘1)”⟩‘1) = (𝑊‘1)
31	27, 30	eqtr4di 2790	. . . . . . 7 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) → ((𝑊 prefix 2)‘1) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘1))
32	31	adantr 481	. . . . . 6 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) ∧ (♯‘(𝑊 prefix 2)) = 2) → ((𝑊 prefix 2)‘1) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘1))
33		0nn0 12489	. . . . . . 7 ⊢ 0 ∈ ℕ₀
34		fveq2 6891	. . . . . . . . 9 ⊢ (𝑖 = 0 → ((𝑊 prefix 2)‘𝑖) = ((𝑊 prefix 2)‘0))
35		fveq2 6891	. . . . . . . . 9 ⊢ (𝑖 = 0 → (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘0))
36	34, 35	eqeq12d 2748	. . . . . . . 8 ⊢ (𝑖 = 0 → (((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖) ↔ ((𝑊 prefix 2)‘0) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘0)))
37		fveq2 6891	. . . . . . . . 9 ⊢ (𝑖 = 1 → ((𝑊 prefix 2)‘𝑖) = ((𝑊 prefix 2)‘1))
38		fveq2 6891	. . . . . . . . 9 ⊢ (𝑖 = 1 → (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘1))
39	37, 38	eqeq12d 2748	. . . . . . . 8 ⊢ (𝑖 = 1 → (((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖) ↔ ((𝑊 prefix 2)‘1) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘1)))
40	36, 39	ralprg 4698	. . . . . . 7 ⊢ ((0 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) → (∀𝑖 ∈ {0, 1} ((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖) ↔ (((𝑊 prefix 2)‘0) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘0) ∧ ((𝑊 prefix 2)‘1) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘1))))
41	33, 22, 40	mp2an 690	. . . . . 6 ⊢ (∀𝑖 ∈ {0, 1} ((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖) ↔ (((𝑊 prefix 2)‘0) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘0) ∧ ((𝑊 prefix 2)‘1) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘1)))
42	21, 32, 41	sylanbrc 583	. . . . 5 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) ∧ (♯‘(𝑊 prefix 2)) = 2) → ∀𝑖 ∈ {0, 1} ((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖))
43		eqeq1 2736	. . . . . . 7 ⊢ ((♯‘(𝑊 prefix 2)) = 2 → ((♯‘(𝑊 prefix 2)) = (♯‘⟨“(𝑊‘0)(𝑊‘1)”⟩) ↔ 2 = (♯‘⟨“(𝑊‘0)(𝑊‘1)”⟩)))
44		oveq2 7419	. . . . . . . . 9 ⊢ ((♯‘(𝑊 prefix 2)) = 2 → (0..^(♯‘(𝑊 prefix 2))) = (0..^2))
45		fzo0to2pr 13719	. . . . . . . . 9 ⊢ (0..^2) = {0, 1}
46	44, 45	eqtrdi 2788	. . . . . . . 8 ⊢ ((♯‘(𝑊 prefix 2)) = 2 → (0..^(♯‘(𝑊 prefix 2))) = {0, 1})
47	46	raleqdv 3325	. . . . . . 7 ⊢ ((♯‘(𝑊 prefix 2)) = 2 → (∀𝑖 ∈ (0..^(♯‘(𝑊 prefix 2)))((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖) ↔ ∀𝑖 ∈ {0, 1} ((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖)))
48	43, 47	anbi12d 631	. . . . . 6 ⊢ ((♯‘(𝑊 prefix 2)) = 2 → (((♯‘(𝑊 prefix 2)) = (♯‘⟨“(𝑊‘0)(𝑊‘1)”⟩) ∧ ∀𝑖 ∈ (0..^(♯‘(𝑊 prefix 2)))((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖)) ↔ (2 = (♯‘⟨“(𝑊‘0)(𝑊‘1)”⟩) ∧ ∀𝑖 ∈ {0, 1} ((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖))))
49	48	adantl 482	. . . . 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)”⟩‘𝑖))))
50	11, 42, 49	mpbir2and 711	. . . 4 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) ∧ (♯‘(𝑊 prefix 2)) = 2) → ((♯‘(𝑊 prefix 2)) = (♯‘⟨“(𝑊‘0)(𝑊‘1)”⟩) ∧ ∀𝑖 ∈ (0..^(♯‘(𝑊 prefix 2)))((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖)))
51	8, 50	mpdan 685	. . 3 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) → ((♯‘(𝑊 prefix 2)) = (♯‘⟨“(𝑊‘0)(𝑊‘1)”⟩) ∧ ∀𝑖 ∈ (0..^(♯‘(𝑊 prefix 2)))((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖)))
52		pfxcl 14629	. . . . 5 ⊢ (𝑊 ∈ Word 𝑉 → (𝑊 prefix 2) ∈ Word 𝑉)
53		s2cli 14833	. . . . 5 ⊢ ⟨“(𝑊‘0)(𝑊‘1)”⟩ ∈ Word V
54		eqwrd 14509	. . . . 5 ⊢ (((𝑊 prefix 2) ∈ Word 𝑉 ∧ ⟨“(𝑊‘0)(𝑊‘1)”⟩ ∈ Word V) → ((𝑊 prefix 2) = ⟨“(𝑊‘0)(𝑊‘1)”⟩ ↔ ((♯‘(𝑊 prefix 2)) = (♯‘⟨“(𝑊‘0)(𝑊‘1)”⟩) ∧ ∀𝑖 ∈ (0..^(♯‘(𝑊 prefix 2)))((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖))))
55	52, 53, 54	sylancl 586	. . . 4 ⊢ (𝑊 ∈ Word 𝑉 → ((𝑊 prefix 2) = ⟨“(𝑊‘0)(𝑊‘1)”⟩ ↔ ((♯‘(𝑊 prefix 2)) = (♯‘⟨“(𝑊‘0)(𝑊‘1)”⟩) ∧ ∀𝑖 ∈ (0..^(♯‘(𝑊 prefix 2)))((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖))))
56	55	adantr 481	. . 3 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) → ((𝑊 prefix 2) = ⟨“(𝑊‘0)(𝑊‘1)”⟩ ↔ ((♯‘(𝑊 prefix 2)) = (♯‘⟨“(𝑊‘0)(𝑊‘1)”⟩) ∧ ∀𝑖 ∈ (0..^(♯‘(𝑊 prefix 2)))((𝑊 prefix 2)‘𝑖) = (⟨“(𝑊‘0)(𝑊‘1)”⟩‘𝑖))))
57	51, 56	mpbird 256	. 2 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ∈ (0...(♯‘𝑊))) → (𝑊 prefix 2) = ⟨“(𝑊‘0)(𝑊‘1)”⟩)
58	7, 57	syldan 591	1 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑊)) → (𝑊 prefix 2) = ⟨“(𝑊‘0)(𝑊‘1)”⟩)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ∀wral 3061 Vcvv 3474 {cpr 4630 class class class wbr 5148 ‘cfv 6543 (class class class)co 7411 0cc0 11112 1c1 11113 < clt 11250 ≤ cle 11251 ℕcn 12214 2c2 12269 ℕ₀cn0 12474 ...cfz 13486 ..^cfzo 13629 ♯chash 14292 Word cword 14466 prefix cpfx 14622 ⟨“cs2 14794

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7727 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7858 df-1st 7977 df-2nd 7978 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-1o 8468 df-er 8705 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-card 9936 df-pnf 11252 df-mnf 11253 df-xr 11254 df-ltxr 11255 df-le 11256 df-sub 11448 df-neg 11449 df-nn 12215 df-2 12277 df-n0 12475 df-z 12561 df-uz 12825 df-fz 13487 df-fzo 13630 df-hash 14293 df-word 14467 df-concat 14523 df-s1 14548 df-substr 14593 df-pfx 14623 df-s2 14801

This theorem is referenced by: (None)

W3C validator