wrdf - Metamath Proof Explorer

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

Theorem wrdf 14231

Description: A word is a zero-based sequence with a recoverable upper limit. (Contributed by Stefan O'Rear, 15-Aug-2015.)

**Assertion**
Ref	Expression
wrdf	⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0..^(♯‘𝑊))⟶𝑆)

Proof of Theorem wrdf Dummy variable 𝑙 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		iswrd 14228	. 2 ⊢ (𝑊 ∈ Word 𝑆 ↔ ∃𝑙 ∈ ℕ₀ 𝑊:(0..^𝑙)⟶𝑆)
2		simpr 485	. . . 4 ⊢ ((𝑙 ∈ ℕ₀ ∧ 𝑊:(0..^𝑙)⟶𝑆) → 𝑊:(0..^𝑙)⟶𝑆)
3		fnfzo0hash 14171	. . . . . 6 ⊢ ((𝑙 ∈ ℕ₀ ∧ 𝑊:(0..^𝑙)⟶𝑆) → (♯‘𝑊) = 𝑙)
4	3	oveq2d 7300	. . . . 5 ⊢ ((𝑙 ∈ ℕ₀ ∧ 𝑊:(0..^𝑙)⟶𝑆) → (0..^(♯‘𝑊)) = (0..^𝑙))
5	4	feq2d 6595	. . . 4 ⊢ ((𝑙 ∈ ℕ₀ ∧ 𝑊:(0..^𝑙)⟶𝑆) → (𝑊:(0..^(♯‘𝑊))⟶𝑆 ↔ 𝑊:(0..^𝑙)⟶𝑆))
6	2, 5	mpbird 256	. . 3 ⊢ ((𝑙 ∈ ℕ₀ ∧ 𝑊:(0..^𝑙)⟶𝑆) → 𝑊:(0..^(♯‘𝑊))⟶𝑆)
7	6	rexlimiva 3211	. 2 ⊢ (∃𝑙 ∈ ℕ₀ 𝑊:(0..^𝑙)⟶𝑆 → 𝑊:(0..^(♯‘𝑊))⟶𝑆)
8	1, 7	sylbi 216	1 ⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0..^(♯‘𝑊))⟶𝑆)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2107 ∃wrex 3066 ⟶wf 6433 ‘cfv 6437 (class class class)co 7284 0cc0 10880 ℕ₀cn0 12242 ..^cfzo 13391 ♯chash 14053 Word cword 14226

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2710 ax-rep 5210 ax-sep 5224 ax-nul 5231 ax-pow 5289 ax-pr 5353 ax-un 7597 ax-cnex 10936 ax-resscn 10937 ax-1cn 10938 ax-icn 10939 ax-addcl 10940 ax-addrcl 10941 ax-mulcl 10942 ax-mulrcl 10943 ax-mulcom 10944 ax-addass 10945 ax-mulass 10946 ax-distr 10947 ax-i2m1 10948 ax-1ne0 10949 ax-1rid 10950 ax-rnegex 10951 ax-rrecex 10952 ax-cnre 10953 ax-pre-lttri 10954 ax-pre-lttrn 10955 ax-pre-ltadd 10956 ax-pre-mulgt0 10957

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-ne 2945 df-nel 3051 df-ral 3070 df-rex 3071 df-reu 3073 df-rab 3074 df-v 3435 df-sbc 3718 df-csb 3834 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-pss 3907 df-nul 4258 df-if 4461 df-pw 4536 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4841 df-int 4881 df-iun 4927 df-br 5076 df-opab 5138 df-mpt 5159 df-tr 5193 df-id 5490 df-eprel 5496 df-po 5504 df-so 5505 df-fr 5545 df-we 5547 df-xp 5596 df-rel 5597 df-cnv 5598 df-co 5599 df-dm 5600 df-rn 5601 df-res 5602 df-ima 5603 df-pred 6206 df-ord 6273 df-on 6274 df-lim 6275 df-suc 6276 df-iota 6395 df-fun 6439 df-fn 6440 df-f 6441 df-f1 6442 df-fo 6443 df-f1o 6444 df-fv 6445 df-riota 7241 df-ov 7287 df-oprab 7288 df-mpo 7289 df-om 7722 df-1st 7840 df-2nd 7841 df-frecs 8106 df-wrecs 8137 df-recs 8211 df-rdg 8250 df-1o 8306 df-er 8507 df-en 8743 df-dom 8744 df-sdom 8745 df-fin 8746 df-card 9706 df-pnf 11020 df-mnf 11021 df-xr 11022 df-ltxr 11023 df-le 11024 df-sub 11216 df-neg 11217 df-nn 11983 df-n0 12243 df-z 12329 df-uz 12592 df-fz 13249 df-fzo 13392 df-hash 14054 df-word 14227

This theorem is referenced by: iswrdb 14232 wrddm 14233 wrdsymbcl 14239 wrdfn 14240 wrdffz 14247 0wrd0 14252 wrdsymb 14254 wrdnval 14257 wrdred1 14272 wrdred1hash 14273 ccatcl 14286 ccatalpha 14307 s1dm 14322 swrdcl 14367 swrdf 14372 swrdwrdsymb 14384 pfxres 14401 cats1un 14443 revcl 14483 revlen 14484 revrev 14489 repsdf2 14500 cshwf 14522 cshinj 14533 wrdco 14553 lenco 14554 revco 14556 ccatco 14557 lswco 14561 s2dm 14612 wwlktovf 14680 ofccat 14689 gsumwsubmcl 18484 gsumsgrpccat 18487 gsumccatOLD 18488 gsumwmhm 18493 frmdss2 18511 symgtrinv 19089 psgnunilem5 19111 psgnunilem2 19112 psgnunilem3 19113 efginvrel1 19343 efgsf 19344 efgsrel 19349 efgs1b 19351 efgredlemf 19356 efgredlemd 19359 efgredlemc 19360 efgredlem 19362 frgpup3lem 19392 pgpfaclem1 19693 ablfaclem2 19698 ablfaclem3 19699 ablfac2 19701 dchrptlem1 26421 dchrptlem2 26422 trgcgrg 26885 tgcgr4 26901 wrdupgr 27464 wrdumgr 27476 vdegp1ai 27912 vdegp1bi 27913 wlkres 28047 wlkp1 28058 wlkdlem1 28059 trlf1 28075 trlreslem 28076 upgrwlkdvdelem 28113 pthdlem1 28143 pthdlem2lem 28144 uspgrn2crct 28182 wlkiswwlks2lem3 28245 wlkiswwlksupgr2 28251 clwlkclwwlklem2a 28371 clwlkclwwlklem2 28373 1wlkdlem1 28510 wlk2v2e 28530 eucrctshift 28616 konigsbergssiedgw 28623 wrdfd 31219 wrdres 31220 pfxf1 31225 s3f1 31230 ccatf1 31232 swrdrn3 31236 cycpmcl 31392 tocyc01 31394 cycpmco2rn 31401 cycpmrn 31419 tocyccntz 31420 cycpmconjslem2 31431 sseqf 32368 fiblem 32374 ofcccat 32531 signstcl 32553 signstf 32554 signstfvn 32557 signsvtn0 32558 signstres 32563 signsvtp 32571 signsvtn 32572 signsvfpn 32573 signsvfnn 32574 signshf 32576 revwlk 33095 mvrsfpw 33477 frlmfzowrdb 40242 amgm2d 41816 amgm3d 41817 amgm4d 41818 lswn0 44907 amgmw2d 46519

W3C validator