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 \in Word A \to S prefix \|S\| = S$

Step	Hyp	Ref	Expression
1		lencl	$⊢ S \in Word A \to \|S\| \in ℕ_{0}$
2		nn0fz0	$⊢ \|S\| \in ℕ_{0} \leftrightarrow \|S\| \in (0 \dots \|S\|)$
3	1 2	sylib	$⊢ S \in Word A \to \|S\| \in (0 \dots \|S\|)$
4		pfxf	$⊢ (S \in Word A \land \|S\| \in (0 \dots \|S\|)) \to (S prefix \|S\|) : (0 ..^\|S\|) ⟶ A$
5	3 4	mpdan	$⊢ S \in Word A \to (S prefix \|S\|) : (0 ..^\|S\|) ⟶ A$
6	5	ffnd	$⊢ S \in Word A \to (S prefix \|S\|) Fn (0 ..^\|S\|)$
7		wrdfn	$⊢ S \in Word A \to S Fn (0 ..^\|S\|)$
8		simpl	$⊢ (S \in Word A \land x \in (0 ..^\|S\|)) \to S \in Word A$
9	3	adantr	$⊢ (S \in Word A \land x \in (0 ..^\|S\|)) \to \|S\| \in (0 \dots \|S\|)$
10		simpr	$⊢ (S \in Word A \land x \in (0 ..^\|S\|)) \to x \in (0 ..^\|S\|)$
11		pfxfv	$⊢ (S \in Word A \land \|S\| \in (0 \dots \|S\|) \land x \in (0 ..^\|S\|)) \to (S prefix \|S\|) (x) = S (x)$
12	8 9 10 11	syl3anc	$⊢ (S \in Word A \land x \in (0 ..^\|S\|)) \to (S prefix \|S\|) (x) = S (x)$
13	6 7 12	eqfnfvd	$⊢ S \in Word A \to S prefix \|S\| = S$

Metamath Proof Explorer