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