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 ⊢ S ∈ V → Word S = ⋃ l ∈ ℕ 0 S 0 ..^ l

Proof

Step Hyp Ref Expression
1 eliun ⊢ w ∈ ⋃ l ∈ ℕ 0 S 0 ..^ l ↔ ∃ l ∈ ℕ 0 w ∈ S 0 ..^ l
2 ovex ⊢ 0 ..^ l ∈ V
3 elmapg ⊢ S ∈ V ∧ 0 ..^ l ∈ V → w ∈ S 0 ..^ l ↔ w : 0 ..^ l ⟶ S
4 2 3 mpan2 ⊢ S ∈ V → w ∈ S 0 ..^ l ↔ w : 0 ..^ l ⟶ S
5 4 rexbidv ⊢ S ∈ V → ∃ l ∈ ℕ 0 w ∈ S 0 ..^ l ↔ ∃ l ∈ ℕ 0 w : 0 ..^ l ⟶ S
6 1 5 syl5bb ⊢ S ∈ V → w ∈ ⋃ l ∈ ℕ 0 S 0 ..^ l ↔ ∃ l ∈ ℕ 0 w : 0 ..^ l ⟶ S
7 6 abbi2dv ⊢ S ∈ V → ⋃ l ∈ ℕ 0 S 0 ..^ l = w | ∃ l ∈ ℕ 0 w : 0 ..^ l ⟶ S
8 df-word ⊢ Word S = w | ∃ l ∈ ℕ 0 w : 0 ..^ l ⟶ S
9 7 8 syl6reqr ⊢ S ∈ V → Word S = ⋃ l ∈ ℕ 0 S 0 ..^ l