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

Metamath Proof Explorer

Theorem wrdf

Description: A word is a zero-based sequence with a recoverable upper limit. (Contributed by Stefan O'Rear, 15-Aug-2015)

Ref Expression
Assertion wrdf ( 𝑊 ∈ Word 𝑆 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑆 )

Proof

Step Hyp Ref Expression
1 iswrd ⊢ ( 𝑊 ∈ Word 𝑆 ↔ ∃ 𝑙 ∈ ℕ0 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 )
2 simpr ⊢ ( ( 𝑙 ∈ ℕ0 ∧ 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 ) → 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 )
3 fnfzo0hash ⊢ ( ( 𝑙 ∈ ℕ0 ∧ 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 ) → ( ♯ ‘ 𝑊 ) = 𝑙 )
4 3 oveq2d ⊢ ( ( 𝑙 ∈ ℕ0 ∧ 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 ) → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ..^ 𝑙 ) )
5 4 feq2d ⊢ ( ( 𝑙 ∈ ℕ0 ∧ 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 ) → ( 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑆 ↔ 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 ) )
6 2 5 mpbird ⊢ ( ( 𝑙 ∈ ℕ0 ∧ 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 ) → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑆 )
7 6 rexlimiva ⊢ ( ∃ 𝑙 ∈ ℕ0 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑆 )
8 1 7 sylbi ⊢ ( 𝑊 ∈ Word 𝑆 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑆 )