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	⊢ ( 𝑊 ∈ Word 𝑆 ↔ ∃ 𝑙 ∈ ℕ0 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		df-word	⊢ Word 𝑆 = { 𝑤 ∣ ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 }
2	1	eleq2i	⊢ ( 𝑊 ∈ Word 𝑆 ↔ 𝑊 ∈ { 𝑤 ∣ ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 } )
3		ovex	⊢ ( 0 ..^ 𝑙 ) ∈ V
4		fex	⊢ ( ( 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 ∧ ( 0 ..^ 𝑙 ) ∈ V ) → 𝑊 ∈ V )
5	3 4	mpan2	⊢ ( 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 → 𝑊 ∈ V )
6	5	rexlimivw	⊢ ( ∃ 𝑙 ∈ ℕ0 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 → 𝑊 ∈ V )
7		feq1	⊢ ( 𝑤 = 𝑊 → ( 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 ↔ 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 ) )
8	7	rexbidv	⊢ ( 𝑤 = 𝑊 → ( ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 ↔ ∃ 𝑙 ∈ ℕ0 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 ) )
9	6 8	elab3	⊢ ( 𝑊 ∈ { 𝑤 ∣ ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 } ↔ ∃ 𝑙 ∈ ℕ0 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 )
10	2 9	bitri	⊢ ( 𝑊 ∈ Word 𝑆 ↔ ∃ 𝑙 ∈ ℕ0 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 )