Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > wrdexg | Structured version Visualization version GIF version |
Description: The set of words over a set is a set. (Contributed by Mario Carneiro, 26-Feb-2016.) (Proof shortened by JJ, 18-Nov-2022.) |
Ref | Expression |
---|---|
wrdexg | ⊢ (𝑆 ∈ 𝑉 → Word 𝑆 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wrdval 13854 | . 2 ⊢ (𝑆 ∈ 𝑉 → Word 𝑆 = ∪ 𝑙 ∈ ℕ0 (𝑆 ↑m (0..^𝑙))) | |
2 | nn0ex 11890 | . . 3 ⊢ ℕ0 ∈ V | |
3 | ovexd 7177 | . . . 4 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑙 ∈ ℕ0) → (𝑆 ↑m (0..^𝑙)) ∈ V) | |
4 | 3 | ralrimiva 3182 | . . 3 ⊢ (𝑆 ∈ 𝑉 → ∀𝑙 ∈ ℕ0 (𝑆 ↑m (0..^𝑙)) ∈ V) |
5 | iunexg 7650 | . . 3 ⊢ ((ℕ0 ∈ V ∧ ∀𝑙 ∈ ℕ0 (𝑆 ↑m (0..^𝑙)) ∈ V) → ∪ 𝑙 ∈ ℕ0 (𝑆 ↑m (0..^𝑙)) ∈ V) | |
6 | 2, 4, 5 | sylancr 589 | . 2 ⊢ (𝑆 ∈ 𝑉 → ∪ 𝑙 ∈ ℕ0 (𝑆 ↑m (0..^𝑙)) ∈ V) |
7 | 1, 6 | eqeltrd 2913 | 1 ⊢ (𝑆 ∈ 𝑉 → Word 𝑆 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∈ wcel 2114 ∀wral 3138 Vcvv 3486 ∪ ciun 4905 (class class class)co 7142 ↑m cmap 8392 0cc0 10523 ℕ0cn0 11884 ..^cfzo 13023 Word cword 13851 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-rep 5176 ax-sep 5189 ax-nul 5196 ax-pow 5252 ax-pr 5316 ax-un 7447 ax-cnex 10579 ax-1cn 10581 ax-addcl 10583 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-reu 3145 df-rab 3147 df-v 3488 df-sbc 3764 df-csb 3872 df-dif 3927 df-un 3929 df-in 3931 df-ss 3940 df-pss 3942 df-nul 4280 df-if 4454 df-pw 4527 df-sn 4554 df-pr 4556 df-tp 4558 df-op 4560 df-uni 4825 df-iun 4907 df-br 5053 df-opab 5115 df-mpt 5133 df-tr 5159 df-id 5446 df-eprel 5451 df-po 5460 df-so 5461 df-fr 5500 df-we 5502 df-xp 5547 df-rel 5548 df-cnv 5549 df-co 5550 df-dm 5551 df-rn 5552 df-res 5553 df-ima 5554 df-pred 6134 df-ord 6180 df-on 6181 df-lim 6182 df-suc 6183 df-iota 6300 df-fun 6343 df-fn 6344 df-f 6345 df-f1 6346 df-fo 6347 df-f1o 6348 df-fv 6349 df-ov 7145 df-oprab 7146 df-mpo 7147 df-om 7567 df-wrecs 7933 df-recs 7994 df-rdg 8032 df-map 8394 df-nn 11625 df-n0 11885 df-word 13852 |
This theorem is referenced by: wrdexb 13862 wrdexi 13863 wrdnfi 13885 elovmpowrd 13895 elovmptnn0wrd 13896 wrd2f1tovbij 14309 frmdbas 18000 frmdplusg 18002 efgval 18826 frgp0 18869 frgpmhm 18874 vrgpf 18877 vrgpinv 18878 frgpupf 18882 frgpup1 18884 frgpup2 18885 frgpup3lem 18886 frgpnabllem1 18976 frgpnabllem2 18977 wksfval 27377 wksv 27387 wwlks 27599 clwwlk 27746 tocycval 30757 sseqval 31653 upwlksfval 44095 |
Copyright terms: Public domain | W3C validator |