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 13972

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 13969	. 2 ⊢ (𝑊 ∈ Word 𝑆 ↔ ∃𝑙 ∈ ℕ₀ 𝑊:(0..^𝑙)⟶𝑆)
2		simpr 488	. . . 4 ⊢ ((𝑙 ∈ ℕ₀ ∧ 𝑊:(0..^𝑙)⟶𝑆) → 𝑊:(0..^𝑙)⟶𝑆)
3		fnfzo0hash 13912	. . . . . 6 ⊢ ((𝑙 ∈ ℕ₀ ∧ 𝑊:(0..^𝑙)⟶𝑆) → (♯‘𝑊) = 𝑙)
4	3	oveq2d 7198	. . . . 5 ⊢ ((𝑙 ∈ ℕ₀ ∧ 𝑊:(0..^𝑙)⟶𝑆) → (0..^(♯‘𝑊)) = (0..^𝑙))
5	4	feq2d 6500	. . . 4 ⊢ ((𝑙 ∈ ℕ₀ ∧ 𝑊:(0..^𝑙)⟶𝑆) → (𝑊:(0..^(♯‘𝑊))⟶𝑆 ↔ 𝑊:(0..^𝑙)⟶𝑆))
6	2, 5	mpbird 260	. . 3 ⊢ ((𝑙 ∈ ℕ₀ ∧ 𝑊:(0..^𝑙)⟶𝑆) → 𝑊:(0..^(♯‘𝑊))⟶𝑆)
7	6	rexlimiva 3192	. 2 ⊢ (∃𝑙 ∈ ℕ₀ 𝑊:(0..^𝑙)⟶𝑆 → 𝑊:(0..^(♯‘𝑊))⟶𝑆)
8	1, 7	sylbi 220	1 ⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0..^(♯‘𝑊))⟶𝑆)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 ∈ wcel 2114 ∃wrex 3055 ⟶wf 6345 ‘cfv 6349 (class class class)co 7182 0cc0 10627 ℕ₀cn0 11988 ..^cfzo 13136 ♯chash 13794 Word cword 13967

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2711 ax-rep 5164 ax-sep 5177 ax-nul 5184 ax-pow 5242 ax-pr 5306 ax-un 7491 ax-cnex 10683 ax-resscn 10684 ax-1cn 10685 ax-icn 10686 ax-addcl 10687 ax-addrcl 10688 ax-mulcl 10689 ax-mulrcl 10690 ax-mulcom 10691 ax-addass 10692 ax-mulass 10693 ax-distr 10694 ax-i2m1 10695 ax-1ne0 10696 ax-1rid 10697 ax-rnegex 10698 ax-rrecex 10699 ax-cnre 10700 ax-pre-lttri 10701 ax-pre-lttrn 10702 ax-pre-ltadd 10703 ax-pre-mulgt0 10704

This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2541 df-eu 2571 df-clab 2718 df-cleq 2731 df-clel 2812 df-nfc 2882 df-ne 2936 df-nel 3040 df-ral 3059 df-rex 3060 df-reu 3061 df-rab 3063 df-v 3402 df-sbc 3686 df-csb 3801 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-pss 3872 df-nul 4222 df-if 4425 df-pw 4500 df-sn 4527 df-pr 4529 df-tp 4531 df-op 4533 df-uni 4807 df-int 4847 df-iun 4893 df-br 5041 df-opab 5103 df-mpt 5121 df-tr 5147 df-id 5439 df-eprel 5444 df-po 5452 df-so 5453 df-fr 5493 df-we 5495 df-xp 5541 df-rel 5542 df-cnv 5543 df-co 5544 df-dm 5545 df-rn 5546 df-res 5547 df-ima 5548 df-pred 6139 df-ord 6185 df-on 6186 df-lim 6187 df-suc 6188 df-iota 6307 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 df-fv 6357 df-riota 7139 df-ov 7185 df-oprab 7186 df-mpo 7187 df-om 7612 df-1st 7726 df-2nd 7727 df-wrecs 7988 df-recs 8049 df-rdg 8087 df-1o 8143 df-er 8332 df-en 8568 df-dom 8569 df-sdom 8570 df-fin 8571 df-card 9453 df-pnf 10767 df-mnf 10768 df-xr 10769 df-ltxr 10770 df-le 10771 df-sub 10962 df-neg 10963 df-nn 11729 df-n0 11989 df-z 12075 df-uz 12337 df-fz 12994 df-fzo 13137 df-hash 13795 df-word 13968

This theorem is referenced by: iswrdb 13973 wrddm 13974 wrdsymbcl 13980 wrdfn 13981 wrdffz 13988 0wrd0 13993 wrdsymb 13995 wrdnval 13998 wrdred1 14013 wrdred1hash 14014 ccatcl 14027 ccatalpha 14048 s1dm 14063 swrdcl 14108 swrdf 14113 swrdwrdsymb 14125 pfxres 14142 cats1un 14184 revcl 14224 revlen 14225 revrev 14230 repsdf2 14241 cshwf 14263 cshinj 14274 wrdco 14294 lenco 14295 revco 14297 ccatco 14298 lswco 14302 s2dm 14353 wwlktovf 14421 ofccat 14430 gsumwsubmcl 18129 gsumsgrpccat 18132 gsumccatOLD 18133 gsumwmhm 18138 frmdss2 18156 symgtrinv 18730 psgnunilem5 18752 psgnunilem2 18753 psgnunilem3 18754 efginvrel1 18984 efgsf 18985 efgsrel 18990 efgs1b 18992 efgredlemf 18997 efgredlemd 19000 efgredlemc 19001 efgredlem 19003 frgpup3lem 19033 pgpfaclem1 19334 ablfaclem2 19339 ablfaclem3 19340 ablfac2 19342 dchrptlem1 26012 dchrptlem2 26013 trgcgrg 26473 tgcgr4 26489 wrdupgr 27042 wrdumgr 27054 vdegp1ai 27490 vdegp1bi 27491 wlkres 27624 wlkp1 27635 wlkdlem1 27636 trlf1 27652 trlreslem 27653 upgrwlkdvdelem 27689 pthdlem1 27719 pthdlem2lem 27720 uspgrn2crct 27758 wlkiswwlks2lem3 27821 wlkiswwlksupgr2 27827 clwlkclwwlklem2a 27947 clwlkclwwlklem2 27949 1wlkdlem1 28086 wlk2v2e 28106 eucrctshift 28192 konigsbergssiedgw 28199 wrdfd 30797 wrdres 30798 pfxf1 30803 s3f1 30808 ccatf1 30810 swrdrn3 30814 cycpmcl 30972 tocyc01 30974 cycpmco2rn 30981 cycpmrn 30999 tocyccntz 31000 cycpmconjslem2 31011 sseqf 31941 fiblem 31947 ofcccat 32104 signstcl 32126 signstf 32127 signstfvn 32130 signsvtn0 32131 signstres 32136 signsvtp 32144 signsvtn 32145 signsvfpn 32146 signsvfnn 32147 signshf 32149 revwlk 32669 mvrsfpw 33051 frlmfzowrdb 39857 amgm2d 41396 amgm3d 41397 amgm4d 41398 lswn0 44477 amgmw2d 46008

W3C validator