This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ..^ 𝑙 ) ) )