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 ⊢ S ∈ Word A → S prefix S = S

Proof

Step Hyp Ref Expression
1 lencl ⊢ S ∈ Word A → S ∈ ℕ 0
2 nn0fz0 ⊢ S ∈ ℕ 0 ↔ S ∈ 0 … S
3 1 2 sylib ⊢ S ∈ Word A → S ∈ 0 … S
4 pfxf ⊢ S ∈ Word A ∧ S ∈ 0 … S → S prefix S : 0 ..^ S ⟶ A
5 3 4 mpdan ⊢ S ∈ Word A → S prefix S : 0 ..^ S ⟶ A
6 5 ffnd ⊢ S ∈ Word A → S prefix S Fn 0 ..^ S
7 wrdfn ⊢ S ∈ Word A → S Fn 0 ..^ S
8 simpl ⊢ S ∈ Word A ∧ x ∈ 0 ..^ S → S ∈ Word A
9 3 adantr ⊢ S ∈ Word A ∧ x ∈ 0 ..^ S → S ∈ 0 … S
10 simpr ⊢ S ∈ Word A ∧ x ∈ 0 ..^ S → x ∈ 0 ..^ S
11 pfxfv ⊢ S ∈ Word A ∧ S ∈ 0 … S ∧ x ∈ 0 ..^ S → S prefix S ⁡ x = S ⁡ x
12 8 9 10 11 syl3anc ⊢ S ∈ Word A ∧ x ∈ 0 ..^ S → S prefix S ⁡ x = S ⁡ x
13 6 7 12 eqfnfvd ⊢ S ∈ Word A → S prefix S = S