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\leftrightarrow \exists l\in {\mathbb{N}}_{0}W:\left(0..^l\right)⟶S$$

Proof

Step	Hyp	Ref	Expression
1		df-word	$$⊢\mathrm{Word}S=\left\{w|\exists l\in {\mathbb{N}}_{0}w:\left(0..^l\right)⟶S\right\}$$
2	1	eleq2i	$$⊢W\in \mathrm{Word}S\leftrightarrow W\in \left\{w|\exists l\in {\mathbb{N}}_{0}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 {\mathbb{N}}_{0}W:\left(0..^l\right)⟶S\to W\in \mathrm{V}$$
7		feq1	$$⊢w=W\to \left(w:\left(0..^l\right)⟶S\leftrightarrow W:\left(0..^l\right)⟶S\right)$$
8	7	rexbidv	$$⊢w=W\to \left(\exists l\in {\mathbb{N}}_{0}w:\left(0..^l\right)⟶S\leftrightarrow \exists l\in {\mathbb{N}}_{0}W:\left(0..^l\right)⟶S\right)$$
9	6 8	elab3	$$⊢W\in \left\{w|\exists l\in {\mathbb{N}}_{0}w:\left(0..^l\right)⟶S\right\}\leftrightarrow \exists l\in {\mathbb{N}}_{0}W:\left(0..^l\right)⟶S$$
10	2 9	bitri	$$⊢W\in \mathrm{Word}S\leftrightarrow \exists l\in {\mathbb{N}}_{0}W:\left(0..^l\right)⟶S$$