This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑊 ∈ 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 ..^ 𝑙 ) ⟶ 𝑆 )