# Metamath Proof Explorer

## Theorem iswrd

Description: Property of being a word over a set with an existential quantifier over the length. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 26-Feb-2016) (Proof shortened by AV, 13-May-2020)

Ref Expression
Assertion iswrd ${⊢}{W}\in \mathrm{Word}{S}↔\exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{W}:\left(0..^{l}\right)⟶{S}$

### Proof

Step Hyp Ref Expression
1 df-word ${⊢}\mathrm{Word}{S}=\left\{{w}|\exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{w}:\left(0..^{l}\right)⟶{S}\right\}$
2 1 eleq2i ${⊢}{W}\in \mathrm{Word}{S}↔{W}\in \left\{{w}|\exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{w}:\left(0..^{l}\right)⟶{S}\right\}$
3 ovex ${⊢}\left(0..^{l}\right)\in \mathrm{V}$
4 fex ${⊢}\left({W}:\left(0..^{l}\right)⟶{S}\wedge \left(0..^{l}\right)\in \mathrm{V}\right)\to {W}\in \mathrm{V}$
5 3 4 mpan2 ${⊢}{W}:\left(0..^{l}\right)⟶{S}\to {W}\in \mathrm{V}$
6 5 rexlimivw ${⊢}\exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{W}:\left(0..^{l}\right)⟶{S}\to {W}\in \mathrm{V}$
7 feq1 ${⊢}{w}={W}\to \left({w}:\left(0..^{l}\right)⟶{S}↔{W}:\left(0..^{l}\right)⟶{S}\right)$
8 7 rexbidv ${⊢}{w}={W}\to \left(\exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{w}:\left(0..^{l}\right)⟶{S}↔\exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{W}:\left(0..^{l}\right)⟶{S}\right)$
9 6 8 elab3 ${⊢}{W}\in \left\{{w}|\exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{w}:\left(0..^{l}\right)⟶{S}\right\}↔\exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{W}:\left(0..^{l}\right)⟶{S}$
10 2 9 bitri ${⊢}{W}\in \mathrm{Word}{S}↔\exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{W}:\left(0..^{l}\right)⟶{S}$