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		df-word	⊢ Word 𝑆 = { 𝑤 ∣ ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 }
2		eliun	⊢ ( 𝑤 ∈ ∪ 𝑙 ∈ ℕ0 ( 𝑆 ↑m ( 0 ..^ 𝑙 ) ) ↔ ∃ 𝑙 ∈ ℕ0 𝑤 ∈ ( 𝑆 ↑m ( 0 ..^ 𝑙 ) ) )
3		ovex	⊢ ( 0 ..^ 𝑙 ) ∈ V
4		elmapg	⊢ ( ( 𝑆 ∈ 𝑉 ∧ ( 0 ..^ 𝑙 ) ∈ V ) → ( 𝑤 ∈ ( 𝑆 ↑m ( 0 ..^ 𝑙 ) ) ↔ 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 ) )
5	3 4	mpan2	⊢ ( 𝑆 ∈ 𝑉 → ( 𝑤 ∈ ( 𝑆 ↑m ( 0 ..^ 𝑙 ) ) ↔ 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 ) )
6	5	rexbidv	⊢ ( 𝑆 ∈ 𝑉 → ( ∃ 𝑙 ∈ ℕ0 𝑤 ∈ ( 𝑆 ↑m ( 0 ..^ 𝑙 ) ) ↔ ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 ) )
7	2 6	bitrid	⊢ ( 𝑆 ∈ 𝑉 → ( 𝑤 ∈ ∪ 𝑙 ∈ ℕ0 ( 𝑆 ↑m ( 0 ..^ 𝑙 ) ) ↔ ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 ) )
8	7	eqabdv	⊢ ( 𝑆 ∈ 𝑉 → ∪ 𝑙 ∈ ℕ0 ( 𝑆 ↑m ( 0 ..^ 𝑙 ) ) = { 𝑤 ∣ ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 } )
9	1 8	eqtr4id	⊢ ( 𝑆 ∈ 𝑉 → Word 𝑆 = ∪ 𝑙 ∈ ℕ0 ( 𝑆 ↑m ( 0 ..^ 𝑙 ) ) )