Theorem wrdval

Description: Value of the set of words over a set. (Contributed by Stefan O'Rear, 10-Aug-2015) (Revised by Mario Carneiro, 26-Feb-2016)

	Ref	Expression
Assertion	wrdval	⊢ ( 𝑆 ∈ 𝑉 → Word 𝑆 = ∪ 𝑙 ∈ ℕ0 ( 𝑆 ↑m ( 0 ..^ 𝑙 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eliun	⊢ ( 𝑤 ∈ ∪ 𝑙 ∈ ℕ0 ( 𝑆 ↑m ( 0 ..^ 𝑙 ) ) ↔ ∃ 𝑙 ∈ ℕ0 𝑤 ∈ ( 𝑆 ↑m ( 0 ..^ 𝑙 ) ) )
2		ovex	⊢ ( 0 ..^ 𝑙 ) ∈ V
3		elmapg	⊢ ( ( 𝑆 ∈ 𝑉 ∧ ( 0 ..^ 𝑙 ) ∈ V ) → ( 𝑤 ∈ ( 𝑆 ↑m ( 0 ..^ 𝑙 ) ) ↔ 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 ) )
4	2 3	mpan2	⊢ ( 𝑆 ∈ 𝑉 → ( 𝑤 ∈ ( 𝑆 ↑m ( 0 ..^ 𝑙 ) ) ↔ 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 ) )
5	4	rexbidv	⊢ ( 𝑆 ∈ 𝑉 → ( ∃ 𝑙 ∈ ℕ0 𝑤 ∈ ( 𝑆 ↑m ( 0 ..^ 𝑙 ) ) ↔ ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 ) )
6	1 5	syl5bb	⊢ ( 𝑆 ∈ 𝑉 → ( 𝑤 ∈ ∪ 𝑙 ∈ ℕ0 ( 𝑆 ↑m ( 0 ..^ 𝑙 ) ) ↔ ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 ) )
7	6	abbi2dv	⊢ ( 𝑆 ∈ 𝑉 → ∪ 𝑙 ∈ ℕ0 ( 𝑆 ↑m ( 0 ..^ 𝑙 ) ) = { 𝑤 ∣ ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 } )
8		df-word	⊢ Word 𝑆 = { 𝑤 ∣ ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 }
9	7 8	syl6reqr	⊢ ( 𝑆 ∈ 𝑉 → Word 𝑆 = ∪ 𝑙 ∈ ℕ0 ( 𝑆 ↑m ( 0 ..^ 𝑙 ) ) )