Theorem wrdexg

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
Assertion	wrdexg	⊢ ( 𝑆 ∈ 𝑉 → Word 𝑆 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		wrdval	⊢ ( 𝑆 ∈ 𝑉 → Word 𝑆 = ∪ 𝑙 ∈ ℕ0 ( 𝑆 ↑m ( 0 ..^ 𝑙 ) ) )
2		nn0ex	⊢ ℕ0 ∈ V
3		ovexd	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑙 ∈ ℕ0 ) → ( 𝑆 ↑m ( 0 ..^ 𝑙 ) ) ∈ V )
4	3	ralrimiva	⊢ ( 𝑆 ∈ 𝑉 → ∀ 𝑙 ∈ ℕ0 ( 𝑆 ↑m ( 0 ..^ 𝑙 ) ) ∈ V )
5		iunexg	⊢ ( ( ℕ0 ∈ V ∧ ∀ 𝑙 ∈ ℕ0 ( 𝑆 ↑m ( 0 ..^ 𝑙 ) ) ∈ V ) → ∪ 𝑙 ∈ ℕ0 ( 𝑆 ↑m ( 0 ..^ 𝑙 ) ) ∈ V )
6	2 4 5	sylancr	⊢ ( 𝑆 ∈ 𝑉 → ∪ 𝑙 ∈ ℕ0 ( 𝑆 ↑m ( 0 ..^ 𝑙 ) ) ∈ V )
7	1 6	eqeltrd	⊢ ( 𝑆 ∈ 𝑉 → Word 𝑆 ∈ V )