![]() |
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.) |
Ref | Expression |
---|---|
wrdexg | ⊢ (𝑆 ∈ 𝑉 → Word 𝑆 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wrdval 13576 | . 2 ⊢ (𝑆 ∈ 𝑉 → Word 𝑆 = ∪ 𝑙 ∈ ℕ0 (𝑆 ↑𝑚 (0..^𝑙))) | |
2 | mapsspw 8157 | . . . . . 6 ⊢ (𝑆 ↑𝑚 (0..^𝑙)) ⊆ 𝒫 ((0..^𝑙) × 𝑆) | |
3 | elfzoelz 12764 | . . . . . . . . 9 ⊢ (𝑠 ∈ (0..^𝑙) → 𝑠 ∈ ℤ) | |
4 | 3 | ssriv 3830 | . . . . . . . 8 ⊢ (0..^𝑙) ⊆ ℤ |
5 | xpss1 5360 | . . . . . . . 8 ⊢ ((0..^𝑙) ⊆ ℤ → ((0..^𝑙) × 𝑆) ⊆ (ℤ × 𝑆)) | |
6 | 4, 5 | ax-mp 5 | . . . . . . 7 ⊢ ((0..^𝑙) × 𝑆) ⊆ (ℤ × 𝑆) |
7 | sspwb 5137 | . . . . . . 7 ⊢ (((0..^𝑙) × 𝑆) ⊆ (ℤ × 𝑆) ↔ 𝒫 ((0..^𝑙) × 𝑆) ⊆ 𝒫 (ℤ × 𝑆)) | |
8 | 6, 7 | mpbi 222 | . . . . . 6 ⊢ 𝒫 ((0..^𝑙) × 𝑆) ⊆ 𝒫 (ℤ × 𝑆) |
9 | 2, 8 | sstri 3835 | . . . . 5 ⊢ (𝑆 ↑𝑚 (0..^𝑙)) ⊆ 𝒫 (ℤ × 𝑆) |
10 | 9 | rgenw 3132 | . . . 4 ⊢ ∀𝑙 ∈ ℕ0 (𝑆 ↑𝑚 (0..^𝑙)) ⊆ 𝒫 (ℤ × 𝑆) |
11 | iunss 4780 | . . . 4 ⊢ (∪ 𝑙 ∈ ℕ0 (𝑆 ↑𝑚 (0..^𝑙)) ⊆ 𝒫 (ℤ × 𝑆) ↔ ∀𝑙 ∈ ℕ0 (𝑆 ↑𝑚 (0..^𝑙)) ⊆ 𝒫 (ℤ × 𝑆)) | |
12 | 10, 11 | mpbir 223 | . . 3 ⊢ ∪ 𝑙 ∈ ℕ0 (𝑆 ↑𝑚 (0..^𝑙)) ⊆ 𝒫 (ℤ × 𝑆) |
13 | zex 11712 | . . . . 5 ⊢ ℤ ∈ V | |
14 | xpexg 7219 | . . . . 5 ⊢ ((ℤ ∈ V ∧ 𝑆 ∈ 𝑉) → (ℤ × 𝑆) ∈ V) | |
15 | 13, 14 | mpan 683 | . . . 4 ⊢ (𝑆 ∈ 𝑉 → (ℤ × 𝑆) ∈ V) |
16 | 15 | pwexd 5078 | . . 3 ⊢ (𝑆 ∈ 𝑉 → 𝒫 (ℤ × 𝑆) ∈ V) |
17 | ssexg 5028 | . . 3 ⊢ ((∪ 𝑙 ∈ ℕ0 (𝑆 ↑𝑚 (0..^𝑙)) ⊆ 𝒫 (ℤ × 𝑆) ∧ 𝒫 (ℤ × 𝑆) ∈ V) → ∪ 𝑙 ∈ ℕ0 (𝑆 ↑𝑚 (0..^𝑙)) ∈ V) | |
18 | 12, 16, 17 | sylancr 583 | . 2 ⊢ (𝑆 ∈ 𝑉 → ∪ 𝑙 ∈ ℕ0 (𝑆 ↑𝑚 (0..^𝑙)) ∈ V) |
19 | 1, 18 | eqeltrd 2905 | 1 ⊢ (𝑆 ∈ 𝑉 → Word 𝑆 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2166 ∀wral 3116 Vcvv 3413 ⊆ wss 3797 𝒫 cpw 4377 ∪ ciun 4739 × cxp 5339 (class class class)co 6904 ↑𝑚 cmap 8121 0cc0 10251 ℕ0cn0 11617 ℤcz 11703 ..^cfzo 12759 Word cword 13573 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-8 2168 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2390 ax-ext 2802 ax-sep 5004 ax-nul 5012 ax-pow 5064 ax-pr 5126 ax-un 7208 ax-cnex 10307 ax-resscn 10308 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3or 1114 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2604 df-eu 2639 df-clab 2811 df-cleq 2817 df-clel 2820 df-nfc 2957 df-ne 2999 df-ral 3121 df-rex 3122 df-rab 3125 df-v 3415 df-sbc 3662 df-csb 3757 df-dif 3800 df-un 3802 df-in 3804 df-ss 3811 df-nul 4144 df-if 4306 df-pw 4379 df-sn 4397 df-pr 4399 df-op 4403 df-uni 4658 df-iun 4741 df-br 4873 df-opab 4935 df-mpt 4952 df-id 5249 df-xp 5347 df-rel 5348 df-cnv 5349 df-co 5350 df-dm 5351 df-rn 5352 df-res 5353 df-ima 5354 df-iota 6085 df-fun 6124 df-fn 6125 df-f 6126 df-fv 6130 df-ov 6907 df-oprab 6908 df-mpt2 6909 df-1st 7427 df-2nd 7428 df-map 8123 df-pm 8124 df-neg 10587 df-z 11704 df-uz 11968 df-fz 12619 df-fzo 12760 df-word 13574 |
This theorem is referenced by: wrdexb 13584 wrdexi 13585 wrdnfi 13607 elovmpt2wrd 13617 elovmptnn0wrd 13618 wrd2f1tovbij 14081 frmdbas 17742 frmdplusg 17744 vrmdfval 17746 efgval 18480 frgp0 18525 frgpmhm 18530 vrgpf 18533 vrgpinv 18534 frgpupf 18538 frgpup1 18540 frgpup2 18541 frgpup3lem 18542 frgpnabllem1 18628 frgpnabllem2 18629 ablfaclem1 18837 israg 26008 wksfval 26906 wksv 26916 wwlks 27133 clwwlk 27311 sseqval 30995 upwlksfval 42562 |
Copyright terms: Public domain | W3C validator |