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 syl5bb ( 𝑆𝑉 → ( 𝑤 𝑙 ∈ ℕ0 ( 𝑆m ( 0 ..^ 𝑙 ) ) ↔ ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 ) )
8 7 abbi2dv ( 𝑆𝑉 𝑙 ∈ ℕ0 ( 𝑆m ( 0 ..^ 𝑙 ) ) = { 𝑤 ∣ ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 } )
9 1 8 eqtr4id ( 𝑆𝑉 → Word 𝑆 = 𝑙 ∈ ℕ0 ( 𝑆m ( 0 ..^ 𝑙 ) ) )