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 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑆 )