![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > wrdco | Structured version Visualization version GIF version |
Description: Mapping a word by a function. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
Ref | Expression |
---|---|
wrdco | ⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ 𝑊) ∈ Word 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr 479 | . . 3 ⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → 𝐹:𝐴⟶𝐵) | |
2 | wrdf 13517 | . . . 4 ⊢ (𝑊 ∈ Word 𝐴 → 𝑊:(0..^(♯‘𝑊))⟶𝐴) | |
3 | 2 | adantr 472 | . . 3 ⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → 𝑊:(0..^(♯‘𝑊))⟶𝐴) |
4 | fco 6220 | . . 3 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑊:(0..^(♯‘𝑊))⟶𝐴) → (𝐹 ∘ 𝑊):(0..^(♯‘𝑊))⟶𝐵) | |
5 | 1, 3, 4 | syl2anc 696 | . 2 ⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ 𝑊):(0..^(♯‘𝑊))⟶𝐵) |
6 | iswrdi 13516 | . 2 ⊢ ((𝐹 ∘ 𝑊):(0..^(♯‘𝑊))⟶𝐵 → (𝐹 ∘ 𝑊) ∈ Word 𝐵) | |
7 | 5, 6 | syl 17 | 1 ⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ 𝑊) ∈ Word 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∈ wcel 2140 ∘ ccom 5271 ⟶wf 6046 ‘cfv 6050 (class class class)co 6815 0cc0 10149 ..^cfzo 12680 ♯chash 13332 Word cword 13498 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1989 ax-6 2055 ax-7 2091 ax-8 2142 ax-9 2149 ax-10 2169 ax-11 2184 ax-12 2197 ax-13 2392 ax-ext 2741 ax-rep 4924 ax-sep 4934 ax-nul 4942 ax-pow 4993 ax-pr 5056 ax-un 7116 ax-cnex 10205 ax-resscn 10206 ax-1cn 10207 ax-icn 10208 ax-addcl 10209 ax-addrcl 10210 ax-mulcl 10211 ax-mulrcl 10212 ax-mulcom 10213 ax-addass 10214 ax-mulass 10215 ax-distr 10216 ax-i2m1 10217 ax-1ne0 10218 ax-1rid 10219 ax-rnegex 10220 ax-rrecex 10221 ax-cnre 10222 ax-pre-lttri 10223 ax-pre-lttrn 10224 ax-pre-ltadd 10225 ax-pre-mulgt0 10226 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2048 df-eu 2612 df-mo 2613 df-clab 2748 df-cleq 2754 df-clel 2757 df-nfc 2892 df-ne 2934 df-nel 3037 df-ral 3056 df-rex 3057 df-reu 3058 df-rab 3060 df-v 3343 df-sbc 3578 df-csb 3676 df-dif 3719 df-un 3721 df-in 3723 df-ss 3730 df-pss 3732 df-nul 4060 df-if 4232 df-pw 4305 df-sn 4323 df-pr 4325 df-tp 4327 df-op 4329 df-uni 4590 df-int 4629 df-iun 4675 df-br 4806 df-opab 4866 df-mpt 4883 df-tr 4906 df-id 5175 df-eprel 5180 df-po 5188 df-so 5189 df-fr 5226 df-we 5228 df-xp 5273 df-rel 5274 df-cnv 5275 df-co 5276 df-dm 5277 df-rn 5278 df-res 5279 df-ima 5280 df-pred 5842 df-ord 5888 df-on 5889 df-lim 5890 df-suc 5891 df-iota 6013 df-fun 6052 df-fn 6053 df-f 6054 df-f1 6055 df-fo 6056 df-f1o 6057 df-fv 6058 df-riota 6776 df-ov 6818 df-oprab 6819 df-mpt2 6820 df-om 7233 df-1st 7335 df-2nd 7336 df-wrecs 7578 df-recs 7639 df-rdg 7677 df-1o 7731 df-er 7914 df-en 8125 df-dom 8126 df-sdom 8127 df-fin 8128 df-card 8976 df-pnf 10289 df-mnf 10290 df-xr 10291 df-ltxr 10292 df-le 10293 df-sub 10481 df-neg 10482 df-nn 11234 df-n0 11506 df-z 11591 df-uz 11901 df-fz 12541 df-fzo 12681 df-hash 13333 df-word 13506 |
This theorem is referenced by: cshco 13803 swrdco 13804 frmdgsum 17621 frmdss2 17622 frmdup1 17623 frmdup3lem 17625 efginvrel2 18361 efginvrel1 18362 frgp0 18394 frgpinv 18398 frgpuplem 18406 frgpupf 18407 frgpup1 18409 frgpup3lem 18411 mrsubff 31738 mrsubccat 31744 |
Copyright terms: Public domain | W3C validator |