Metamath Proof Explorer

Theorem ccats1pfxeqrex

Description: There exists a symbol such that its concatenation after the prefix obtained by deleting the last symbol of a nonempty word results in the word itself. (Contributed by AV, 5-Oct-2018) (Revised by AV, 9-May-2020)

		Ref	Expression
	Assertion	ccats1pfxeqrex	$⊢ (W \in Word V \land U \in Word V \land \|U\| = \|W\| + 1) \to (W = U prefix \|W\| \to \exists s \in V U = W ++ ⟨“ s ”⟩)$

Proof

Step	Hyp	Ref	Expression
1		simp2	$⊢ (W \in Word V \land U \in Word V \land \|U\| = \|W\| + 1) \to U \in Word V$
2		lencl	$⊢ W \in Word V \to \|W\| \in ℕ_{0}$
3	2	3ad2ant1	$⊢ (W \in Word V \land U \in Word V \land \|U\| = \|W\| + 1) \to \|W\| \in ℕ_{0}$
4		nn0p1nn	$⊢ \|W\| \in ℕ_{0} \to \|W\| + 1 \in ℕ$
5		nngt0	$⊢ \|W\| + 1 \in ℕ \to 0 < \|W\| + 1$
6	3 4 5	3syl	$⊢ (W \in Word V \land U \in Word V \land \|U\| = \|W\| + 1) \to 0 < \|W\| + 1$
7		breq2	$⊢ \|U\| = \|W\| + 1 \to (0 < \|U\| \leftrightarrow 0 < \|W\| + 1)$
8	7	3ad2ant3	$⊢ (W \in Word V \land U \in Word V \land \|U\| = \|W\| + 1) \to (0 < \|U\| \leftrightarrow 0 < \|W\| + 1)$
9	6 8	mpbird	$⊢ (W \in Word V \land U \in Word V \land \|U\| = \|W\| + 1) \to 0 < \|U\|$
10		hashgt0n0	$⊢ (U \in Word V \land 0 < \|U\|) \to U \neq \emptyset$
11	1 9 10	syl2anc	$⊢ (W \in Word V \land U \in Word V \land \|U\| = \|W\| + 1) \to U \neq \emptyset$
12		lswcl	$⊢ (U \in Word V \land U \neq \emptyset) \to lastS (U) \in V$
13	1 11 12	syl2anc	$⊢ (W \in Word V \land U \in Word V \land \|U\| = \|W\| + 1) \to lastS (U) \in V$
14		ccats1pfxeq	$⊢ (W \in Word V \land U \in Word V \land \|U\| = \|W\| + 1) \to (W = U prefix \|W\| \to U = W ++ ⟨“ lastS (U) ”⟩)$
15		s1eq	$⊢ s = lastS (U) \to ⟨“ s ”⟩ = ⟨“ lastS (U) ”⟩$
16	15	oveq2d	$⊢ s = lastS (U) \to W ++ ⟨“ s ”⟩ = W ++ ⟨“ lastS (U) ”⟩$
17	16	rspceeqv	$⊢ (lastS (U) \in V \land U = W ++ ⟨“ lastS (U) ”⟩) \to \exists s \in V U = W ++ ⟨“ s ”⟩$
18	13 14 17	syl6an	$⊢ (W \in Word V \land U \in Word V \land \|U\| = \|W\| + 1) \to (W = U prefix \|W\| \to \exists s \in V U = W ++ ⟨“ s ”⟩)$