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 df-word ⊢ Word S = w | ∃ l ∈ ℕ 0 w : 0 ..^ l ⟶ S
2 eliun ⊢ w ∈ ⋃ l ∈ ℕ 0 S 0 ..^ l ↔ ∃ l ∈ ℕ 0 w ∈ S 0 ..^ l
3 ovex ⊢ 0 ..^ l ∈ V
4 elmapg ⊢ S ∈ V ∧ 0 ..^ l ∈ V → w ∈ S 0 ..^ l ↔ w : 0 ..^ l ⟶ S
5 3 4 mpan2 ⊢ S ∈ V → w ∈ S 0 ..^ l ↔ w : 0 ..^ l ⟶ S
6 5 rexbidv ⊢ S ∈ V → ∃ l ∈ ℕ 0 w ∈ S 0 ..^ l ↔ ∃ l ∈ ℕ 0 w : 0 ..^ l ⟶ S
7 2 6 bitrid ⊢ S ∈ V → w ∈ ⋃ l ∈ ℕ 0 S 0 ..^ l ↔ ∃ l ∈ ℕ 0 w : 0 ..^ l ⟶ S
8 7 eqabdv ⊢ S ∈ V → ⋃ l ∈ ℕ 0 S 0 ..^ l = w | ∃ l ∈ ℕ 0 w : 0 ..^ l ⟶ S
9 1 8 eqtr4id ⊢ S ∈ V → Word S = ⋃ l ∈ ℕ 0 S 0 ..^ l