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

Metamath Proof Explorer

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 ( ♯ ‘ 𝑆 ) ) = 𝑆 )