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

Metamath Proof Explorer

Theorem iswrdi

Description: A zero-based sequence is a word. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion iswrdi ( 𝑊 : ( 0 ..^ 𝐿 ) ⟶ 𝑆 → 𝑊 ∈ Word 𝑆 )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑙 = 𝐿 → ( 0 ..^ 𝑙 ) = ( 0 ..^ 𝐿 ) )
2 1 feq2d ⊢ ( 𝑙 = 𝐿 → ( 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 ↔ 𝑊 : ( 0 ..^ 𝐿 ) ⟶ 𝑆 ) )
3 2 rspcev ⊢ ( ( 𝐿 ∈ ℕ0 ∧ 𝑊 : ( 0 ..^ 𝐿 ) ⟶ 𝑆 ) → ∃ 𝑙 ∈ ℕ0 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 )
4 0nn0 ⊢ 0 ∈ ℕ0
5 fzo0n0 ⊢ ( ( 0 ..^ 𝐿 ) ≠ ∅ ↔ 𝐿 ∈ ℕ )
6 nnnn0 ⊢ ( 𝐿 ∈ ℕ → 𝐿 ∈ ℕ0 )
7 5 6 sylbi ⊢ ( ( 0 ..^ 𝐿 ) ≠ ∅ → 𝐿 ∈ ℕ0 )
8 7 necon1bi ⊢ ( ¬ 𝐿 ∈ ℕ0 → ( 0 ..^ 𝐿 ) = ∅ )
9 fzo0 ⊢ ( 0 ..^ 0 ) = ∅
10 8 9 eqtr4di ⊢ ( ¬ 𝐿 ∈ ℕ0 → ( 0 ..^ 𝐿 ) = ( 0 ..^ 0 ) )
11 10 feq2d ⊢ ( ¬ 𝐿 ∈ ℕ0 → ( 𝑊 : ( 0 ..^ 𝐿 ) ⟶ 𝑆 ↔ 𝑊 : ( 0 ..^ 0 ) ⟶ 𝑆 ) )
12 11 biimpa ⊢ ( ( ¬ 𝐿 ∈ ℕ0 ∧ 𝑊 : ( 0 ..^ 𝐿 ) ⟶ 𝑆 ) → 𝑊 : ( 0 ..^ 0 ) ⟶ 𝑆 )
13 oveq2 ⊢ ( 𝑙 = 0 → ( 0 ..^ 𝑙 ) = ( 0 ..^ 0 ) )
14 13 feq2d ⊢ ( 𝑙 = 0 → ( 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 ↔ 𝑊 : ( 0 ..^ 0 ) ⟶ 𝑆 ) )
15 14 rspcev ⊢ ( ( 0 ∈ ℕ0 ∧ 𝑊 : ( 0 ..^ 0 ) ⟶ 𝑆 ) → ∃ 𝑙 ∈ ℕ0 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 )
16 4 12 15 sylancr ⊢ ( ( ¬ 𝐿 ∈ ℕ0 ∧ 𝑊 : ( 0 ..^ 𝐿 ) ⟶ 𝑆 ) → ∃ 𝑙 ∈ ℕ0 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 )
17 3 16 pm2.61ian ⊢ ( 𝑊 : ( 0 ..^ 𝐿 ) ⟶ 𝑆 → ∃ 𝑙 ∈ ℕ0 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 )
18 iswrd ⊢ ( 𝑊 ∈ Word 𝑆 ↔ ∃ 𝑙 ∈ ℕ0 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 )
19 17 18 sylibr ⊢ ( 𝑊 : ( 0 ..^ 𝐿 ) ⟶ 𝑆 → 𝑊 ∈ Word 𝑆 )