Theorem pfxid

Description: A word is a prefix of itself. (Contributed by Stefan O'Rear, 16-Aug-2015) (Revised by AV, 2-May-2020)

	Ref	Expression
Assertion	pfxid	⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 prefix ( ♯ ‘ 𝑆 ) ) = 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		lencl	⊢ ( 𝑆 ∈ Word 𝐴 → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
2		nn0fz0	⊢ ( ( ♯ ‘ 𝑆 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
3	1 2	sylib	⊢ ( 𝑆 ∈ Word 𝐴 → ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
4		pfxf	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 prefix ( ♯ ‘ 𝑆 ) ) : ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ⟶ 𝐴 )
5	3 4	mpdan	⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 prefix ( ♯ ‘ 𝑆 ) ) : ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ⟶ 𝐴 )
6	5	ffnd	⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 prefix ( ♯ ‘ 𝑆 ) ) Fn ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
7		wrdfn	⊢ ( 𝑆 ∈ Word 𝐴 → 𝑆 Fn ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
8		simpl	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → 𝑆 ∈ Word 𝐴 )
9	3	adantr	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
10		simpr	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
11		pfxfv	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 prefix ( ♯ ‘ 𝑆 ) ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
12	8 9 10 11	syl3anc	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 prefix ( ♯ ‘ 𝑆 ) ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
13	6 7 12	eqfnfvd	⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 prefix ( ♯ ‘ 𝑆 ) ) = 𝑆 )