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 ⊢ W ∈ Word S ↔ ∃ l ∈ ℕ 0 W : 0 ..^ l ⟶ S

Proof

Step Hyp Ref Expression
1 df-word ⊢ Word S = w | ∃ l ∈ ℕ 0 w : 0 ..^ l ⟶ S
2 1 eleq2i ⊢ W ∈ Word S ↔ W ∈ w | ∃ l ∈ ℕ 0 w : 0 ..^ l ⟶ S
3 ovex ⊢ 0 ..^ l ∈ V
4 fex ⊢ W : 0 ..^ l ⟶ S ∧ 0 ..^ l ∈ V → W ∈ V
5 3 4 mpan2 ⊢ W : 0 ..^ l ⟶ S → W ∈ V
6 5 rexlimivw ⊢ ∃ l ∈ ℕ 0 W : 0 ..^ l ⟶ S → W ∈ V
7 feq1 ⊢ w = W → w : 0 ..^ l ⟶ S ↔ W : 0 ..^ l ⟶ S
8 7 rexbidv ⊢ w = W → ∃ l ∈ ℕ 0 w : 0 ..^ l ⟶ S ↔ ∃ l ∈ ℕ 0 W : 0 ..^ l ⟶ S
9 6 8 elab3 ⊢ W ∈ w | ∃ l ∈ ℕ 0 w : 0 ..^ l ⟶ S ↔ ∃ l ∈ ℕ 0 W : 0 ..^ l ⟶ S
10 2 9 bitri ⊢ W ∈ Word S ↔ ∃ l ∈ ℕ 0 W : 0 ..^ l ⟶ S